# mathlib3documentation

algebra.order.hom.ring

# Ordered ring homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Homomorphisms between ordered (semi)rings that respect the ordering.

## Main definitions #

• order_ring_hom : Monotone semiring homomorphisms.
• order_ring_iso : Monotone semiring isomorphisms.

## Notation #

• →+*o: Ordered ring homomorphisms.
• ≃+*o: Ordered ring isomorphisms.

## Tags #

ordered ring homomorphism, order homomorphism

structure order_ring_hom (α : Type u_6) (β : Type u_7) [preorder α] [preorder β] :
Type (max u_6 u_7)
• to_ring_hom : α →+* β
• monotone' :

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.

Instances for order_ring_hom
structure order_ring_iso (α : Type u_6) (β : Type u_7) [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] :
Type (max u_6 u_7)

order_ring_hom α β is the type of order-preserving semiring isomorphisms between α and β.

When possible, instead of parametrizing results over (f : order_ring_iso α β), you should parametrize over (F : Type*) [order_ring_iso_class F α β] (f : F).

When you extend this structure, make sure to extend order_ring_iso_class.

Instances for order_ring_iso
@[class]
structure order_ring_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β] :
Type (max u_6 u_7 u_8)
• to_ring_hom_class : β
• monotone : (f : 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 of this typeclass
Instances of other typeclasses for order_ring_hom_class
• order_ring_hom_class.has_sizeof_inst
@[class]
structure order_ring_iso_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] :
Type (max u_6 u_7 u_8)
• to_ring_equiv_class : β
• map_le_map_iff : (f : F) {a b : α}, f a f b a b

order_ring_iso_class F α β states that F is a type of ordered semiring isomorphisms. You should extend this class when you extend order_ring_iso.

Instances of this typeclass
Instances of other typeclasses for order_ring_iso_class
• order_ring_iso_class.has_sizeof_inst
@[protected, instance]
def order_ring_hom_class.to_order_add_monoid_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] :
Equations
@[protected, instance]
def order_ring_hom_class.to_order_monoid_with_zero_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] :
Equations
@[protected, instance]
def order_ring_iso_class.to_order_iso_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] [ β] :
β
Equations
@[protected, instance]
def order_ring_iso_class.to_order_ring_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] :
β
Equations
@[protected, instance]
def order_ring_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] :
→+*o β)
Equations
@[protected, instance]
def order_ring_iso.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] [ β] :
≃+*o β)
Equations

### Ordered ring homomorphisms #

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

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

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

Reinterpret an ordered ring homomorphism as an order homomorphism.

Equations
@[protected, instance]
def order_ring_hom.order_ring_hom_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
Equations
@[protected, instance]
def order_ring_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
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
theorem order_ring_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) :
@[ext]
theorem order_ring_hom.ext {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f g : α →+*o β} (h : (a : α), f a = g a) :
f = g
@[simp]
theorem order_ring_hom.to_ring_hom_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) :
@[simp]
theorem order_ring_hom.to_order_add_monoid_hom_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) :
@[simp]
theorem order_ring_hom.to_order_monoid_with_zero_hom_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) :
@[simp]
theorem order_ring_hom.coe_coe_ring_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) :
@[simp]
theorem order_ring_hom.coe_coe_order_add_monoid_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) :
@[simp]
theorem order_ring_hom.coe_coe_order_monoid_with_zero_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) :
@[norm_cast]
theorem order_ring_hom.coe_ring_hom_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) (a : α) :
f a = f a
@[norm_cast]
theorem order_ring_hom.coe_order_add_monoid_hom_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) (a : α) :
f a = f a
@[norm_cast]
theorem order_ring_hom.coe_order_monoid_with_zero_hom_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) (a : α) :
f a = f a
@[protected]
def order_ring_hom.copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (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
@[simp]
theorem order_ring_hom.coe_copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem order_ring_hom.copy_eq {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]
def order_ring_hom.id (α : Type u_2) [preorder α] :
α →+*o α

The identity as an ordered ring homomorphism.

Equations
@[protected, instance]
def order_ring_hom.inhabited (α : Type u_2) [preorder α] :
Equations
@[simp]
theorem order_ring_hom.coe_id (α : Type u_2) [preorder α] :
@[simp]
theorem order_ring_hom.id_apply {α : Type u_2} [preorder α] (a : α) :
a = a
@[simp]
theorem order_ring_hom.coe_ring_hom_id {α : Type u_2} [preorder α] :
@[simp]
@[protected]
def order_ring_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : β →+*o γ) (g : α →+*o β) :
α →+*o γ

Composition of two order_ring_homs as an order_ring_hom.

