Mathlib.Algebra.Order.Hom.Ring

OrderRingHom structure

(α β : Type*) [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β]
  [Preorder β] extends α →+* β

Full source

/-- `OrderRingHom α β`, denoted `α →+*o β`,
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`. -/
structure OrderRingHom (α β : Type*) [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β]
  [Preorder β] extends α →+* β where
  /-- The proposition that the function preserves the order. -/
  monotone' : Monotone toFun

Monotone Semiring Homomorphism

Informal description

The structure `OrderRingHom α β`, denoted as `α →+*o β`, represents monotone semiring homomorphisms from `α` to `β`. These are maps that preserve both the ring structure (addition and multiplication) and the order relation between elements. More precisely, given two (semi)rings `α` and `β` equipped with preorders, an `OrderRingHom` is a semiring homomorphism `f : α →+* β` that is also monotone, i.e., for any `x y : α`, if `x ≤ y`, then `f x ≤ f y`.

term_→+*o_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
infixl:25 " →+*o " => OrderRingHom

Ordered ring homomorphism notation (`→+*o`)

Informal description

The notation `→+*o` denotes the type of ordered ring homomorphisms between two ordered semirings (or rings) `α` and `β`. These are ring homomorphisms that are also monotone (order-preserving) functions. More precisely, given: - `α` and `β` as non-associative semirings with preorders - A function `f : α → β` that is both a ring homomorphism (`→+*`) and order-preserving (`o`) The notation `f : α →+*o β` represents such an ordered ring homomorphism.

OrderRingIso structure

(α β : Type*) [Mul α] [Mul β] [Add α] [Add β] [LE α] [LE β] extends
  α ≃+* β

Full source

/-- `OrderRingIso α β`, denoted as `α ≃+*o β`,
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`. -/
structure OrderRingIso (α β : Type*) [Mul α] [Mul β] [Add α] [Add β] [LE α] [LE β] extends
  α ≃+* β where
  /-- The proposition that the function preserves the order bijectively. -/
  map_le_map_iff' {a b : α} : toFun a ≤ toFun b ↔ a ≤ b

Order-preserving semiring isomorphism

Informal description

The structure `OrderRingIso α β`, denoted as $\alpha \simeq_{+*o} \beta$, represents order-preserving semiring isomorphisms between two ordered semirings $\alpha$ and $\beta$. It extends the structure of a semiring isomorphism $\alpha \simeq_{+*} \beta$ and additionally requires that the isomorphism preserves the order relation.

term_≃+*o_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
infixl:25 " ≃+*o " => OrderRingIso

Ordered ring isomorphism notation

Informal description

The notation `≃+*o` denotes an ordered ring isomorphism, which is a bijective semiring homomorphism between ordered (semi)rings that is also monotone (order-preserving).

OrderRingHomClass.toOrderRingHom definition

 [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderHomClass F α β] [RingHomClass F α β]
  (f : F) : α →+*o β

Full source

