# Documentation

Mathlib.Algebra.Order.Hom.Ring

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

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

Instances For

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.

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.

Instances For

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.

Instances For
class OrderRingHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [] [] [] [] extends :
Type (max (max u_6 u_7) u_8)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• map_mul : ∀ (f : F) (x y : α), f (x * y) = f x * f y
• map_one : ∀ (f : F), f 1 = 1
• map_add : ∀ (f : F) (x y : α), f (x + y) = f x + f y
• map_zero : ∀ (f : F), f 0 = 0
• monotone : ∀ (f : F), Monotone f

The proposition that the function preserves the order.

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

Instances
class OrderRingIsoClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] extends :
Type (max (max u_6 u_7) u_8)
• coe : Fαβ
• inv : Fβα
• left_inv : ∀ (e : F),
• right_inv : ∀ (e : F),
• coe_injective' : ∀ (e g : F), e = g
• map_mul : ∀ (f : F) (a b : α), f (a * b) = f a * f b
• map_add : ∀ (f : F) (a b : α), f (a + b) = f a + f b
• map_le_map_iff : ∀ (f : F) {a b : α}, f a f b a b

The proposition that the function preserves the order bijectively.

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

Instances
instance OrderRingHomClass.toOrderAddMonoidHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [] :
instance OrderRingHomClass.toOrderMonoidWithZeroHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [] :
instance OrderRingIsoClass.toOrderIsoClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [] :
instance OrderRingIsoClass.toOrderRingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [] :
def OrderRingHomClass.toOrderRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [] (f : F) :
α →+*o β

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

Instances For
instance instCoeTCOrderRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [] :
CoeTC F (α →+*o β)

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

def OrderRingIsoClass.toOrderRingIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [] (f : F) :
α ≃+*o β

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

Instances For
instance instCoeTCOrderRingIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [] :
CoeTC F (α ≃+*o β)

Any type satisfying OrderRingIsoClass can be cast into OrderRingIso via 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.

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

Reinterpret an ordered ring homomorphism as an order homomorphism.

Instances For
instance OrderRingHom.instOrderRingHomClassOrderRingHom {α : Type u_2} {β : Type u_3} [] [] [] [] :
theorem OrderRingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
f.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 β) :
@[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.

Instances For
@[simp]
theorem OrderRingHom.coe_copy {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) (f' : αβ) (h : f' = f) :
↑() = f'
theorem OrderRingHom.copy_eq {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) (f' : αβ) (h : f' = f) :
= f
def OrderRingHom.id (α : Type u_2) [] [] :
α →+*o α

The identity as an ordered ring homomorphism.

Instances For
@[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.

Instances For
@[simp]
theorem OrderRingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] (f : β →+*o γ) (g : α →+*o β) :
↑() = f g
@[simp]
theorem OrderRingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] (f : β →+*o γ) (g : α →+*o β) (a : α) :
↑() 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 β) :
=
@[simp]
theorem OrderRingHom.comp_id {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
@[simp]
theorem OrderRingHom.id_comp {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →+*o β) :
@[simp]
theorem OrderRingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] {f₁ : β →+*o γ} {f₂ : β →+*o γ} {g : α →+*o β} (hg : ) :
= f₁ = f₂
@[simp]
theorem OrderRingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] {f : β →+*o γ} {g₁ : α →+*o β} {g₂ : α →+*o β} (hf : ) :
= g₁ = g₂
instance OrderRingHom.instPreorderOrderRingHom {α : Type u_2} {β : Type u_3} [] [] [] [] :
instance OrderRingHom.instPartialOrderOrderRingHomToPreorder {α : Type u_2} {β : Type u_3} [] [] [] [] :

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

Instances For
instance OrderRingIso.instOrderRingIsoClassOrderRingIso {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
theorem OrderRingIso.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
f.toFun = f

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

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 : α}, Equiv.toFun e.toEquiv a Equiv.toFun e.toEquiv 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 : α}, Equiv.toFun (e).toEquiv a Equiv.toFun (e).toEquiv 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.

Instances For
instance OrderRingIso.instInhabitedOrderRingIso (α : Type u_2) [Mul α] [Add α] [LE α] :
@[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.

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]

Instances For
@[simp]
theorem OrderRingIso.symm_symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
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.

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 γ) :
().toRingEquiv = RingEquiv.trans f.toRingEquiv 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 γ) :
↑() = RingEquiv.trans f.toRingEquiv 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 : α) :
↑() a = g (f a)
@[simp]
theorem OrderRingIso.self_trans_symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
@[simp]
theorem OrderRingIso.symm_trans_self {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
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.

Instances For
@[simp]
theorem OrderRingIso.toOrderRingHom_eq_coe {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α ≃+*o β) :
@[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.

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.

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.