Equations
@[simp]
theorem order_ring_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : β →+*o γ) (g : α →+*o β) :
(f.comp g) = f g
@[simp]
theorem order_ring_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : β →+*o γ) (g : α →+*o β) (a : α) :
(f.comp g) a = f (g a)
theorem order_ring_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [preorder α] [preorder β] [preorder γ] [preorder δ] (f : γ →+*o δ) (g : β →+*o γ) (h : α →+*o β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem order_ring_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) :
f.comp = f
@[simp]
theorem order_ring_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+*o β) :
f = f
theorem order_ring_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] {f₁ f₂ : β →+*o γ} {g : α →+*o β} (hg : function.surjective g) :
f₁.comp g = f₂.comp g f₁ = f₂
theorem order_ring_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] {f : β →+*o γ} {g₁ g₂ : α →+*o β} (hf : function.injective f) :
f.comp g₁ = f.comp g₂ g₁ = g₂
@[protected, instance]
def order_ring_hom.preorder {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
Equations
@[protected, instance]
def order_ring_hom.partial_order {α : Type u_2} {β : Type u_3} [preorder α]  :
Equations

### Ordered ring isomorphisms #

def order_ring_iso.to_order_iso {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
α ≃o β

Reinterpret an ordered ring isomorphism as an order isomorphism.

Equations
@[protected, instance]
def order_ring_iso.order_ring_iso_class {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] :
Equations
@[protected, instance]
def order_ring_iso.has_coe_to_fun {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] :
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
theorem order_ring_iso.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
@[ext]
theorem order_ring_iso.ext {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] {f g : α ≃+*o β} (h : (a : α), f a = g a) :
f = g
@[simp]
theorem order_ring_iso.coe_mk {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+* β) (h : {a b : α}, e.to_fun a e.to_fun b a b) :
@[simp]
theorem order_ring_iso.mk_coe {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) (h : {a b : α}, e.to_fun a e.to_fun b a b) :
@[simp]
theorem order_ring_iso.to_ring_equiv_eq_coe {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
@[simp]
theorem order_ring_iso.to_order_iso_eq_coe {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
@[simp, norm_cast]
theorem order_ring_iso.coe_to_ring_equiv {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
@[simp, norm_cast]
theorem order_ring_iso.coe_to_order_iso {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
@[protected, refl]
def order_ring_iso.refl (α : Type u_2) [has_mul α] [has_add α] [has_le α] :
α ≃+*o α

The identity map as an ordered ring isomorphism.

Equations
@[protected, instance]
def order_ring_iso.inhabited (α : Type u_2) [has_mul α] [has_add α] [has_le α] :
Equations
@[simp]
theorem order_ring_iso.refl_apply (α : Type u_2) [has_mul α] [has_add α] [has_le α] (x : α) :
x = x
@[simp]
theorem order_ring_iso.coe_ring_equiv_refl (α : Type u_2) [has_mul α] [has_add α] [has_le α] :
@[simp]
theorem order_ring_iso.coe_order_iso_refl (α : Type u_2) [has_mul α] [has_add α] [has_le α] :
@[protected, symm]
def order_ring_iso.symm {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) :
β ≃+*o α

The inverse of an ordered ring isomorphism as an ordered ring isomorphism.

Equations
def order_ring_iso.simps.symm_apply {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) :
β α
Equations
@[simp]
theorem order_ring_iso.symm_symm {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) :
e.symm.symm = e
@[simp]
theorem order_ring_iso.trans_to_ring_equiv {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] [has_mul γ] [has_add γ] [has_le γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
@[protected, trans]
def order_ring_iso.trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] [has_mul γ] [has_add γ] [has_le γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
α ≃+*o γ

Composition of order_ring_isos as an order_ring_iso.

Equations
@[simp]
theorem order_ring_iso.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] [has_mul γ] [has_add γ] [has_le γ] (f : α ≃+*o β) (g : β ≃+*o γ) (a : α) :
(f.trans g) a = g (f a)
@[simp]
theorem order_ring_iso.self_trans_symm {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) :
@[simp]
theorem order_ring_iso.symm_trans_self {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) :
theorem order_ring_iso.symm_bijective {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] :
def order_ring_iso.to_order_ring_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ≃+*o β) :
α →+*o β

Reinterpret an ordered ring isomorphism as an ordered ring homomorphism.

Equations
@[simp]
theorem order_ring_iso.to_order_ring_hom_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ≃+*o β) :
@[simp, norm_cast]
theorem order_ring_iso.coe_to_order_ring_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ≃+*o β) :
@[simp]
theorem order_ring_iso.to_order_ring_hom_injective {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :

### Uniqueness #

There is at most one ordered ring homomorphism from a linear ordered field to an archimedean linear ordered field. Reciprocally, such an ordered ring homomorphism exists when the codomain is further conditionally complete.

@[protected, instance]
def order_ring_hom.subsingleton {α : Type u_2} {β : Type u_3} [archimedean β] :

There is at most one ordered ring homomorphism from a linear ordered field to an archimedean linear ordered field.

@[protected, instance]
def order_ring_iso.subsingleton_right {α : Type u_2} {β : Type u_3} [archimedean β] :

There is at most one ordered ring isomorphism between a linear ordered field and an archimedean linear ordered field.

@[protected, instance]
def order_ring_iso.subsingleton_left {α : Type u_2} {β : Type u_3} [archimedean α]  :

There is at most one ordered ring isomorphism between an archimedean linear ordered field and a linear ordered field.