algebra.order.hom.ring - mathlib docs

structure order_ring_hom (α : Type u_6) (β : Type u_7) [ordered_semiring α] [ordered_semiring β] :

Type (max u_6 u_7)

to_ring_hom : α →+* β
monotone' : monotone self.to_ring_hom.to_fun

order_ring_hom α β is the type of monotone semiring homomorphisms from α to β.

When possible, instead of parametrizing results over (f : order_ring_hom α β), you should parametrize over (F : Type*) [order_ring_hom_class F α β] (f : F). When you extend this structure, make sure to extend order_ring_hom_class.

source

@[class]

structure order_ring_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [ordered_semiring α] [ordered_semiring β] :

Type (max u_6 u_7 u_8)

to_ring_hom_class : ring_hom_class F α β
monotone : ∀ (f : F), monotone ⇑f

order_ring_hom_class F α β states that F is a type of ordered semiring homomorphisms. You should extend this typeclass when you extend order_ring_hom.

Instances

order_ring_hom.order_ring_hom_class

source

@[protected, instance]

def order_ring_hom_class.to_order_add_monoid_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] [order_ring_hom_class F α β] :

order_add_monoid_hom_class F α β

Equations

order_ring_hom_class.to_order_add_monoid_hom_class = {to_add_monoid_hom_class := {coe := ring_hom_class.coe order_ring_hom_class.to_ring_hom_class, coe_injective' := _, map_add := _, map_zero := _}, monotone := _}

source

@[protected, instance]

def order_ring_hom_class.to_order_monoid_with_zero_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] [order_ring_hom_class F α β] :

order_monoid_with_zero_hom_class F α β

Equations

order_ring_hom_class.to_order_monoid_with_zero_hom_class = {to_monoid_with_zero_hom_class := {coe := ring_hom_class.coe order_ring_hom_class.to_ring_hom_class, coe_injective' := _, map_mul := _, map_one := _, map_zero := _}, monotone := _}

source

@[protected, instance]

def order_ring_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] [order_ring_hom_class F α β] :

has_coe_t F (α →+*o β)

Equations

order_ring_hom.has_coe_t = {coe := λ (f : F), {to_ring_hom := {to_fun := ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, monotone' := _}}

source

def order_ring_hom.to_order_add_monoid_hom {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) :

α →+o β

Reinterpret an ordered ring homomorphism as an ordered additive monoid homomorphism.

Equations

f.to_order_add_monoid_hom = {to_add_monoid_hom := {to_fun := f.to_ring_hom.to_fun, map_zero' := _, map_add' := _}, monotone' := _}

source

def order_ring_hom.to_order_monoid_with_zero_hom {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) :

α →*₀o β

Reinterpret an ordered ring homomorphism as an order homomorphism.

Equations

f.to_order_monoid_with_zero_hom = {to_monoid_with_zero_hom := {to_fun := f.to_ring_hom.to_fun, map_zero' := _, map_one' := _, map_mul' := _}, monotone' := _}

source

@[protected, instance]

def order_ring_hom.order_ring_hom_class {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] :

order_ring_hom_class (α →+*o β) α β

Equations

order_ring_hom.order_ring_hom_class = {to_ring_hom_class := {coe := λ (f : α →+*o β), f.to_ring_hom.to_fun, coe_injective' := _, map_mul := _, map_one := _, map_add := _, map_zero := _}, monotone := _}

source

@[protected, instance]

def order_ring_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] :

has_coe_to_fun (α →+*o β) (λ (_x : α →+*o β), α → β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

order_ring_hom.has_coe_to_fun = {coe := λ (f : α →+*o β), f.to_ring_hom.to_fun}

source

theorem order_ring_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) :

f.to_ring_hom.to_fun = ⇑f

source

@[ext]

theorem order_ring_hom.ext {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] {f g : α →+*o β} (h : ∀ (a : α), ⇑f a = ⇑g a) :

f = g

source

@[simp]

theorem order_ring_hom.to_ring_hom_eq_coe {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) :

f.to_ring_hom = ↑f

source

@[simp]

theorem order_ring_hom.to_order_add_monoid_hom_eq_coe {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) :

f.to_order_add_monoid_hom = ↑f

source

@[simp]

theorem order_ring_hom.to_order_monoid_with_zero_hom_eq_coe {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) :

f.to_order_monoid_with_zero_hom = ↑f

source

@[simp]

theorem order_ring_hom.coe_coe_ring_hom {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) :

⇑↑f = ⇑f

source

@[simp]

theorem order_ring_hom.coe_coe_order_add_monoid_hom {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) :

⇑↑f = ⇑f

source

@[simp]

theorem order_ring_hom.coe_coe_order_monoid_with_zero_hom {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) :

⇑↑f = ⇑f

source

@[norm_cast]

theorem order_ring_hom.coe_ring_hom_apply {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) (a : α) :

⇑↑f a = ⇑f a

source

@[norm_cast]

theorem order_ring_hom.coe_order_add_monoid_hom_apply {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) (a : α) :

⇑↑f a = ⇑f a

source

@[norm_cast]

theorem order_ring_hom.coe_order_monoid_with_zero_hom_apply {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) (a : α) :

⇑↑f a = ⇑f a

source

@[protected]

def order_ring_hom.copy {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) (f' : α → β) (h : f' = ⇑f) :

α →+*o β

Copy of a order_ring_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations

f.copy f' h = {to_ring_hom := {to_fun := (f.to_ring_hom.copy f' h).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, monotone' := _}

source

@[protected]

def order_ring_hom.id (α : Type u_2) [ordered_semiring α] :

α →+*o α

The identity as an ordered ring homomorphism.

Equations

order_ring_hom.id α = {to_ring_hom := {to_fun := (ring_hom.id α).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, monotone' := _}

source

@[protected, instance]

def order_ring_hom.inhabited (α : Type u_2) [ordered_semiring α] :

inhabited (α →+*o α)

Equations

order_ring_hom.inhabited α = {default := order_ring_hom.id α _inst_1}

source

@[simp]

theorem order_ring_hom.coe_id (α : Type u_2) [ordered_semiring α] :

⇑(order_ring_hom.id α) = id

source

@[simp]

theorem order_ring_hom.id_apply {α : Type u_2} [ordered_semiring α] (a : α) :

⇑(order_ring_hom.id α) a = a

source

@[simp]

theorem order_ring_hom.coe_ring_hom_id {α : Type u_2} [ordered_semiring α] :

↑(order_ring_hom.id α) = ring_hom.id α

source

@[simp]

theorem order_ring_hom.coe_order_add_monoid_hom_id {α : Type u_2} [ordered_semiring α] :

↑(order_ring_hom.id α) = order_add_monoid_hom.id α

source

@[simp]

theorem order_ring_hom.coe_order_monoid_with_zero_hom_id {α : Type u_2} [ordered_semiring α] :

↑(order_ring_hom.id α) = order_monoid_with_zero_hom.id α

source

@[protected]

def order_ring_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ordered_semiring α] [ordered_semiring β] [ordered_semiring γ] (f : β →+*o γ) (g : α →+*o β) :

α →+*o γ

Composition of two order_ring_homs as an order_ring_hom.

Equations

f.comp g = {to_ring_hom := {to_fun := (f.to_ring_hom.comp g.to_ring_hom).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, monotone' := _}

source

@[simp]

theorem order_ring_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ordered_semiring α] [ordered_semiring β] [ordered_semiring γ] (f : β →+*o γ) (g : α →+*o β) :

⇑(f.comp g) = ⇑f ∘ ⇑g

source

@[simp]

theorem order_ring_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ordered_semiring α] [ordered_semiring β] [ordered_semiring γ] (f : β →+*o γ) (g : α →+*o β) (a : α) :

⇑(f.comp g) a = ⇑f (⇑g a)

source

theorem order_ring_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [ordered_semiring α] [ordered_semiring β] [ordered_semiring γ] [ordered_semiring δ] (f : γ →+*o δ) (g : β →+*o γ) (h : α →+*o β) :

(f.comp g).comp h = f.comp (g.comp h)

source

@[simp]

theorem order_ring_hom.comp_id {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) :

f.comp (order_ring_hom.id α) = f

source

@[simp]

theorem order_ring_hom.id_comp {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] (f : α →+*o β) :

(order_ring_hom.id β).comp f = f

source

theorem order_ring_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ordered_semiring α] [ordered_semiring β] [ordered_semiring γ] {f₁ f₂ : β →+*o γ} {g : α →+*o β} (hg : function.surjective ⇑g) :

f₁.comp g = f₂.comp g ↔ f₁ = f₂

source

theorem order_ring_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ordered_semiring α] [ordered_semiring β] [ordered_semiring γ] {f : β →+*o γ} {g₁ g₂ : α →+*o β} (hf : function.injective ⇑f) :

f.comp g₁ = f.comp g₂ ↔ g₁ = g₂

source

@[protected, instance]

def order_ring_hom.partial_order {α : Type u_2} {β : Type u_3} [ordered_semiring α] [ordered_semiring β] :

partial_order (α →+*o β)

Equations

order_ring_hom.partial_order = partial_order.lift coe_fn order_ring_hom.partial_order._proof_1

mathlib documentation

Ordered ring homomorphisms #

Main definitions #

Notation #

Tags #

Ordered ring homomorphisms #