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.

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) [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] extends RingHom :

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.toFun 1 = 1
map_mul' : ∀ (x y : α), self.toFun (x * y) = self.toFun x * self.toFun y
map_zero' : self.toFun 0 = 0
map_add' : ∀ (x y : α), self.toFun (x + y) = self.toFun x + self.toFun y
monotone' : Monotone self.toFun
The proposition that the function preserves the order.

Instances For

def «term_→+*o_» :

Lean.TrailingParserDescr

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

«term_→+*o_» = Lean.ParserDescr.trailingNode `term_→+*o_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →+*o ") (Lean.ParserDescr.cat `term 26))

structure OrderRingIso (α : Type u_6) (β : Type u_7) [Mul α] [Mul β] [Add α] [Add β] [LE α] [LE β] extends RingEquiv :

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

def «term_≃+*o_» :

Lean.TrailingParserDescr

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

«term_≃+*o_» = Lean.ParserDescr.trailingNode `term_≃+*o_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃+*o ") (Lean.ParserDescr.cat `term 26))

def OrderRingHomClass.toOrderRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderHomClass 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' := ⋯ }

instance instCoeTCOrderRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderHomClass F α β] [RingHomClass F α β] :

CoeTC F (α →+*o β)

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

Equations

instCoeTCOrderRingHom = { coe := OrderRingHomClass.toOrderRingHom }