/-- 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 β`. -/
@[coe]
def OrderRingHomClass.toOrderRingHom [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β]
    [Preorder β] [OrderHomClass F α β] [RingHomClass F α β] (f : F) : α →+*o β :=
{ (f : α →+* β) with monotone' := OrderHomClass.monotone f}

Monotone semiring homomorphism from order-preserving ring homomorphism class

Informal description

Given a type `F` that satisfies both `OrderHomClass F α β` (order-preserving morphisms) and `RingHomClass F α β` (ring homomorphisms), and given two (semi)rings `α` and `β` equipped with preorders, this function constructs a monotone semiring homomorphism `α →+*o β` from an element `f : F`. The resulting homomorphism preserves both the ring structure (addition and multiplication) and the order relation, meaning that for any `x, y ∈ α`, if `x ≤ y`, then `f(x) ≤ f(y)`.

instCoeTCOrderRingHomOfOrderHomClassOfRingHomClass instance

 [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderHomClass F α β] [RingHomClass F α β] :
  CoeTC F (α →+*o β)

Full source

/-- Any type satisfying `OrderRingHomClass` can be cast into `OrderRingHom` via
  `OrderRingHomClass.toOrderRingHom`. -/
instance [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β]
    [OrderHomClass F α β] [RingHomClass F α β] : CoeTC F (α →+*o β) :=
  ⟨OrderRingHomClass.toOrderRingHom⟩

Canonical Interpretation of Order-Preserving Ring Homomorphisms

Informal description

For any two (semi)rings $\alpha$ and $\beta$ equipped with preorders, and any type $F$ that satisfies both `OrderHomClass F \alpha \beta` (order-preserving morphisms) and `RingHomClass F \alpha \beta` (ring homomorphisms), there is a canonical way to interpret an element $f : F$ as a monotone semiring homomorphism $\alpha \to_{+*o} \beta$.

OrderRingIsoClass.toOrderRingIso definition

 [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [OrderIsoClass F α β] [RingEquivClass F α β] (f : F) : α ≃+*o β

Full source

/-- 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 β`. -/
@[coe]
def OrderRingIsoClass.toOrderRingIso [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β]
    [OrderIsoClass F α β] [RingEquivClass F α β] (f : F) : α ≃+*o β :=
{ (f : α ≃+* β) with map_le_map_iff' := map_le_map_iff f}

Order-preserving ring isomorphism from isomorphism class

Informal description

Given types $\alpha$ and $\beta$ equipped with multiplication, addition, and a preorder relation $\leq$, and a type $F$ that satisfies both `OrderIsoClass F α β` (order-preserving bijections) and `RingEquivClass F α β` (ring isomorphisms), this function constructs an actual order-preserving ring isomorphism $\alpha \simeq_{+*o} \beta$ from an element $f : F$. The resulting isomorphism preserves both the ring structure and the order relation, meaning that for any $x, y \in \alpha$, $x \leq y$ if and only if $f(x) \leq f(y)$.

instCoeTCOrderRingIsoOfOrderIsoClassOfRingEquivClass instance

 [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [OrderIsoClass F α β] [RingEquivClass F α β] : CoeTC F (α ≃+*o β)

Full source

/-- Any type satisfying `OrderRingIsoClass` can be cast into `OrderRingIso` via
  `OrderRingIsoClass.toOrderRingIso`. -/
instance [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [OrderIsoClass F α β]
    [RingEquivClass F α β] : CoeTC F (α ≃+*o β) :=
  ⟨OrderRingIsoClass.toOrderRingIso⟩

Canonical Interpretation of Order-Preserving Ring Isomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with multiplication, addition, and a preorder relation $\leq$, and any type $F$ that satisfies both `OrderIsoClass F α β` (order-preserving bijections) and `RingEquivClass F α β` (ring isomorphisms), there is a canonical way to interpret an element $f : F$ as an order-preserving ring isomorphism $\alpha \simeq_{+*o} \beta$.

OrderRingHom.toOrderAddMonoidHom definition

(f : α →+*o β) : α →+o β

Full source

/-- Reinterpret an ordered ring homomorphism as an ordered additive monoid homomorphism. -/
def toOrderAddMonoidHom (f : α →+*o β) : α →+o β :=
  { f with }

Monotone semiring homomorphism as monotone additive monoid homomorphism

Informal description

Given a monotone semiring homomorphism $ f : \alpha \to+*o \beta $ between preordered semirings, this function reinterprets $ f $ as a monotone additive monoid homomorphism $ \alpha \to+o \beta $. The resulting map preserves addition, the additive identity, and the order relation.

OrderRingHom.toOrderMonoidWithZeroHom definition

(f : α →+*o β) : α →*₀o β

Full source

/-- Reinterpret an ordered ring homomorphism as an order homomorphism. -/
def toOrderMonoidWithZeroHom (f : α →+*o β) : α →*₀o β :=
  { f with }

Monotone semiring homomorphism as monotone monoid with zero homomorphism

Informal description

Given a monotone semiring homomorphism $ f : \alpha \to+*o \beta $ between preordered semirings, this function reinterprets $ f $ as a monotone monoid with zero homomorphism $ \alpha \to*₀o \beta $. The resulting map preserves multiplication, the multiplicative identity, the zero element, and the order relation.

OrderRingHom.instFunLike instance

: FunLike (α →+*o β) α β

Full source

instance : FunLike (α →+*o β) α β where
  coe f := f.toFun
  coe_injective' f g h := by
    cases f; cases g; congr
    exact DFunLike.coe_injective' h

Function-Like Structure on Monotone Semiring Homomorphisms

Informal description

For any two (semi)rings $\alpha$ and $\beta$ equipped with preorders, the type $\alpha \to+*o \beta$ of monotone semiring homomorphisms has a function-like structure, meaning its elements can be coerced to functions from $\alpha$ to $\beta$ in an injective way.

OrderRingHom.instOrderHomClass instance

: OrderHomClass (α →+*o β) α β

Full source

instance : OrderHomClass (α →+*o β) α β where
  map_rel f _ _ h := f.monotone' h

Monotone Semiring Homomorphisms Preserve Order

Informal description

For any two (semi)rings $\alpha$ and $\beta$ equipped with preorders, the type $\alpha \to+*o \beta$ of monotone semiring homomorphisms forms an `OrderHomClass`. This means that every element $f \in \alpha \to+*o \beta$ is an order-preserving map, i.e., for any $x, y \in \alpha$, if $x \leq y$ then $f(x) \leq f(y)$.

OrderRingHom.instRingHomClass instance

: RingHomClass (α →+*o β) α β

Full source

instance : RingHomClass (α →+*o β) α β where
  map_mul f := f.map_mul'
  map_one f := f.map_one'
  map_add f := f.map_add'
  map_zero f := f.map_zero'

Monotone Semiring Homomorphisms as Ring Homomorphisms

Informal description

For any two preordered semirings $\alpha$ and $\beta$, the type $\alpha \to+*o \beta$ of monotone semiring homomorphisms forms a `RingHomClass`. This means that every element $f \in \alpha \to+*o \beta$ is a semiring homomorphism, preserving addition, multiplication, and the multiplicative identity.

OrderRingHom.toFun_eq_coe theorem

(f : α →+*o β) : f.toFun = f

Full source

theorem toFun_eq_coe (f : α →+*o β) : f.toFun = f :=
  rfl

Underlying function equals coercion for monotone semiring homomorphisms

Informal description

For any monotone semiring homomorphism $f : \alpha \to+*o \beta$, the underlying function $f$ is equal to its coercion to a function.

OrderRingHom.ext theorem

{f g : α →+*o β} (h : ∀ a, f a = g a) : f = g

Full source

@[ext]
theorem ext {f g : α →+*o β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

Extensionality of Monotone Semiring Homomorphisms

Informal description

Let $f, g : \alpha \to+*o \beta$ be two monotone semiring homomorphisms between preordered semirings. If $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

OrderRingHom.toRingHom_eq_coe theorem

(f : α →+*o β) : f.toRingHom = f

Full source

@[simp]
theorem toRingHom_eq_coe (f : α →+*o β) : f.toRingHom = f :=
  RingHom.ext fun _ => rfl

Underlying Ring Homomorphism Equals Coercion for Monotone Semiring Homomorphisms

Informal description

For any monotone semiring homomorphism $f \colon \alpha \to+*o \beta$ between preordered semirings, the underlying ring homomorphism $f.toRingHom$ is equal to $f$ when viewed as a function.

OrderRingHom.toOrderAddMonoidHom_eq_coe theorem

(f : α →+*o β) : f.toOrderAddMonoidHom = f

Full source

@[simp]
theorem toOrderAddMonoidHom_eq_coe (f : α →+*o β) : f.toOrderAddMonoidHom = f :=
  rfl

Monotone Semiring Homomorphism as Additive Monoid Homomorphism

Informal description

For any monotone semiring homomorphism $f \colon \alpha \to+*o \beta$ between preordered semirings, the underlying monotone additive monoid homomorphism obtained from $f$ is equal to $f$ itself when viewed as a function.

OrderRingHom.toOrderMonoidWithZeroHom_eq_coe theorem

(f : α →+*o β) : f.toOrderMonoidWithZeroHom = f

Full source

@[simp]
theorem toOrderMonoidWithZeroHom_eq_coe (f : α →+*o β) : f.toOrderMonoidWithZeroHom = f :=
  rfl

Equality of Monotone Semiring Homomorphism and its Monoid With Zero Homomorphism

Informal description

For any monotone semiring homomorphism $f : \alpha \to+*o \beta$ between preordered semirings, the underlying function of the induced monotone monoid with zero homomorphism $f.toOrderMonoidWithZeroHom$ is equal to $f$ itself.

OrderRingHom.coe_coe_ringHom theorem

(f : α →+*o β) : ⇑(f : α →+* β) = f

Full source

@[simp]
theorem coe_coe_ringHom (f : α →+*o β) : ⇑(f : α →+* β) = f :=
  rfl

Coercion of Monotone Semiring Homomorphism to Semiring Homomorphism

Informal description

For any monotone semiring homomorphism $f : \alpha \to+*o \beta$, the underlying function of $f$ as a semiring homomorphism (i.e., when viewed as an element of $\alpha \to+* \beta$) is equal to $f$ itself.

OrderRingHom.coe_coe_orderAddMonoidHom theorem

(f : α →+*o β) : ⇑(f : α →+o β) = f

Full source

@[simp]
theorem coe_coe_orderAddMonoidHom (f : α →+*o β) : ⇑(f : α →+o β) = f :=
  rfl

Coercion of Monotone Semiring Homomorphism to Monotone Additive Homomorphism Preserves Function

Informal description

For any monotone semiring homomorphism $f : \alpha \to+*o \beta$ between preordered semirings $\alpha$ and $\beta$, the underlying function of $f$ when viewed as a monotone additive monoid homomorphism (i.e., as an element of $\alpha \to+o \beta$) coincides with $f$ itself.

OrderRingHom.coe_coe_orderMonoidWithZeroHom theorem

(f : α →+*o β) : ⇑(f : α →*₀o β) = f

Full source

@[simp]
theorem coe_coe_orderMonoidWithZeroHom (f : α →+*o β) : ⇑(f : α →*₀o β) = f :=
  rfl

Equality of Underlying Functions in Monotone Semiring and Monoid with Zero Homomorphisms

Informal description

For any monotone semiring homomorphism $f \colon \alpha \to+*o \beta$, the underlying function of $f$ when viewed as a monotone monoid with zero homomorphism (i.e., as an element of $\alpha \to*₀o \beta$) is equal to $f$ itself.

OrderRingHom.coe_ringHom_apply theorem

(f : α →+*o β) (a : α) : (f : α →+* β) a = f a

Full source

@[norm_cast]
theorem coe_ringHom_apply (f : α →+*o β) (a : α) : (f : α →+* β) a = f a :=
  rfl

Evaluation of Monotone Semiring Homomorphism as Semiring Homomorphism

Informal description

For any monotone semiring homomorphism $f \colon \alpha \to+*o \beta$ and any element $a \in \alpha$, the evaluation of $f$ as a semiring homomorphism at $a$ is equal to $f(a)$.

OrderRingHom.coe_orderAddMonoidHom_apply theorem

(f : α →+*o β) (a : α) : (f : α →+o β) a = f a

Full source

@[norm_cast]
theorem coe_orderAddMonoidHom_apply (f : α →+*o β) (a : α) : (f : α →+o β) a = f a :=
  rfl

Equality of Monotone Semiring Homomorphism and its Additive Monoid Homomorphism Component

Informal description

For any monotone semiring homomorphism $f : \alpha \to+*o \beta$ and any element $a \in \alpha$, the application of $f$ as an order-preserving additive monoid homomorphism to $a$ is equal to the direct application of $f$ to $a$, i.e., $(f : \alpha \to+o \beta)(a) = f(a)$.

OrderRingHom.coe_orderMonoidWithZeroHom_apply theorem

(f : α →+*o β) (a : α) : (f : α →*₀o β) a = f a

Full source

@[norm_cast]
theorem coe_orderMonoidWithZeroHom_apply (f : α →+*o β) (a : α) : (f : α →*₀o β) a = f a :=
  rfl

Evaluation of Monotone Semiring Homomorphism as Order-Preserving Monoid-with-Zero Homomorphism

Informal description

For any monotone semiring homomorphism $f \colon \alpha \to+*o \beta$ and any element $a \in \alpha$, the evaluation of $f$ as an order-preserving monoid-with-zero homomorphism at $a$ is equal to $f(a)$.

OrderRingHom.copy definition

(f : α →+*o β) (f' : α → β) (h : f' = f) : α →+*o β

Full source

/-- Copy of an `OrderRingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : α →+*o β) (f' : α → β) (h : f' = f) : α →+*o β :=
  { f.toRingHom.copy f' h, f.toOrderAddMonoidHom.copy f' h with }

Copy of a monotone semiring homomorphism with a new function

Informal description

Given a monotone semiring homomorphism $ f : \alpha \to+*o \beta $ and a function $ f' : \alpha \to \beta $ that is definitionally equal to $ f $, this function constructs a new monotone semiring homomorphism with $ f' $ as its underlying function. This is useful for fixing definitional equalities while preserving the structure of $ f $.

OrderRingHom.coe_copy theorem

(f : α →+*o β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f'

Full source

@[simp]
theorem coe_copy (f : α →+*o β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl

Underlying function of copied monotone semiring homomorphism equals copied function

Informal description

Let $f : \alpha \to+*o \beta$ be a monotone semiring homomorphism between preordered semirings $\alpha$ and $\beta$, and let $f' : \alpha \to \beta$ be a function such that $f' = f$. Then the underlying function of the copied homomorphism $f.copy\ f'\ h$ is equal to $f'$.

OrderRingHom.copy_eq theorem

(f : α →+*o β) (f' : α → β) (h : f' = f) : f.copy f' h = f

Full source

theorem copy_eq (f : α →+*o β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

Copy of Monotone Semiring Homomorphism Equals Original

Informal description

Let $f : \alpha \to+*o \beta$ be a monotone semiring homomorphism between preordered semirings $\alpha$ and $\beta$, and let $f' : \alpha \to \beta$ be a function such that $f' = f$. Then the copy of $f$ with underlying function $f'$ is equal to $f$ itself, i.e., $f.\text{copy}\, f'\, h = f$.

OrderRingHom.id definition

: α →+*o α

Full source

/-- The identity as an ordered ring homomorphism. -/
protected def id : α →+*o α :=
  { RingHom.id _, OrderHom.id with }

Identity ordered ring homomorphism

Informal description

The identity function on a preordered semiring $\alpha$, viewed as a bundled monotone semiring homomorphism from $\alpha$ to itself. That is, the function $\operatorname{id} : \alpha \to \alpha$ together with the proofs that it preserves the semiring structure (addition, multiplication, and multiplicative identity) and is monotone (i.e., $x \leq y$ implies $\operatorname{id}(x) \leq \operatorname{id}(y)$ for all $x, y \in \alpha$).

OrderRingHom.instInhabited instance

: Inhabited (α →+*o α)

Full source

instance : Inhabited (α →+*o α) :=
  ⟨OrderRingHom.id α⟩

Inhabited Type of Monotone Semiring Endomorphisms

Informal description

For any preordered semiring $\alpha$, the type of monotone semiring homomorphisms from $\alpha$ to itself is inhabited, with the identity function as a canonical element.

OrderRingHom.coe_id theorem

: ⇑(OrderRingHom.id α) = id

Full source

@[simp, norm_cast]
theorem coe_id : ⇑(OrderRingHom.id α) = id :=
  rfl

Identity Ordered Ring Homomorphism as Identity Function

Informal description

The underlying function of the identity ordered ring homomorphism on a preordered semiring $\alpha$ is equal to the identity function on $\alpha$.

OrderRingHom.id_apply theorem

(a : α) : OrderRingHom.id α a = a

Full source

@[simp]
theorem id_apply (a : α) : OrderRingHom.id α a = a :=
  rfl

Identity Ordered Ring Homomorphism Acts as Identity Function

Informal description

For any element $a$ in a preordered semiring $\alpha$, the identity ordered ring homomorphism evaluated at $a$ is equal to $a$, i.e., $\operatorname{id}(a) = a$.

OrderRingHom.coe_ringHom_id theorem

: (OrderRingHom.id α : α →+* α) = RingHom.id α

Full source

@[simp]
theorem coe_ringHom_id : (OrderRingHom.id α : α →+* α) = RingHom.id α :=
  rfl

Identity Ordered Ring Homomorphism as Identity Semiring Homomorphism

Informal description

The underlying semiring homomorphism of the identity ordered ring homomorphism on a preordered semiring $\alpha$ is equal to the identity semiring homomorphism on $\alpha$.

OrderRingHom.coe_orderAddMonoidHom_id theorem

: (OrderRingHom.id α : α →+o α) = OrderAddMonoidHom.id α

Full source

@[simp]
theorem coe_orderAddMonoidHom_id : (OrderRingHom.id α : α →+o α) = OrderAddMonoidHom.id α :=
  rfl

Identity Ordered Ring Homomorphism as Ordered Additive Monoid Homomorphism

Informal description

The identity ordered ring homomorphism on a preordered semiring $\alpha$, when viewed as an ordered additive monoid homomorphism, is equal to the identity ordered additive monoid homomorphism on $\alpha$.

OrderRingHom.coe_orderMonoidWithZeroHom_id theorem

: (OrderRingHom.id α : α →*₀o α) = OrderMonoidWithZeroHom.id α

Full source

@[simp]
theorem coe_orderMonoidWithZeroHom_id :
    (OrderRingHom.id α : α →*₀o α) = OrderMonoidWithZeroHom.id α :=
  rfl

Identity Ordered Ring Homomorphism as Ordered Monoid with Zero Homomorphism

Informal description

The identity ordered ring homomorphism on a preordered semiring $\alpha$, when viewed as an ordered monoid with zero homomorphism, is equal to the identity ordered monoid with zero homomorphism on $\alpha$.

OrderRingHom.comp definition

(f : β →+*o γ) (g : α →+*o β) : α →+*o γ

Full source

/-- Composition of two `OrderRingHom`s as an `OrderRingHom`. -/
protected def comp (f : β →+*o γ) (g : α →+*o β) : α →+*o γ :=
  { f.toRingHom.comp g.toRingHom, f.toOrderAddMonoidHom.comp g.toOrderAddMonoidHom with }

Composition of monotone semiring homomorphisms

Informal description

The composition of two monotone semiring homomorphisms $ f : \beta \to+*o \gamma $ and $ g : \alpha \to+*o \beta $ is a monotone semiring homomorphism $ \alpha \to+*o \gamma $. This composition preserves both the ring structure and the order relation.

OrderRingHom.coe_comp theorem

(f : β →+*o γ) (g : α →+*o β) : ⇑(f.comp g) = f ∘ g

Full source

@[simp]
theorem coe_comp (f : β →+*o γ) (g : α →+*o β) : ⇑(f.comp g) = f ∘ g :=
  rfl

Composition of Monotone Semiring Homomorphisms Preserves Underlying Function

Informal description

For any monotone semiring homomorphisms $ f : \beta \to+*o \gamma $ and $ g : \alpha \to+*o \beta $, the underlying function of the composition $ f \circ g $ is equal to the composition of the underlying functions $ f \circ g $.

OrderRingHom.comp_apply theorem

(f : β →+*o γ) (g : α →+*o β) (a : α) : f.comp g a = f (g a)

Full source

@[simp]
theorem comp_apply (f : β →+*o γ) (g : α →+*o β) (a : α) : f.comp g a = f (g a) :=
  rfl

Composition of Monotone Semiring Homomorphisms Evaluates Pointwise

Informal description

For any monotone semiring homomorphisms $ f \colon \beta \to+*o \gamma $ and $ g \colon \alpha \to+*o \beta $, and any element $ a \in \alpha $, the composition $ f \circ g $ evaluated at $ a $ equals $ f(g(a)) $. That is, $ (f \circ g)(a) = f(g(a)) $.

OrderRingHom.comp_assoc theorem

(f : γ →+*o δ) (g : β →+*o γ) (h : α →+*o β) : (f.comp g).comp h = f.comp (g.comp h)

Full source

theorem comp_assoc (f : γ →+*o δ) (g : β →+*o γ) (h : α →+*o β) :
    (f.comp g).comp h = f.comp (g.comp h) :=
  rfl

Associativity of Composition for Monotone Semiring Homomorphisms

Informal description

Given monotone semiring homomorphisms $f \colon \gamma \to+*o \delta$, $g \colon \beta \to+*o \gamma$, and $h \colon \alpha \to+*o \beta$, the composition operation satisfies the associativity property $(f \circ g) \circ h = f \circ (g \circ h)$.

OrderRingHom.comp_id theorem

(f : α →+*o β) : f.comp (OrderRingHom.id α) = f

Full source

@[simp]
theorem comp_id (f : α →+*o β) : f.comp (OrderRingHom.id α) = f :=
  rfl

Composition with Identity Preserves Monotone Semiring Homomorphism

Informal description

For any monotone semiring homomorphism $f \colon \alpha \to+*o \beta$, the composition of $f$ with the identity ordered ring homomorphism on $\alpha$ is equal to $f$ itself, i.e., $f \circ \mathrm{id} = f$.

OrderRingHom.id_comp theorem

(f : α →+*o β) : (OrderRingHom.id β).comp f = f

Full source

@[simp]
theorem id_comp (f : α →+*o β) : (OrderRingHom.id β).comp f = f :=
  rfl

Left Identity Law for Composition of Monotone Semiring Homomorphisms

Informal description

For any monotone semiring homomorphism $f \colon \alpha \to+*o \beta$, the composition of the identity homomorphism on $\beta$ with $f$ is equal to $f$.

OrderRingHom.cancel_right theorem

{f₁ f₂ : β →+*o γ} {g : α →+*o β} (hg : Surjective g) : f₁.comp g = f₂.comp g ↔ f₁ = f₂

Full source

@[simp]
theorem cancel_right {f₁ f₂ : β →+*o γ} {g : α →+*o β} (hg : Surjective g) :
    f₁.comp g = f₂.comp g ↔ f₁ = f₂ :=
  ⟨fun h => ext <| hg.forall.2 <| DFunLike.ext_iff.1 h, fun h => by rw [h]⟩

Right Cancellation Property for Composition of Monotone Semiring Homomorphisms

Informal description

Let $f₁, f₂ \colon \beta \to+*o \gamma$ be two monotone semiring homomorphisms, and let $g \colon \alpha \to+*o \beta$ be a surjective monotone semiring homomorphism. Then the compositions $f₁ \circ g$ and $f₂ \circ g$ are equal if and only if $f₁ = f₂$.

OrderRingHom.cancel_left theorem

{f : β →+*o γ} {g₁ g₂ : α →+*o β} (hf : Injective f) : f.comp g₁ = f.comp g₂ ↔ g₁ = g₂

Full source

@[simp]
theorem cancel_left {f : β →+*o γ} {g₁ g₂ : α →+*o β} (hf : Injective f) :
    f.comp g₁ = f.comp g₂ ↔ g₁ = g₂ :=
  ⟨fun h => ext fun a => hf <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Left Cancellation Property for Composition of Monotone Semiring Homomorphisms

Informal description

Let $f \colon \beta \to+*o \gamma$ be an injective monotone semiring homomorphism, and let $g_1, g_2 \colon \alpha \to+*o \beta$ be two monotone semiring homomorphisms. Then the compositions $f \circ g_1$ and $f \circ g_2$ are equal if and only if $g_1 = g_2$.

OrderRingHom.instPreorder instance

[Preorder β] : Preorder (OrderRingHom α β)

Full source

instance [Preorder β] : Preorder (OrderRingHom α β) :=
  Preorder.lift ((⇑) : _ → α → β)

Pointwise Preorder on Monotone Semiring Homomorphisms

Informal description

For any two (semi)rings $\alpha$ and $\beta$ where $\beta$ is equipped with a preorder, the type $\alpha \to+*o \beta$ of monotone semiring homomorphisms has a canonical preorder structure. This order is defined pointwise: for any $f, g \in \alpha \to+*o \beta$, we have $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x \in \alpha$.

OrderRingHom.instPartialOrder instance

[PartialOrder β] : PartialOrder (OrderRingHom α β)

Full source

instance [PartialOrder β] : PartialOrder (OrderRingHom α β) :=
  PartialOrder.lift _ DFunLike.coe_injective

Pointwise Partial Order on Monotone Semiring Homomorphisms

Informal description

For any two (semi)rings $\alpha$ and $\beta$ where $\beta$ is equipped with a partial order, the type $\alpha \to+*o \beta$ of monotone semiring homomorphisms has a canonical partial order structure. This order is defined pointwise: for any $f, g \in \alpha \to+*o \beta$, we have $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x \in \alpha$.

OrderRingIso.toOrderIso definition

(f : α ≃+*o β) : α ≃o β

Full source

/-- Reinterpret an ordered ring isomorphism as an order isomorphism. -/
@[coe]
def toOrderIso (f : α ≃+*o β) : α ≃o β :=
  ⟨f.toRingEquiv.toEquiv, f.map_le_map_iff'⟩

Order isomorphism underlying an order-preserving semiring isomorphism

Informal description

Given an order-preserving semiring isomorphism $f : \alpha \simeq_{+*o} \beta$, the function returns the underlying order isomorphism $\alpha \simeq_o \beta$, which consists of the bijection from $f$ and the proof that $f$ preserves the order relation in both directions.

OrderRingIso.instEquivLike instance

: EquivLike (α ≃+*o β) α β

Full source

instance : EquivLike (α ≃+*o β) α β where
  coe f := f.toFun
  inv f := f.invFun
  coe_injective' f g h₁ h₂ := by
    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
    congr
  left_inv f := f.left_inv
  right_inv f := f.right_inv

Order-Preserving Semiring Isomorphisms as Equivalences

Informal description

For any ordered semirings $\alpha$ and $\beta$, the type $\alpha \simeq_{+*o} \beta$ of order-preserving semiring isomorphisms can be injectively coerced to bijections between $\alpha$ and $\beta$.

OrderRingIso.instOrderIsoClass instance

: OrderIsoClass (α ≃+*o β) α β

Full source

instance : OrderIsoClass (α ≃+*o β) α β where
  map_le_map_iff f _ _ := f.map_le_map_iff'

Order-Preserving Semiring Isomorphisms as Order Isomorphisms

Informal description

For any ordered semirings $\alpha$ and $\beta$, the type $\alpha \simeq_{+*o} \beta$ of order-preserving semiring isomorphisms forms a class of order isomorphisms between $\alpha$ and $\beta$.

OrderRingIso.instRingEquivClass instance

: RingEquivClass (α ≃+*o β) α β

Full source

instance : RingEquivClass (α ≃+*o β) α β where
  map_mul f := f.map_mul'
  map_add f := f.map_add'

Order-Preserving Semiring Isomorphisms as Ring Equivalences

Informal description

For any ordered semirings $\alpha$ and $\beta$, the type $\alpha \simeq_{+*o} \beta$ of order-preserving semiring isomorphisms forms a class of ring equivalences between $\alpha$ and $\beta$.

OrderRingIso.toFun_eq_coe theorem

(f : α ≃+*o β) : f.toFun = f

Full source

theorem toFun_eq_coe (f : α ≃+*o β) : f.toFun = f :=
  rfl

Underlying Function of Order-Preserving Semiring Isomorphism

Informal description

For any order-preserving semiring isomorphism $f : \alpha \simeq_{+*o} \beta$, the underlying function $f.\text{toFun}$ is equal to $f$ itself.

OrderRingIso.ext theorem

{f g : α ≃+*o β} (h : ∀ a, f a = g a) : f = g

Full source

@[ext]
theorem ext {f g : α ≃+*o β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

Extensionality of Order-Preserving Semiring Isomorphisms

Informal description

For any two order-preserving semiring isomorphisms $f, g : \alpha \simeq_{+*o} \beta$, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

OrderRingIso.coe_mk theorem

(e : α ≃+* β) (h) : ⇑(⟨e, h⟩ : α ≃+*o β) = e

Full source

@[simp]
theorem coe_mk (e : α ≃+* β) (h) : ⇑(⟨e, h⟩ : α ≃+*o β) = e :=
  rfl

Coercion of Order-Preserving Semiring Isomorphism Construction

Informal description

Given a semiring isomorphism $e : \alpha \simeq_{+*} \beta$ and a proof $h$ that $e$ is order-preserving, the underlying function of the order-preserving semiring isomorphism $\langle e, h \rangle : \alpha \simeq_{+*o} \beta$ is equal to $e$.

OrderRingIso.mk_coe theorem

(e : α ≃+*o β) (h) : (⟨e, h⟩ : α ≃+*o β) = e

Full source

@[simp]
theorem mk_coe (e : α ≃+*o β) (h) : (⟨e, h⟩ : α ≃+*o β) = e :=
  ext fun _ => rfl

Construction of Order-Preserving Semiring Isomorphism Yields Original Isomorphism

Informal description

Given an order-preserving semiring isomorphism $e : \alpha \simeq_{+*o} \beta$ and a proof $h$ that $e$ is order-preserving, the constructed isomorphism $\langle e, h \rangle$ is equal to $e$ itself.

OrderRingIso.toRingEquiv_eq_coe theorem

(f : α ≃+*o β) : f.toRingEquiv = f

Full source

@[simp]
theorem toRingEquiv_eq_coe (f : α ≃+*o β) : f.toRingEquiv = f :=
  RingEquiv.ext fun _ => rfl

Equality of Order-Preserving Semiring Isomorphism and its Underlying Ring Equivalence

Informal description

For any order-preserving semiring isomorphism $f : \alpha \simeq_{+*o} \beta$, the underlying semiring isomorphism $f.\text{toRingEquiv}$ is equal to $f$ itself.

OrderRingIso.toOrderIso_eq_coe theorem

(f : α ≃+*o β) : f.toOrderIso = f

Full source

@[simp]
theorem toOrderIso_eq_coe (f : α ≃+*o β) : f.toOrderIso = f :=
  OrderIso.ext rfl

Equality of Order-Preserving Semiring Isomorphism and its Underlying Order Isomorphism

Informal description

For any order-preserving semiring isomorphism $f : \alpha \simeq_{+*o} \beta$, the underlying order isomorphism $f.\text{toOrderIso}$ is equal to $f$ itself.

OrderRingIso.coe_toRingEquiv theorem

(f : α ≃+*o β) : ⇑(f : α ≃+* β) = f

Full source

@[simp, norm_cast]
theorem coe_toRingEquiv (f : α ≃+*o β) : ⇑(f : α ≃+* β) = f :=
  rfl

Underlying Function of Order-Preserving Semiring Isomorphism Matches the Isomorphism Itself

Informal description

For any order-preserving semiring isomorphism $f : \alpha \simeq_{+*o} \beta$, the underlying function of the corresponding ring equivalence $f : \alpha \simeq_{+*} \beta$ is equal to $f$ itself.

OrderRingIso.coe_toOrderIso theorem

(f : α ≃+*o β) : DFunLike.coe (f : α ≃o β) = f

Full source

@[simp, norm_cast]
theorem coe_toOrderIso (f : α ≃+*o β) : DFunLike.coe (f : α ≃o β) = f :=
  rfl

Coercion of Order-Preserving Semiring Isomorphism to Order Isomorphism Preserves Function

Informal description

For any order-preserving semiring isomorphism $f : \alpha \simeq_{+*o} \beta$, the underlying function of $f$ viewed as an order isomorphism (via `f.toOrderIso`) coincides with $f$ itself.

OrderRingIso.refl definition

: α ≃+*o α

Full source

/-- The identity map as an ordered ring isomorphism. -/
@[refl]
protected def refl : α ≃+*o α :=
  ⟨RingEquiv.refl α, Iff.rfl⟩

Identity ordered semiring isomorphism

Informal description

The identity map on an ordered semiring $\alpha$, viewed as an order-preserving semiring isomorphism from $\alpha$ to itself.

OrderRingIso.instInhabited instance

: Inhabited (α ≃+*o α)

Full source

instance : Inhabited (α ≃+*o α) :=
  ⟨OrderRingIso.refl α⟩

Inhabited Type of Order-Preserving Semiring Isomorphisms

Informal description

For any ordered semiring $\alpha$, the type of order-preserving semiring isomorphisms $\alpha \simeq_{+*o} \alpha$ is inhabited, with the identity map as a canonical element.

OrderRingIso.refl_apply theorem

(x : α) : OrderRingIso.refl α x = x

Full source

@[simp]
theorem refl_apply (x : α) : OrderRingIso.refl α x = x := by
  rfl

Identity Order-Preserving Semiring Isomorphism Maps Element to Itself

Informal description

For any element $x$ in an ordered semiring $\alpha$, the identity order-preserving semiring isomorphism $\text{refl}_\alpha$ maps $x$ to itself, i.e., $\text{refl}_\alpha(x) = x$.

OrderRingIso.coe_ringEquiv_refl theorem

: (OrderRingIso.refl α : α ≃+* α) = RingEquiv.refl α

Full source

@[simp]
theorem coe_ringEquiv_refl : (OrderRingIso.refl α : α ≃+* α) = RingEquiv.refl α :=
  rfl

Identity Order-Preserving Semiring Isomorphism as Identity Semiring Equivalence

Informal description

The underlying semiring equivalence of the identity order-preserving semiring isomorphism $\text{refl}_\alpha$ is equal to the identity semiring equivalence on $\alpha$.

OrderRingIso.coe_orderIso_refl theorem

: (OrderRingIso.refl α : α ≃o α) = OrderIso.refl α

Full source

@[simp]
theorem coe_orderIso_refl : (OrderRingIso.refl α : α ≃o α) = OrderIso.refl α :=
  rfl

Identity Ordered Semiring Isomorphism as Identity Order Isomorphism

Informal description

The underlying order isomorphism of the identity ordered semiring isomorphism $\text{refl}_\alpha : \alpha \simeq_{+*o} \alpha$ is equal to the identity order isomorphism $\text{refl}_\alpha : \alpha \simeq_o \alpha$.

OrderRingIso.symm definition

(e : α ≃+*o β) : β ≃+*o α

Full source

/-- The inverse of an ordered ring isomorphism as an ordered ring isomorphism. -/
@[symm]
protected def symm (e : α ≃+*o β) : β ≃+*o α :=
  ⟨e.toRingEquiv.symm, by
    intro a b
    erw [← map_le_map_iff e, e.1.apply_symm_apply, e.1.apply_symm_apply]⟩

Inverse of an ordered ring isomorphism

Informal description

Given an ordered ring isomorphism $e : \alpha \simeq_{+*o} \beta$, the inverse function $e^{-1} : \beta \simeq_{+*o} \alpha$ is also an ordered ring isomorphism. This means $e^{-1}$ preserves both the ring structure and the order relation.

OrderRingIso.Simps.symm_apply definition

(e : α ≃+*o β) : β → α

Full source

/-- See Note [custom simps projection] -/
def Simps.symm_apply (e : α ≃+*o β) : β → α :=
  e.symm

Inverse map of an order-preserving semiring isomorphism

Informal description

For an order-preserving semiring isomorphism $e : \alpha \simeq_{+*o} \beta$, the function maps an element $y \in \beta$ to its preimage $e^{-1}(y) \in \alpha$ under the isomorphism.

OrderRingIso.symm_symm theorem

(e : α ≃+*o β) : e.symm.symm = e

Full source

@[simp]
theorem symm_symm (e : α ≃+*o β) : e.symm.symm = e := rfl

Double Inverse of Order-Preserving Semiring Isomorphism

Informal description

For any order-preserving semiring isomorphism $e : \alpha \simeq_{+*o} \beta$, the double inverse $e^{-1^{-1}}$ equals $e$ itself, i.e., $(e^{-1})^{-1} = e$.

OrderRingIso.symm_bijective theorem

: Bijective (OrderRingIso.symm : (α ≃+*o β) → β ≃+*o α)

Full source

theorem symm_bijective : Bijective (OrderRingIso.symm : (α ≃+*o β) → β ≃+*o α) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Operation on Order-Preserving Semiring Isomorphisms

Informal description

The inverse operation on order-preserving semiring isomorphisms, which maps an isomorphism $e : \alpha \simeq_{+*o} \beta$ to its inverse $e^{-1} : \beta \simeq_{+*o} \alpha$, is a bijective function. That is, it is both injective (distinct isomorphisms have distinct inverses) and surjective (every order-preserving semiring isomorphism from $\beta$ to $\alpha$ is the inverse of some isomorphism from $\alpha$ to $\beta$).

OrderRingIso.trans definition

(f : α ≃+*o β) (g : β ≃+*o γ) : α ≃+*o γ

Full source

/-- Composition of `OrderRingIso`s as an `OrderRingIso`. -/
@[trans]
protected def trans (f : α ≃+*o β) (g : β ≃+*o γ) : α ≃+*o γ :=
  ⟨f.toRingEquiv.trans g.toRingEquiv, (map_le_map_iff g).trans (map_le_map_iff f)⟩

Composition of order-preserving semiring isomorphisms

Informal description

The composition of two order-preserving semiring isomorphisms $f : \alpha \simeq_{+*o} \beta$ and $g : \beta \simeq_{+*o} \gamma$ is an order-preserving semiring isomorphism $\alpha \simeq_{+*o} \gamma$, where the underlying ring isomorphism is the composition of the underlying ring isomorphisms of $f$ and $g$, and the order-preserving property is preserved under composition.

OrderRingIso.trans_toRingEquiv theorem

 (f : α ≃+*o β) (g : β ≃+*o γ) : (OrderRingIso.trans f g).toRingEquiv = RingEquiv.trans f.toRingEquiv g.toRingEquiv

Full source

/-- This lemma used to be generated by [simps] on `trans`, but the lhs of this simplifies under
simp. Removed [simps] attribute and added aux version below. -/
theorem trans_toRingEquiv (f : α ≃+*o β) (g : β ≃+*o γ) :
    (OrderRingIso.trans f g).toRingEquiv = RingEquiv.trans f.toRingEquiv g.toRingEquiv :=
  rfl

Composition of Order-Preserving Isomorphisms Preserves Ring Equivalence

Informal description

For any order-preserving semiring isomorphisms $f : \alpha \simeq_{+*o} \beta$ and $g : \beta \simeq_{+*o} \gamma$, the underlying ring equivalence of their composition $f \circ g$ is equal to the composition of their underlying ring equivalences, i.e., $(f \circ g).\text{toRingEquiv} = f.\text{toRingEquiv} \circ g.\text{toRingEquiv}$.

OrderRingIso.trans_toRingEquiv_aux theorem

 (f : α ≃+*o β) (g : β ≃+*o γ) :
  RingEquivClass.toRingEquiv (OrderRingIso.trans f g) = RingEquiv.trans f.toRingEquiv g.toRingEquiv

Full source

/-- `simp`-normal form of `trans_toRingEquiv`. -/
@[simp]
theorem trans_toRingEquiv_aux (f : α ≃+*o β) (g : β ≃+*o γ) :
    RingEquivClass.toRingEquiv (OrderRingIso.trans f g)
      = RingEquiv.trans f.toRingEquiv g.toRingEquiv :=
  rfl

Composition of Order-Preserving Isomorphisms Preserves Ring Equivalence Structure

Informal description

For any order-preserving semiring isomorphisms $f \colon \alpha \simeq_{+*o} \beta$ and $g \colon \beta \simeq_{+*o} \gamma$, the underlying ring equivalence of their composition $f \circ g$ is equal to the composition of their underlying ring equivalences, i.e., \[ \text{RingEquivClass.toRingEquiv}(f \circ g) = \text{RingEquiv.trans}(f.\text{toRingEquiv}, g.\text{toRingEquiv}). \]

OrderRingIso.trans_apply theorem

(f : α ≃+*o β) (g : β ≃+*o γ) (a : α) : f.trans g a = g (f a)

Full source

@[simp]
theorem trans_apply (f : α ≃+*o β) (g : β ≃+*o γ) (a : α) : f.trans g a = g (f a) :=
  rfl

Composition of Order-Preserving Isomorphisms Evaluates as Function Composition

Informal description

For any order-preserving semiring isomorphisms $f \colon \alpha \simeq_{+*o} \beta$ and $g \colon \beta \simeq_{+*o} \gamma$, and any element $a \in \alpha$, the composition $(f \circ g)(a)$ equals $g(f(a))$.

OrderRingIso.self_trans_symm theorem

(e : α ≃+*o β) : e.trans e.symm = OrderRingIso.refl α

Full source

@[simp]
theorem self_trans_symm (e : α ≃+*o β) : e.trans e.symm = OrderRingIso.refl α :=
  ext e.left_inv

Composition of an Order-Preserving Isomorphism with its Inverse Yields the Identity

Informal description

For any order-preserving semiring isomorphism $e \colon \alpha \simeq_{+*o} \beta$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity isomorphism on $\alpha$, i.e., $e \circ e^{-1} = \text{id}_\alpha$.

OrderRingIso.symm_trans_self theorem

(e : α ≃+*o β) : e.symm.trans e = OrderRingIso.refl β

Full source

@[simp]
theorem symm_trans_self (e : α ≃+*o β) : e.symm.trans e = OrderRingIso.refl β :=
  ext e.right_inv

Inverse-Identity Composition for Order-Preserving Semiring Isomorphisms

Informal description

For any order-preserving semiring isomorphism $e \colon \alpha \simeq_{+*o} \beta$, the composition of its inverse $e^{-1}$ with $e$ itself equals the identity isomorphism on $\beta$, i.e., $e^{-1} \circ e = \text{id}_\beta$.

OrderRingIso.toOrderRingHom definition

(f : α ≃+*o β) : α →+*o β

Full source

/-- Reinterpret an ordered ring isomorphism as an ordered ring homomorphism. -/
def toOrderRingHom (f : α ≃+*o β) : α →+*o β :=
  ⟨f.toRingEquiv.toRingHom, fun _ _ => (map_le_map_iff f).2⟩

Ordered ring isomorphism as ordered ring homomorphism

Informal description

Given an order-preserving semiring isomorphism $f : \alpha \simeq_{+*o} \beta$, the function returns the corresponding monotone semiring homomorphism $\alpha \to_{+*o} \beta$ obtained by forgetting the inverse operation of $f$ while preserving both the ring structure and the order relation.

OrderRingIso.toOrderRingHom_eq_coe theorem

(f : α ≃+*o β) : f.toOrderRingHom = f

Full source

@[simp]
theorem toOrderRingHom_eq_coe (f : α ≃+*o β) : f.toOrderRingHom = f :=
  rfl

Ordered Ring Isomorphism Coincides with its Underlying Homomorphism

Informal description

For any order-preserving semiring isomorphism $f \colon \alpha \simeq_{+*o} \beta$, the underlying monotone semiring homomorphism $f \colon \alpha \to_{+*o} \beta$ is equal to $f$ itself when viewed as a function.

OrderRingIso.coe_toOrderRingHom theorem

(f : α ≃+*o β) : ⇑(f : α →+*o β) = f

Full source

@[simp, norm_cast]
theorem coe_toOrderRingHom (f : α ≃+*o β) : ⇑(f : α →+*o β) = f :=
  rfl

Underlying Function of Order-Preserving Semiring Isomorphism as Monotone Homomorphism

Informal description

For any order-preserving semiring isomorphism $f : \alpha \simeq_{+*o} \beta$, the underlying function of the corresponding monotone semiring homomorphism $f : \alpha \to_{+*o} \beta$ is equal to $f$ itself.

OrderRingIso.coe_toOrderRingHom_refl theorem

: (OrderRingIso.refl α : α →+*o α) = OrderRingHom.id α

Full source

@[simp]
theorem coe_toOrderRingHom_refl : (OrderRingIso.refl α : α →+*o α) = OrderRingHom.id α :=
  rfl

Identity Order-Preserving Semiring Isomorphism as Identity Monotone Semiring Homomorphism

Informal description

The identity order-preserving semiring isomorphism $\operatorname{refl} : \alpha \simeq_{+*o} \alpha$, when viewed as a monotone semiring homomorphism $\alpha \to_{+*o} \alpha$, coincides with the identity monotone semiring homomorphism $\operatorname{id} : \alpha \to_{+*o} \alpha$.

OrderRingIso.toOrderRingHom_injective theorem

: Injective (toOrderRingHom : α ≃+*o β → α →+*o β)

Full source

theorem toOrderRingHom_injective : Injective (toOrderRingHom : α ≃+*o β → α →+*o β) :=
  fun f g h => DFunLike.coe_injective <| by convert DFunLike.ext'_iff.1 h using 0

Injectivity of the Forgetful Map from Order-Preserving Semiring Isomorphisms to Monotone Semiring Homomorphisms

Informal description

The map from order-preserving semiring isomorphisms $\alpha \simeq_{+*o} \beta$ to monotone semiring homomorphisms $\alpha \to_{+*o} \beta$, given by forgetting the inverse operation, is injective. That is, if two order-preserving semiring isomorphisms $f, g : \alpha \simeq_{+*o} \beta$ satisfy $f = g$ as monotone semiring homomorphisms, then $f = g$ as isomorphisms.

Mathlib.Algebra.Order.Hom.Ring

Main definitions

Notation

Implementation notes

Tags