# Ordered ring homomorphisms #

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

## Main definitions #

• OrderRingHom : Monotone semiring homomorphisms.
• OrderRingIso : Monotone semiring isomorphisms.

## Notation #

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

## Implementation notes #

This file used to define typeclasses for order-preserving ring homomorphisms and isomorphisms. In #10544, we migrated from assumptions like [FunLike F R S] [OrderRingHomClass F R S] to assumptions like [FunLike F R S] [OrderHomClass F R S] [RingHomClass F R S], making some typeclasses and instances irrelevant.

## Tags #

ordered ring homomorphism, order homomorphism

structure OrderRingHom (α : Type u_6) (β : Type u_7) [] [] [] [] extends :
Type (max u_6 u_7)

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

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

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

• toFun : αβ
• map_one' : (self.toRingHom).toFun 1 = 1
• map_mul' : ∀ (x y : α), (self.toRingHom).toFun (x * y) = (self.toRingHom).toFun x * (self.toRingHom).toFun y
• map_zero' : (self.toRingHom).toFun 0 = 0
• map_add' : ∀ (x y : α), (self.toRingHom).toFun (x + y) = (self.toRingHom).toFun x + (self.toRingHom).toFun y
• monotone' : Monotone (self.toRingHom).toFun

The proposition that the function preserves the order.

Instances For
theorem OrderRingHom.monotone' {α : Type u_6} {β : Type u_7} [] [] [] [] (self : α →+*o β) :
Monotone (self.toRingHom).toFun

The proposition that the function preserves the order.

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

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

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

Equations
Instances For
structure OrderRingIso (α : Type u_6) (β : Type u_7) [Mul α] [Mul β] [Add α] [Add β] [LE α] [LE β] extends :
Type (max u_6 u_7)

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

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

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

• toFun : αβ
• invFun : βα
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_mul' : ∀ (x y : α), self.toFun (x * y) = self.toFun x * self.toFun y
• map_add' : ∀ (x y : α), self.toFun (x + y) = self.toFun x + self.toFun y
• map_le_map_iff' : ∀ {a b : α}, self.toFun a self.toFun b a b

The proposition that the function preserves the order bijectively.

Instances For
theorem OrderRingIso.map_le_map_iff' {α : Type u_6} {β : Type u_7} [Mul α] [Mul β] [Add α] [Add β] [LE α] [LE β] (self : α ≃+*o β) {a : α} {b : α} :
self.toFun a self.toFun b a b

The proposition that the function preserves the order bijectively.

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

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

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

Equations
Instances For
def OrderRingHomClass.toOrderRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] [] [] [] [] [RingHomClass F α β] (f : F) :
α →+*o β

Turn an element of a type F satisfying OrderHomClass F α β and RingHomClass F α β into an actual OrderRingHom. This is declared as the default coercion from F to α →+*o β.