def OrderRingIsoClass.toOrderRingIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [OrderIsoClass F α β] [RingEquivClass F α β] (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' := ⋯ }

instance instCoeTCOrderRingIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [OrderIsoClass F α β] [RingEquivClass F α β] :

CoeTC F (α ≃+*o β)

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

Equations

instCoeTCOrderRingIso = { coe := OrderRingIsoClass.toOrderRingIso }

Ordered ring homomorphisms #

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

α →+o β

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

Equations

OrderRingHom.toOrderAddMonoidHom f = { toAddMonoidHom := { toZeroHom := { toFun := f.toFun, map_zero' := ⋯ }, map_add' := ⋯ }, monotone' := ⋯ }

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

Reinterpret an ordered ring homomorphism as an order homomorphism.

Equations

OrderRingHom.toOrderMonoidWithZeroHom f = { toMonoidWithZeroHom := { toZeroHom := { toFun := f.toFun, map_zero' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }, monotone' := ⋯ }

instance OrderRingHom.instFunLikeOrderRingHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :

FunLike (α →+*o β) α β

Equations

OrderRingHom.instFunLikeOrderRingHom = { coe := fun (f : α →+*o β) => f.toFun, coe_injective' := ⋯ }

instance OrderRingHom.instOrderHomClassOrderRingHomToLEToLEInstFunLikeOrderRingHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :

OrderHomClass (α →+*o β) α β

Equations

⋯ = ⋯

instance OrderRingHom.instRingHomClassOrderRingHomInstFunLikeOrderRingHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :

RingHomClass (α →+*o β) α β

Equations

⋯ = ⋯

theorem OrderRingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :

f.toFun = ⇑f

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

f = g

@[simp]

theorem OrderRingHom.toRingHom_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :

f.toRingHom = ↑f

@[simp]

theorem OrderRingHom.toOrderAddMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :

OrderRingHom.toOrderAddMonoidHom f = ↑f

@[simp]

theorem OrderRingHom.toOrderMonoidWithZeroHom_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :

OrderRingHom.toOrderMonoidWithZeroHom f = ↑f

@[simp]

theorem OrderRingHom.coe_coe_ringHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :

⇑↑f = ⇑f

@[simp]

theorem OrderRingHom.coe_coe_orderAddMonoidHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :

⇑↑f = ⇑f

@[simp]

theorem OrderRingHom.coe_coe_orderMonoidWithZeroHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :

⇑↑f = ⇑f

theorem OrderRingHom.coe_ringHom_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (a : α) :

↑f a = f a

theorem OrderRingHom.coe_orderAddMonoidHom_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (a : α) :

↑f a = f a

theorem OrderRingHom.coe_orderMonoidWithZeroHom_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (a : α) :

↑f a = f a

def OrderRingHom.copy {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (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

OrderRingHom.copy f f' h = let __src := RingHom.copy f.toRingHom f' h; let __src_1 := OrderAddMonoidHom.copy (OrderRingHom.toOrderAddMonoidHom f) f' h; { toRingHom := __src, monotone' := ⋯ }

@[simp]

theorem OrderRingHom.coe_copy {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (f' : α → β) (h : f' = ⇑f) :

⇑(OrderRingHom.copy f f' h) = f'

theorem OrderRingHom.copy_eq {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (f' : α → β) (h : f' = ⇑f) :

OrderRingHom.copy f f' h = f

def OrderRingHom.id (α : Type u_2) [NonAssocSemiring α] [Preorder α] :

α →+*o α

The identity as an ordered ring homomorphism.

Equations

OrderRingHom.id α = let __src := RingHom.id α; let __src_1 := OrderHom.id; { toRingHom := __src, monotone' := ⋯ }

instance OrderRingHom.instInhabitedOrderRingHom (α : Type u_2) [NonAssocSemiring α] [Preorder α] :

Inhabited (α →+*o α)

Equations

OrderRingHom.instInhabitedOrderRingHom α = { default := OrderRingHom.id α }

@[simp]

theorem OrderRingHom.coe_id (α : Type u_2) [NonAssocSemiring α] [Preorder α] :

⇑(OrderRingHom.id α) = id

@[simp]

theorem OrderRingHom.id_apply {α : Type u_2} [NonAssocSemiring α] [Preorder α] (a : α) :

(OrderRingHom.id α) a = a

@[simp]

theorem OrderRingHom.coe_ringHom_id {α : Type u_2} [NonAssocSemiring α] [Preorder α] :

↑(OrderRingHom.id α) = RingHom.id α

@[simp]

theorem OrderRingHom.coe_orderAddMonoidHom_id {α : Type u_2} [NonAssocSemiring α] [Preorder α] :

↑(OrderRingHom.id α) = OrderAddMonoidHom.id α

@[simp]

theorem OrderRingHom.coe_orderMonoidWithZeroHom_id {α : Type u_2} [NonAssocSemiring α] [Preorder α] :

↑(OrderRingHom.id α) = OrderMonoidWithZeroHom.id α

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

α →+*o γ

Composition of two OrderRingHoms as an OrderRingHom.

Equations

One or more equations did not get rendered due to their size.

@[simp]

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

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

@[simp]

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

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

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

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

@[simp]

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

OrderRingHom.comp f (OrderRingHom.id α) = f

@[simp]

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

OrderRingHom.comp (OrderRingHom.id β) f = f

@[simp]

theorem OrderRingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] {f₁ : β →+*o γ} {f₂ : β →+*o γ} {g : α →+*o β} (hg : Function.Surjective ⇑g) :

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

@[simp]

theorem OrderRingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] {f : β →+*o γ} {g₁ : α →+*o β} {g₂ : α →+*o β} (hf : Function.Injective ⇑f) :

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

instance OrderRingHom.instPreorderOrderRingHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :

Preorder (α →+*o β)

Equations

OrderRingHom.instPreorderOrderRingHom = Preorder.lift DFunLike.coe

instance OrderRingHom.instPartialOrderOrderRingHomToPreorder {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [PartialOrder β] :

PartialOrder (α →+*o β)

Equations

OrderRingHom.instPartialOrderOrderRingHomToPreorder = PartialOrder.lift (fun (f : α →+*o β) => ⇑f) ⋯

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' := ⋯ }

instance OrderRingIso.instEquivLikeOrderRingIso {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :

EquivLike (α ≃+*o β) α β

Equations

OrderRingIso.instEquivLikeOrderRingIso = { coe := fun (f : α ≃+*o β) => f.toFun, inv := fun (f : α ≃+*o β) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance OrderRingIso.instOrderIsoClassOrderRingIsoInstEquivLikeOrderRingIso {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :

OrderIsoClass (α ≃+*o β) α β

Equations

⋯ = ⋯

instance OrderRingIso.instRingEquivClassOrderRingIsoInstEquivLikeOrderRingIso {α : 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

OrderRingIso.refl α = { toRingEquiv := RingEquiv.refl α, map_le_map_iff' := ⋯ }

instance OrderRingIso.instInhabitedOrderRingIso (α : Type u_2) [Mul α] [Add α] [LE α] :

Inhabited (α ≃+*o α)

Equations

OrderRingIso.instInhabitedOrderRingIso α = { default := OrderRingIso.refl α }

@[simp]

theorem OrderRingIso.refl_apply (α : Type u_2) [Mul α] [Add α] [LE α] (x : α) :

(OrderRingIso.refl α) x = x

@[simp]

theorem OrderRingIso.coe_ringEquiv_refl (α : Type u_2) [Mul α] [Add α] [LE α] :

↑(OrderRingIso.refl α) = RingEquiv.refl α

@[simp]

theorem OrderRingIso.coe_orderIso_refl (α : Type u_2) [Mul α] [Add α] [LE α] :

↑(OrderRingIso.refl α) = OrderIso.refl α

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

OrderRingIso.symm e = { toRingEquiv := RingEquiv.symm e.toRingEquiv, map_le_map_iff' := ⋯ }

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

OrderRingIso.Simps.symm_apply e = ⇑(OrderRingIso.symm e)

@[simp]

theorem OrderRingIso.symm_symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :

OrderRingIso.symm (OrderRingIso.symm e) = 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

OrderRingIso.trans f g = { toRingEquiv := RingEquiv.trans f.toRingEquiv g.toRingEquiv, map_le_map_iff' := ⋯ }

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 γ) :

(OrderRingIso.trans f g).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 γ) :

↑(OrderRingIso.trans f g) = 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 : α) :

(OrderRingIso.trans f 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 β) :

OrderRingIso.trans e (OrderRingIso.symm e) = OrderRingIso.refl α

@[simp]

theorem OrderRingIso.symm_trans_self {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :

OrderRingIso.trans (OrderRingIso.symm e) e = OrderRingIso.refl β

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} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α ≃+*o β) :

α →+*o β

Reinterpret an ordered ring isomorphism as an ordered ring homomorphism.

Equations

OrderRingIso.toOrderRingHom f = { toRingHom := RingEquiv.toRingHom f.toRingEquiv, monotone' := ⋯ }

@[simp]

theorem OrderRingIso.toOrderRingHom_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α ≃+*o β) :

OrderRingIso.toOrderRingHom f = ↑f

@[simp]

theorem OrderRingIso.coe_toOrderRingHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α ≃+*o β) :

⇑↑f = ⇑f

@[simp]

theorem OrderRingIso.coe_toOrderRingHom_refl {α : Type u_2} [NonAssocSemiring α] [Preorder α] :

↑(OrderRingIso.refl α) = OrderRingHom.id α

theorem OrderRingIso.toOrderRingHom_injective {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :

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} [LinearOrderedField α] [LinearOrderedField β] [Archimedean β] :

Subsingleton (α →+*o β)

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} [LinearOrderedField α] [LinearOrderedField β] [Archimedean β] :

Subsingleton (α ≃+*o β)

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} [LinearOrderedField α] [Archimedean α] [LinearOrderedField β] :

Subsingleton (α ≃+*o β)

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

Equations

⋯ = ⋯