Equations
• f = let __src := f; { toRingHom := __src, monotone' := }
Instances For
instance instCoeTCOrderRingHomOfOrderHomClassOfRingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [] [] [] [] [] [RingHomClass F α β] :
CoeTC F (α →+*o β)

Any type satisfying OrderRingHomClass can be cast into OrderRingHom via OrderRingHomClass.toOrderRingHom.

Equations
• instCoeTCOrderRingHomOfOrderHomClassOfRingHomClass = { coe := OrderRingHomClass.toOrderRingHom }
def OrderRingIsoClass.toOrderRingIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [] [] (f : F) :
α ≃+*o β

Turn an element of a type F satisfying OrderIsoClass F α β and RingEquivClass F α β into an actual OrderRingIso. This is declared as the default coercion from F to α ≃+*o β.

Equations
• f = let __src := f; { toRingEquiv := __src, map_le_map_iff' := }
Instances For
instance instCoeTCOrderRingIsoOfOrderIsoClassOfRingEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [] [] :
CoeTC F (α ≃+*o β)

Any type satisfying OrderRingIsoClass can be cast into OrderRingIso via OrderRingIsoClass.toOrderRingIso.

Equations
• instCoeTCOrderRingIsoOfOrderIsoClassOfRingEquivClass = { coe := OrderRingIsoClass.toOrderRingIso }

### Ordered ring homomorphisms #

def OrderRingHom.toOrderAddMonoidHom {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
α →+o β

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

Equations
• f.toOrderAddMonoidHom = { toFun := (f.toRingHom).toFun, map_zero' := , map_add' := , monotone' := }
Instances For
def OrderRingHom.toOrderMonoidWithZeroHom {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
α →*₀o β

Reinterpret an ordered ring homomorphism as an order homomorphism.

Equations
• f.toOrderMonoidWithZeroHom = { toFun := (f.toRingHom).toFun, map_zero' := , map_one' := , map_mul' := , monotone' := }
Instances For
instance OrderRingHom.instFunLike {α : Type u_2} {β : Type u_3} [] [] [] [] :
FunLike (α →+*o β) α β
Equations
• OrderRingHom.instFunLike = { coe := fun (f : α →+*o β) => (f.toRingHom).toFun, coe_injective' := }
instance OrderRingHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [] [] [] [] :
OrderHomClass (α →+*o β) α β
Equations
• =
instance OrderRingHom.instRingHomClass {α : Type u_2} {β : Type u_3} [] [] [] [] :
RingHomClass (α →+*o β) α β
Equations
• =
theorem OrderRingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
(f.toRingHom).toFun = f
theorem OrderRingHom.ext {α : Type u_2} {β : Type u_3} [] [] [] [] {f : α →+*o β} {g : α →+*o β} (h : ∀ (a : α), f a = g a) :
f = g
@[simp]
theorem OrderRingHom.toRingHom_eq_coe {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
f.toRingHom = f
@[simp]
theorem OrderRingHom.toOrderAddMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
@[simp]
theorem OrderRingHom.toOrderMonoidWithZeroHom_eq_coe {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
f.toOrderMonoidWithZeroHom = f
@[simp]
theorem OrderRingHom.coe_coe_ringHom {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
f = f
@[simp]
theorem OrderRingHom.coe_coe_orderAddMonoidHom {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
f = f
@[simp]
theorem OrderRingHom.coe_coe_orderMonoidWithZeroHom {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
f = f
theorem OrderRingHom.coe_ringHom_apply {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) (a : α) :
f a = f a
theorem OrderRingHom.coe_orderAddMonoidHom_apply {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) (a : α) :
f a = f a
theorem OrderRingHom.coe_orderMonoidWithZeroHom_apply {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) (a : α) :
f a = f a
def OrderRingHom.copy {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) (f' : αβ) (h : f' = f) :
α →+*o β

Copy of an OrderRingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• f.copy f' h = let __src := f.copy f' h; let __src_1 := f.toOrderAddMonoidHom.copy f' h; { toRingHom := __src, monotone' := }
Instances For
@[simp]
theorem OrderRingHom.coe_copy {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem OrderRingHom.copy_eq {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) (f' : αβ) (h : f' = f) :
f.copy f' h = f
def OrderRingHom.id (α : Type u_2) [] [] :
α →+*o α

The identity as an ordered ring homomorphism.

Equations
• = let __src := ; let __src_1 := OrderHom.id; { toRingHom := __src, monotone' := }
Instances For
instance OrderRingHom.instInhabited (α : Type u_2) [] [] :
Equations
• = { default := }
@[simp]
theorem OrderRingHom.coe_id (α : Type u_2) [] [] :
() = id
@[simp]
theorem OrderRingHom.id_apply {α : Type u_2} [] [] (a : α) :
() a = a
@[simp]
theorem OrderRingHom.coe_ringHom_id {α : Type u_2} [] [] :
() =
@[simp]
theorem OrderRingHom.coe_orderAddMonoidHom_id {α : Type u_2} [] [] :
@[simp]
def OrderRingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] (f : β →+*o γ) (g : α →+*o β) :
α →+*o γ

Composition of two OrderRingHoms as an OrderRingHom.

Equations
• f.comp g = let __src := f.comp g.toRingHom; let __src_1 := f.toOrderAddMonoidHom.comp g.toOrderAddMonoidHom; { toRingHom := __src, monotone' := }
Instances For
@[simp]
theorem OrderRingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] (f : β →+*o γ) (g : α →+*o β) :
(f.comp g) = f g
@[simp]
theorem OrderRingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] (f : β →+*o γ) (g : α →+*o β) (a : α) :
(f.comp g) a = f (g a)
theorem OrderRingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] [] [] [] [] (f : γ →+*o δ) (g : β →+*o γ) (h : α →+*o β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem OrderRingHom.comp_id {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
f.comp () = f
@[simp]
theorem OrderRingHom.id_comp {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
().comp f = f
@[simp]
theorem OrderRingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] {f₁ : β →+*o γ} {f₂ : β →+*o γ} {g : α →+*o β} (hg : ) :
f₁.comp g = f₂.comp g f₁ = f₂
@[simp]
theorem OrderRingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] {f : β →+*o γ} {g₁ : α →+*o β} {g₂ : α →+*o β} (hf : ) :
f.comp g₁ = f.comp g₂ g₁ = g₂
instance OrderRingHom.instPreorder {α : Type u_2} {β : Type u_3} [] [] [] [] :
Equations
instance OrderRingHom.instPartialOrder {α : Type u_2} {β : Type u_3} [] [] [] [] :
Equations

### Ordered ring isomorphisms #

def OrderRingIso.toOrderIso {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
α ≃o β

Reinterpret an ordered ring isomorphism as an order isomorphism.

Equations
• f = { toEquiv := f.toEquiv, map_rel_iff' := }
Instances For
instance OrderRingIso.instEquivLike {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
EquivLike (α ≃+*o β) α β
Equations
• OrderRingIso.instEquivLike = { coe := fun (f : α ≃+*o β) => f.toFun, inv := fun (f : α ≃+*o β) => f.invFun, left_inv := , right_inv := , coe_injective' := }
instance OrderRingIso.instOrderIsoClass {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
OrderIsoClass (α ≃+*o β) α β
Equations
• =
instance OrderRingIso.instRingEquivClass {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
RingEquivClass (α ≃+*o β) α β
Equations
• =
theorem OrderRingIso.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
f.toFun = f
theorem OrderRingIso.ext {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] {f : α ≃+*o β} {g : α ≃+*o β} (h : ∀ (a : α), f a = g a) :
f = g
@[simp]
theorem OrderRingIso.coe_mk {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+* β) (h : ∀ {a b : α}, e.toFun a e.toFun b a b) :
{ toRingEquiv := e, map_le_map_iff' := h } = e
@[simp]
theorem OrderRingIso.mk_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) (h : ∀ {a b : α}, (e).toFun a (e).toFun b a b) :
{ toRingEquiv := e, map_le_map_iff' := h } = e
@[simp]
theorem OrderRingIso.toRingEquiv_eq_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
f.toRingEquiv = f
@[simp]
theorem OrderRingIso.toOrderIso_eq_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
f = f
@[simp]
theorem OrderRingIso.coe_toRingEquiv {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
f = f
@[simp]
theorem OrderRingIso.coe_toOrderIso {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
f = f
def OrderRingIso.refl (α : Type u_2) [Mul α] [Add α] [LE α] :
α ≃+*o α

The identity map as an ordered ring isomorphism.

Equations
• = { toRingEquiv := , map_le_map_iff' := }
Instances For
instance OrderRingIso.instInhabited (α : Type u_2) [Mul α] [Add α] [LE α] :
Equations
• = { default := }
@[simp]
theorem OrderRingIso.refl_apply (α : Type u_2) [Mul α] [Add α] [LE α] (x : α) :
x = x
@[simp]
theorem OrderRingIso.coe_ringEquiv_refl (α : Type u_2) [Mul α] [Add α] [LE α] :
@[simp]
theorem OrderRingIso.coe_orderIso_refl (α : Type u_2) [Mul α] [Add α] [LE α] :
def OrderRingIso.symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
β ≃+*o α

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

Equations
• e.symm = { toRingEquiv := e.symm, map_le_map_iff' := }
Instances For
def OrderRingIso.Simps.symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
βα

See Note [custom simps projection]

Equations
• = e.symm
Instances For
@[simp]
theorem OrderRingIso.symm_symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
e.symm.symm = e
def OrderRingIso.trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
α ≃+*o γ

Composition of OrderRingIsos as an OrderRingIso.

Equations
• f.trans g = { toRingEquiv := f.trans g.toRingEquiv, map_le_map_iff' := }
Instances For
theorem OrderRingIso.trans_toRingEquiv {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
(f.trans g).toRingEquiv = f.trans g.toRingEquiv
@[simp]
theorem OrderRingIso.trans_toRingEquiv_aux {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
(f.trans g) = f.trans g.toRingEquiv
@[simp]
theorem OrderRingIso.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) (a : α) :
(f.trans g) a = g (f a)
@[simp]
theorem OrderRingIso.self_trans_symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
e.trans e.symm =
@[simp]
theorem OrderRingIso.symm_trans_self {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
e.symm.trans e =
theorem OrderRingIso.symm_bijective {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
Function.Bijective OrderRingIso.symm
def OrderRingIso.toOrderRingHom {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α ≃+*o β) :
α →+*o β

Reinterpret an ordered ring isomorphism as an ordered ring homomorphism.

Equations
• f.toOrderRingHom = { toRingHom := f.toRingHom, monotone' := }
Instances For
@[simp]
theorem OrderRingIso.toOrderRingHom_eq_coe {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α ≃+*o β) :
f.toOrderRingHom = f
@[simp]
theorem OrderRingIso.coe_toOrderRingHom {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α ≃+*o β) :
f = f
@[simp]
theorem OrderRingIso.coe_toOrderRingHom_refl {α : Type u_2} [] [] :
theorem OrderRingIso.toOrderRingHom_injective {α : Type u_2} {β : Type u_3} [] [] [] [] :
Function.Injective OrderRingIso.toOrderRingHom

### 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.

instance OrderRingHom.subsingleton {α : Type u_2} {β : Type u_3} [] :

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

Equations
• =
instance OrderRingIso.subsingleton_right {α : Type u_2} {β : Type u_3} [] :

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

Equations
• =
instance OrderRingIso.subsingleton_left {α : Type u_2} {β : Type u_3} [] :

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

Equations
• =