Mathlib.Algebra.Order.Hom.Monoid

OrderAddMonoidHom structure

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

Full source

/-- `α →+o β` is the type of monotone functions `α → β` that preserve the `OrderedAddCommMonoid`
structure.

`OrderAddMonoidHom` is also used for ordered group homomorphisms.

When possible, instead of parametrizing results over `(f : α →+o β)`,
you should parametrize over
`(F : Type*) [FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N] (f : F)`. -/
structure OrderAddMonoidHom (α β : Type*) [Preorder α] [Preorder β] [AddZeroClass α]
  [AddZeroClass β] extends α →+ β where
  /-- An `OrderAddMonoidHom` is a monotone function. -/
  monotone' : Monotone toFun

Ordered additive monoid homomorphism

Informal description

The structure `OrderAddMonoidHom` represents monotone additive monoid homomorphisms between two preordered additive monoids $\alpha$ and $\beta$. It extends the bundled additive monoid homomorphism $\alpha \to^+ \beta$ and additionally requires the function to be order-preserving (monotone).

term_→+o_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Infix notation for `OrderAddMonoidHom`. -/
infixr:25 " →+o " => OrderAddMonoidHom

Notation for ordered additive monoid homomorphisms

Informal description

The infix notation `→+o` represents the type of ordered additive monoid homomorphisms between two ordered additive monoids.

OrderAddMonoidIso structure

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

Full source

/-- `α ≃+o β` is the type of monotone isomorphisms `α ≃ β` that preserve the `OrderedAddCommMonoid`
structure.

`OrderAddMonoidIso` is also used for ordered group isomorphisms.

When possible, instead of parametrizing results over `(f : α ≃+o β)`,
you should parametrize over
`(F : Type*) [FunLike F M N] [AddEquivClass F M N] [OrderIsoClass F M N] (f : F)`. -/
structure OrderAddMonoidIso (α β : Type*) [Preorder α] [Preorder β] [Add α] [Add β]
  extends α ≃+ β where
  /-- An `OrderAddMonoidIso` respects `≤`. -/
  map_le_map_iff' {a b : α} : toFun a ≤ toFun b ↔ a ≤ b

Ordered additive monoid isomorphism

Informal description

The structure `OrderAddMonoidIso` represents an order-preserving isomorphism between two additive monoids $\alpha$ and $\beta$ with preorders. It extends the notion of an additive equivalence (`α ≃+ β`) by additionally requiring that the isomorphism is monotone, i.e., it preserves the order structure.

term_≃+o_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Infix notation for `OrderAddMonoidIso`. -/
infixr:25 " ≃+o " => OrderAddMonoidIso

Ordered additive monoid isomorphism notation

Informal description

The notation `≃+o` represents bundled ordered additive monoid isomorphisms, which are bijective maps preserving both the additive structure and the order between two ordered additive monoids.

OrderMonoidHom structure

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

Full source

/-- `α →*o β` is the type of functions `α → β` that preserve the `OrderedCommMonoid` structure.

`OrderMonoidHom` is also used for ordered group homomorphisms.

When possible, instead of parametrizing results over `(f : α →*o β)`,
you should parametrize over
`(F : Type*) [FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N] (f : F)`. -/
@[to_additive]
structure OrderMonoidHom (α β : Type*) [Preorder α] [Preorder β] [MulOneClass α]
  [MulOneClass β] extends α →* β where
  /-- An `OrderMonoidHom` is a monotone function. -/
  monotone' : Monotone toFun

Ordered Monoid Homomorphism

Informal description

The structure `OrderMonoidHom` represents ordered monoid homomorphisms between two preordered monoids $\alpha$ and $\beta$. It extends the notion of monoid homomorphisms (`α →* β`) by additionally preserving the order structure.

term_→*o_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Infix notation for `OrderMonoidHom`. -/
infixr:25 " →*o " => OrderMonoidHom

Ordered monoid homomorphism notation

Informal description

The notation `→*o` represents the type of ordered monoid homomorphisms between two preordered monoids. Specifically, for preordered monoids $\alpha$ and $\beta$, the notation $\alpha \rightarrow*o \beta$ denotes the type of homomorphisms from $\alpha$ to $\beta$ that preserve both the monoid structure and the order relation.

OrderMonoidHomClass.toOrderMonoidHom definition

[OrderHomClass F α β] [MonoidHomClass F α β] (f : F) : α →*o β

Full source

/-- Turn an element of a type `F` satisfying `OrderHomClass F α β` and `MonoidHomClass F α β`
into an actual `OrderMonoidHom`. This is declared as the default coercion from `F` to `α →*o β`. -/
@[to_additive (attr := coe)
  "Turn an element of a type `F` satisfying `OrderHomClass F α β` and `AddMonoidHomClass F α β`
  into an actual `OrderAddMonoidHom`.
  This is declared as the default coercion from `F` to `α →+o β`."]
def OrderMonoidHomClass.toOrderMonoidHom [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) :
    α →*o β :=
  { (f : α →* β) with monotone' := OrderHomClass.monotone f }

Conversion to Ordered Monoid Homomorphism

Informal description

Given a type `F` satisfying both `OrderHomClass F α β` (order-preserving morphisms) and `MonoidHomClass F α β` (monoid homomorphisms), the function converts an element `f : F` into an ordered monoid homomorphism from `α$ to $\beta$. This homomorphism preserves both the multiplicative structure and the order relation.

instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass instance

[OrderHomClass F α β] [MonoidHomClass F α β] : CoeTC F (α →*o β)

Full source

/-- Any type satisfying `OrderMonoidHomClass` can be cast into `OrderMonoidHom` via
  `OrderMonoidHomClass.toOrderMonoidHom`. -/
@[to_additive "Any type satisfying `OrderAddMonoidHomClass` can be cast into `OrderAddMonoidHom` via
  `OrderAddMonoidHomClass.toOrderAddMonoidHom`"]
instance [OrderHomClass F α β] [MonoidHomClass F α β] : CoeTC F (α →*o β) :=
  ⟨OrderMonoidHomClass.toOrderMonoidHom⟩

Coercion from Order-Preserving Monoid Homomorphism Classes to Ordered Monoid Homomorphisms

Informal description

For any type $F$ that satisfies both `OrderHomClass F α β` (order-preserving morphisms) and `MonoidHomClass F α β` (monoid homomorphisms), there is a canonical coercion from $F$ to the type of ordered monoid homomorphisms $\alpha \to^*o \beta$. This means any element $f : F$ can be treated as an ordered monoid homomorphism that preserves both the multiplicative structure and the order relation between $\alpha$ and $\beta$.

OrderMonoidIso structure

(α β : Type*) [Preorder α] [Preorder β] [Mul α] [Mul β]
  extends α ≃* β

Full source

/-- `α ≃*o β` is the type of isomorphisms `α ≃ β` that preserve the `OrderedCommMonoid` structure.

`OrderMonoidIso` is also used for ordered group isomorphisms.

When possible, instead of parametrizing results over `(f : α ≃*o β)`,
you should parametrize over
`(F : Type*) [FunLike F M N] [MulEquivClass F M N] [OrderIsoClass F M N] (f : F)`. -/
@[to_additive]
structure OrderMonoidIso (α β : Type*) [Preorder α] [Preorder β] [Mul α] [Mul β]
  extends α ≃* β where
  /-- An `OrderMonoidIso` respects `≤`. -/
  map_le_map_iff' {a b : α} : toFun a ≤ toFun b ↔ a ≤ b

Ordered Monoid Isomorphism

Informal description

The structure `OrderMonoidIso α β` represents order-preserving isomorphisms between two ordered monoids (or groups) $\alpha$ and $\beta$. It extends the notion of a multiplicative isomorphism (`MulEquiv`) by additionally requiring that the isomorphism preserves the order structure. An element of `OrderMonoidIso α β` is a bijection $f : \alpha \to \beta$ that satisfies: 1. $f$ is a monoid homomorphism (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ and $f(1) = 1$), 2. $f$ is order-preserving (i.e., $x \leq y \implies f(x) \leq f(y)$), 3. $f$ has an inverse $f^{-1}$ that is also a monoid homomorphism and order-preserving. This structure is also used for ordered group isomorphisms.

term_≃*o_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Infix notation for `OrderMonoidIso`. -/
infixr:25 " ≃*o " => OrderMonoidIso

Ordered monoid isomorphism notation (`≃*o`)

Informal description

The infix notation `≃*o` represents an order-preserving monoid isomorphism between two preordered monoids $\alpha$ and $\beta$. This notation is used to denote bundled ordered monoid isomorphisms, which are both order isomorphisms and monoid isomorphisms.

OrderMonoidIsoClass.toOrderMonoidIso definition

[EquivLike F α β] [OrderIsoClass F α β] [MulEquivClass F α β] (f : F) : α ≃*o β

Full source

/-- Turn an element of a type `F` satisfying `OrderIsoClass F α β` and `MulEquivClass F α β`
into an actual `OrderMonoidIso`. This is declared as the default coercion from `F` to `α ≃*o β`. -/
@[to_additive (attr := coe)
  "Turn an element of a type `F` satisfying `OrderIsoClass F α β` and `AddEquivClass F α β`
  into an actual `OrderAddMonoidIso`.
  This is declared as the default coercion from `F` to `α ≃+o β`."]
def OrderMonoidIsoClass.toOrderMonoidIso [EquivLike F α β] [OrderIsoClass F α β]
    [MulEquivClass F α β] (f : F) :
    α ≃*o β :=
  { (f : α ≃* β) with map_le_map_iff' := OrderIsoClass.map_le_map_iff f }

Conversion to Ordered Monoid Isomorphism

Informal description

Given a type `F` that satisfies `EquivLike F α β`, `OrderIsoClass F α β`, and `MulEquivClass F α β`, the function converts an element `f : F` into an explicit ordered monoid isomorphism `α ≃*o β`. This isomorphism consists of: 1. A bijection between `α` and `β` that preserves the multiplicative structure (as in `MulEquiv`), 2. An order-preserving property (as in `OrderIso`), meaning that for any `x, y ∈ α`, `x ≤ y` if and only if `f(x) ≤ f(y)`.

instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass_1 instance

[OrderHomClass F α β] [MonoidHomClass F α β] : CoeTC F (α →*o β)

Full source

/-- Any type satisfying `OrderMonoidHomClass` can be cast into `OrderMonoidHom` via
  `OrderMonoidHomClass.toOrderMonoidHom`. -/
@[to_additive "Any type satisfying `OrderAddMonoidHomClass` can be cast into `OrderAddMonoidHom` via
  `OrderAddMonoidHomClass.toOrderAddMonoidHom`"]
instance [OrderHomClass F α β] [MonoidHomClass F α β] : CoeTC F (α →*o β) :=
  ⟨OrderMonoidHomClass.toOrderMonoidHom⟩

Canonical Interpretation of Ordered Monoid Homomorphisms

Informal description

For any type `F` that satisfies both `OrderHomClass F α β` (order-preserving morphisms) and `MonoidHomClass F α β` (monoid homomorphisms), there is a canonical way to interpret an element `f : F` as an ordered monoid homomorphism `α →*o β`. This homomorphism preserves both the multiplicative structure and the order relation.

instCoeTCOrderMonoidIsoOfOrderIsoClassOfMulEquivClass instance

[EquivLike F α β] [OrderIsoClass F α β] [MulEquivClass F α β] : CoeTC F (α ≃*o β)

Full source

/-- Any type satisfying `OrderMonoidIsoClass` can be cast into `OrderMonoidIso` via
  `OrderMonoidIsoClass.toOrderMonoidIso`. -/
@[to_additive "Any type satisfying `OrderAddMonoidIsoClass` can be cast into `OrderAddMonoidIso` via
  `OrderAddMonoidIsoClass.toOrderAddMonoidIso`"]
instance [EquivLike F α β] [OrderIsoClass F α β] [MulEquivClass F α β] : CoeTC F (α ≃*o β) :=
  ⟨OrderMonoidIsoClass.toOrderMonoidIso⟩

Canonical Interpretation of Ordered Monoid Isomorphisms

Informal description

For any type `F` that satisfies `EquivLike F α β`, `OrderIsoClass F α β`, and `MulEquivClass F α β`, there is a canonical way to interpret an element `f : F` as an ordered monoid isomorphism `α ≃*o β`. This means that `f` is a bijection between the ordered monoids `α` and `β` that preserves both the multiplicative structure and the order relation.

OrderMonoidWithZeroHom structure

(α β : Type*) [Preorder α] [Preorder β] [MulZeroOneClass α]
  [MulZeroOneClass β] extends α →*₀ β

Full source

/-- `OrderMonoidWithZeroHom α β` is the type of functions `α → β` that preserve
the `MonoidWithZero` structure.

`OrderMonoidWithZeroHom` is also used for group homomorphisms.

When possible, instead of parametrizing results over `(f : α →+ β)`,
you should parameterize over
`(F : Type*) [FunLike F M N] [MonoidWithZeroHomClass F M N] [OrderHomClass F M N] (f : F)`. -/
structure OrderMonoidWithZeroHom (α β : Type*) [Preorder α] [Preorder β] [MulZeroOneClass α]
  [MulZeroOneClass β] extends α →*₀ β where
  /-- An `OrderMonoidWithZeroHom` is a monotone function. -/
  monotone' : Monotone toFun

Ordered Monoid with Zero Homomorphism

Informal description

The structure `OrderMonoidWithZeroHom α β` represents the type of functions from a preordered monoid with zero `α` to a preordered monoid with zero `β` that preserve both the multiplicative monoid with zero structure and the order relation. This structure extends the bundled homomorphism type `α →*₀ β` (monoid with zero homomorphisms) and is also used for group homomorphisms when appropriate. The functions in this type must satisfy the properties of preserving multiplication, zero, one, and the order relation.

term_→*₀o_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Infix notation for `OrderMonoidWithZeroHom`. -/
infixr:25 " →*₀o " => OrderMonoidWithZeroHom

Ordered monoid with zero homomorphism notation

Informal description

The infix notation `→*₀o` denotes the type of ordered monoid homomorphisms that preserve zero and multiplication between preordered monoids with zero.

OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom definition

[OrderHomClass F α β] [MonoidWithZeroHomClass F α β] (f : F) : α →*₀o β

Full source

/-- Turn an element of a type `F`
satisfying `OrderHomClass F α β` and `MonoidWithZeroHomClass F α β`
into an actual `OrderMonoidWithZeroHom`.
This is declared as the default coercion from `F` to `α →+*₀o β`. -/
@[coe]
def OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom [OrderHomClass F α β]
    [MonoidWithZeroHomClass F α β] (f : F) : α →*₀o β :=
{ (f : α →*₀ β) with monotone' := OrderHomClass.monotone f }

Conversion to ordered monoid-with-zero homomorphism

Informal description

Given a type `F` of functions between preordered monoids with zero `α` and `β`, where `F` satisfies both `OrderHomClass` (order-preserving) and `MonoidWithZeroHomClass` (multiplicative structure-preserving), this definition converts an element `f : F` into an `OrderMonoidWithZeroHom` (a bundled ordered monoid-with-zero homomorphism). The resulting homomorphism preserves both the algebraic structure (multiplication, zero, one) and the order relation.

instCoeTCOrderMonoidWithZeroHomOfOrderHomClassOfMonoidWithZeroHomClass instance

[OrderHomClass F α β] [MonoidWithZeroHomClass F α β] : CoeTC F (α →*₀o β)

Full source

instance [OrderHomClass F α β] [MonoidWithZeroHomClass F α β] : CoeTC F (α →*₀o β) :=
  ⟨OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom⟩

Canonical View of Order-Preserving Monoid-with-Zero Homomorphisms

Informal description

For any type `F` of functions between preordered monoids with zero `α` and `β`, if `F` satisfies both `OrderHomClass` (order-preserving) and `MonoidWithZeroHomClass` (multiplicative structure-preserving), then there is a canonical way to view elements of `F` as bundled ordered monoid-with-zero homomorphisms (`α →*₀o β`).

map_nonneg theorem

(ha : 0 ≤ a) : 0 ≤ f a

Full source

/-- See also `NonnegHomClass.apply_nonneg`. -/
theorem map_nonneg (ha : 0 ≤ a) : 0 ≤ f a := by
  rw [← map_zero f]
  exact OrderHomClass.mono _ ha

Nonnegativity preservation under order-preserving monoid homomorphisms

Informal description

For any order-preserving monoid homomorphism $f \colon \alpha \to \beta$ and any element $a \in \alpha$ such that $0 \leq a$, the image $f(a)$ satisfies $0 \leq f(a)$.

map_nonpos theorem

(ha : a ≤ 0) : f a ≤ 0

Full source

theorem map_nonpos (ha : a ≤ 0) : f a ≤ 0 := by
  rw [← map_zero f]
  exact OrderHomClass.mono _ ha

Order-Preserving Monoid Homomorphism Maps Nonpositive Elements to Nonpositive Elements

Informal description

For any order-preserving monoid homomorphism $f \colon \alpha \to \beta$ and any element $a \in \alpha$ such that $a \leq 0$, the image $f(a)$ satisfies $f(a) \leq 0$.

monotone_iff_map_nonneg theorem

[iamhc : AddMonoidHomClass F α β] : Monotone (f : α → β) ↔ ∀ a, 0 ≤ a → 0 ≤ f a

Full source

theorem monotone_iff_map_nonneg [iamhc : AddMonoidHomClass F α β] :
    MonotoneMonotone (f : α → β) ↔ ∀ a, 0 ≤ a → 0 ≤ f a :=
  ⟨fun h a => by
    rw [← map_zero f]
    apply h, fun h a b hl => by
    rw [← sub_add_cancel b a, map_add f]
    exact le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)⟩

Monotonicity Criterion for Additive Monoid Homomorphisms via Non-Negativity

Informal description

Let $\alpha$ and $\beta$ be ordered additive monoids, and let $F$ be a type of additive monoid homomorphisms from $\alpha$ to $\beta$. For any $f \in F$, the function $f$ is monotone if and only if for every $a \in \alpha$ with $0 \leq a$, we have $0 \leq f(a)$.

antitone_iff_map_nonpos theorem

: Antitone (f : α → β) ↔ ∀ a, 0 ≤ a → f a ≤ 0

Full source

theorem antitone_iff_map_nonpos : AntitoneAntitone (f : α → β) ↔ ∀ a, 0 ≤ a → f a ≤ 0 :=
  monotone_toDual_comp_iff.symm.trans <| monotone_iff_map_nonneg (β := βᵒᵈ) (iamhc := iamhc) _

Antitonicity Criterion for Additive Monoid Homomorphisms via Non-Positivity

Informal description

Let $\alpha$ and $\beta$ be ordered additive monoids, and let $f \colon \alpha \to \beta$ be an additive monoid homomorphism. Then $f$ is antitone (order-reversing) if and only if for every $a \in \alpha$ with $0 \leq a$, we have $f(a) \leq 0$.

monotone_iff_map_nonpos theorem

: Monotone (f : α → β) ↔ ∀ a ≤ 0, f a ≤ 0

Full source

theorem monotone_iff_map_nonpos : MonotoneMonotone (f : α → β) ↔ ∀ a ≤ 0, f a ≤ 0 :=
  antitone_comp_ofDual_iff.symm.trans <| antitone_iff_map_nonpos (α := αᵒᵈ) (iamhc := iamhc) _

Monotonicity Criterion for Additive Monoid Homomorphisms via Non-Positive Elements

Informal description

Let $\alpha$ and $\beta$ be ordered additive monoids, and let $f \colon \alpha \to \beta$ be an additive monoid homomorphism. Then $f$ is monotone (order-preserving) if and only if for every $a \in \alpha$ with $a \leq 0$, we have $f(a) \leq 0$.

antitone_iff_map_nonneg theorem

: Antitone (f : α → β) ↔ ∀ a ≤ 0, 0 ≤ f a

Full source

theorem antitone_iff_map_nonneg : AntitoneAntitone (f : α → β) ↔ ∀ a ≤ 0, 0 ≤ f a :=
  monotone_comp_ofDual_iff.symm.trans <| monotone_iff_map_nonneg (α := αᵒᵈ) (iamhc := iamhc) _

Antitone Additive Monoid Homomorphisms Preserve Non-Negativity on Non-Positive Elements

Informal description

Let $\alpha$ and $\beta$ be ordered additive monoids, and let $f \colon \alpha \to \beta$ be an additive monoid homomorphism. Then $f$ is antitone (order-reversing) if and only if for every $a \in \alpha$ with $a \leq 0$, we have $0 \leq f(a)$.

strictMono_iff_map_pos theorem

: StrictMono (f : α → β) ↔ ∀ a, 0 < a → 0 < f a

Full source

theorem strictMono_iff_map_pos :
    StrictMonoStrictMono (f : α → β) ↔ ∀ a, 0 < a → 0 < f a := by
  refine ⟨fun h a => ?_, fun h a b hl => ?_⟩
  · rw [← map_zero f]
    apply h
  · rw [← sub_add_cancel b a, map_add f]
    exact lt_add_of_pos_left _ (h _ <| sub_pos.2 hl)

Characterization of Strictly Monotone Functions via Positive Elements: $f$ strictly monotone $\iff$ $f$ preserves positivity

Informal description

A function $f \colon \alpha \to \beta$ between ordered additive monoids is strictly monotone if and only if for every element $a \in \alpha$ such that $0 < a$, it holds that $0 < f(a)$.

strictAnti_iff_map_neg theorem

: StrictAnti (f : α → β) ↔ ∀ a, 0 < a → f a < 0

Full source

theorem strictAnti_iff_map_neg : StrictAntiStrictAnti (f : α → β) ↔ ∀ a, 0 < a → f a < 0 :=
  strictMono_toDual_comp_iff.symm.trans <| strictMono_iff_map_pos (β := βᵒᵈ) (iamhc := iamhc) _

Characterization of Strictly Antitone Functions via Positive Elements: $f$ strictly antitone $\iff$ $f$ maps positives to negatives

Informal description

A function $f \colon \alpha \to \beta$ between ordered additive monoids is strictly antitone if and only if for every positive element $a \in \alpha$ (i.e., $0 < a$), the image $f(a)$ is negative (i.e., $f(a) < 0$).

strictMono_iff_map_neg theorem

: StrictMono (f : α → β) ↔ ∀ a < 0, f a < 0

Full source

theorem strictMono_iff_map_neg : StrictMonoStrictMono (f : α → β) ↔ ∀ a < 0, f a < 0 :=
  strictAnti_comp_ofDual_iff.symm.trans <| strictAnti_iff_map_neg (α := αᵒᵈ) (iamhc := iamhc) _

Characterization of Strictly Monotone Functions via Negative Elements: $f$ strictly monotone $\iff$ $f$ preserves negativity

Informal description

A function $f \colon \alpha \to \beta$ between ordered additive monoids is strictly monotone if and only if for every negative element $a \in \alpha$ (i.e., $a < 0$), the image $f(a)$ is also negative (i.e., $f(a) < 0$).

strictAnti_iff_map_pos theorem

: StrictAnti (f : α → β) ↔ ∀ a < 0, 0 < f a

Full source

theorem strictAnti_iff_map_pos : StrictAntiStrictAnti (f : α → β) ↔ ∀ a < 0, 0 < f a :=
  strictMono_comp_ofDual_iff.symm.trans <| strictMono_iff_map_pos (α := αᵒᵈ) (iamhc := iamhc) _

Characterization of Strictly Antitone Functions via Negative Elements: $f$ strictly antitone $\iff$ $f$ maps negatives to positives

Informal description

A function $f \colon \alpha \to \beta$ between ordered additive monoids is strictly antitone if and only if for every element $a \in \alpha$ such that $a < 0$, it holds that $0 < f(a)$.

OrderMonoidHom.instFunLike instance

: FunLike (α →*o β) α β

Full source

@[to_additive]
instance : FunLike (α →*o β) α β where
  coe f := f.toFun
  coe_injective' f g h := by
    obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
    congr

Function-Like Structure on Ordered Monoid Homomorphisms

Informal description

For any two preordered monoids $\alpha$ and $\beta$, the type $\alpha \to^* \beta$ of ordered monoid homomorphisms is equipped with a function-like structure, meaning each homomorphism can be treated as a function from $\alpha$ to $\beta$.

OrderMonoidHom.instOrderHomClass instance

: OrderHomClass (α →*o β) α β

Full source

@[to_additive]
instance : OrderHomClass (α →*o β) α β where
  map_rel f _ _ h := f.monotone' h

Ordered Monoid Homomorphisms as Order-Preserving Maps

Informal description

For any two preordered monoids $\alpha$ and $\beta$, the type $\alpha \to^* \beta$ of ordered monoid homomorphisms forms an `OrderHomClass`, meaning each homomorphism preserves both the order structure and the multiplicative structure between $\alpha$ and $\beta$.

OrderMonoidHom.instMonoidHomClass instance

: MonoidHomClass (α →*o β) α β

Full source

@[to_additive]
instance : MonoidHomClass (α →*o β) α β where
  map_mul f := f.map_mul'
  map_one f := f.map_one'

Ordered Monoid Homomorphisms as Monoid Homomorphisms

Informal description

For any two preordered monoids $\alpha$ and $\beta$, the type $\alpha \to^* \beta$ of ordered monoid homomorphisms forms a `MonoidHomClass`, meaning each homomorphism preserves the multiplicative structure (including the identity element) between $\alpha$ and $\beta$.

OrderMonoidHom.ext theorem

(h : ∀ a, f a = g a) : f = g

Full source

@[to_additive (attr := ext)]
theorem ext (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

Extensionality of Ordered Monoid Homomorphisms

Informal description

If two ordered monoid homomorphisms $f, g \colon \alpha \to^* \beta$ satisfy $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

OrderMonoidHom.toFun_eq_coe theorem

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

Full source

@[to_additive]
theorem toFun_eq_coe (f : α →*o β) : f.toFun = (f : α → β) :=
  rfl

Underlying Function of Ordered Monoid Homomorphism Equals its Coercion

Informal description

For any ordered monoid homomorphism $f \colon \alpha \to^* \beta$, the underlying function $f.\text{toFun}$ is equal to the coercion of $f$ to a function $\alpha \to \beta$.

OrderMonoidHom.coe_mk theorem

(f : α →* β) (h) : (OrderMonoidHom.mk f h : α → β) = f

Full source

@[to_additive (attr := simp)]
theorem coe_mk (f : α →* β) (h) : (OrderMonoidHom.mk f h : α → β) = f :=
  rfl

Coercion of Constructed Ordered Monoid Homomorphism Equals Original Function

Informal description

For any monoid homomorphism $f \colon \alpha \to^* \beta$ and any proof $h$ that $f$ preserves the order, the coercion of the ordered monoid homomorphism constructed from $f$ and $h$ to a function $\alpha \to \beta$ is equal to $f$ itself.

OrderMonoidHom.mk_coe theorem

(f : α →*o β) (h) : OrderMonoidHom.mk (f : α →* β) h = f

Full source

@[to_additive (attr := simp)]
theorem mk_coe (f : α →*o β) (h) : OrderMonoidHom.mk (f : α →* β) h = f := by
  ext
  rfl

Construction of Ordered Monoid Homomorphism from Underlying Homomorphism Preserves Identity

Informal description

Given an ordered monoid homomorphism $f \colon \alpha \to^* \beta$ and a proof $h$ that $f$ preserves the order, the ordered monoid homomorphism constructed from the underlying monoid homomorphism $(f \colon \alpha \to^* \beta)$ and $h$ is equal to $f$ itself.

OrderMonoidHom.toOrderHom definition

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

Full source

/-- Reinterpret an ordered monoid homomorphism as an order homomorphism. -/
@[to_additive "Reinterpret an ordered additive monoid homomorphism as an order homomorphism."]
def toOrderHom (f : α →*o β) : α →o β :=
  { f with }

Ordered monoid homomorphism as order homomorphism

Informal description

Given an ordered monoid homomorphism $f : \alpha \to^* \beta$, this function reinterprets $f$ as an order homomorphism, i.e., a monotone function between the preorders $\alpha$ and $\beta$.

OrderMonoidHom.coe_monoidHom theorem

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

Full source

@[to_additive (attr := simp)]
theorem coe_monoidHom (f : α →*o β) : ((f : α →* β) : α → β) = f :=
  rfl

Coercion of Ordered Monoid Homomorphism to Function via Monoid Homomorphism

Informal description

For any ordered monoid homomorphism $f \colon \alpha \to^* \beta$, the underlying function obtained by first coercing $f$ to a monoid homomorphism and then to a function is equal to $f$ itself.

OrderMonoidHom.coe_orderHom theorem

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

Full source

@[to_additive (attr := simp)]
theorem coe_orderHom (f : α →*o β) : ((f : α →o β) : α → β) = f :=
  rfl

Coercion of Ordered Monoid Homomorphism to Function via Order Homomorphism

Informal description

For any ordered monoid homomorphism $f \colon \alpha \to^* \beta$, the underlying function obtained by first coercing $f$ to an order homomorphism $\alpha \to_o \beta$ and then to a function $\alpha \to \beta$ is equal to $f$ itself.

OrderMonoidHom.toMonoidHom_injective theorem

: Injective (toMonoidHom : _ → α →* β)

Full source

@[to_additive]
theorem toMonoidHom_injective : Injective (toMonoidHom : _ → α →* β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

Injectivity of the Underlying Monoid Homomorphism for Ordered Monoid Homomorphisms

Informal description

The function that maps an ordered monoid homomorphism $f \colon \alpha \to^* \beta$ to its underlying monoid homomorphism is injective. In other words, if two ordered monoid homomorphisms have the same underlying monoid homomorphism, then they are equal.

OrderMonoidHom.toOrderHom_injective theorem

: Injective (toOrderHom : _ → α →o β)

Full source

@[to_additive]
theorem toOrderHom_injective : Injective (toOrderHom : _ → α →o β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

Injectivity of the Order Homomorphism Underlying an Ordered Monoid Homomorphism

Informal description

The function that maps an ordered monoid homomorphism $f \colon \alpha \to^* \beta$ to its underlying order homomorphism $f \colon \alpha \to_o \beta$ is injective. In other words, if two ordered monoid homomorphisms induce the same order homomorphism, then they are equal.

OrderMonoidHom.copy definition

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

Full source

/-- Copy of an `OrderMonoidHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
@[to_additive "Copy of an `OrderAddMonoidHom` 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.toMonoidHom.copy f' h with toFun := f', monotone' := h.symm.subst f.monotone' }

Copy of an ordered monoid homomorphism with a new function

Informal description

Given an ordered monoid homomorphism $f \colon \alpha \to^* \beta$ between preordered monoids $\alpha$ and $\beta$, and a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, the function `OrderMonoidHom.copy` constructs a new ordered monoid homomorphism with the underlying function $f'$ that preserves both the multiplicative and order structures. This is useful for fixing definitional equalities while maintaining the homomorphism structure.

OrderMonoidHom.coe_copy theorem

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

Full source

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

Underlying function of copied ordered monoid homomorphism equals the copied function

Informal description

Given an ordered monoid homomorphism $f \colon \alpha \to^* \beta$ between preordered monoids $\alpha$ and $\beta$, a function $f' \colon \alpha \to \beta$ such that $f' = f$, then the underlying function of the copied homomorphism $f.copy\ f'\ h$ is equal to $f'$.

OrderMonoidHom.copy_eq theorem

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

Full source

@[to_additive]
theorem copy_eq (f : α →*o β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

Copy of Ordered Monoid Homomorphism Preserves Equality

Informal description

Let $\alpha$ and $\beta$ be preordered monoids, and let $f \colon \alpha \to^* \beta$ be an ordered monoid homomorphism. Given a function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with underlying function $f'$ is equal to $f$ itself.

OrderMonoidHom.id definition

: α →*o α

Full source

/-- The identity map as an ordered monoid homomorphism. -/
@[to_additive "The identity map as an ordered additive monoid homomorphism."]
protected def id : α →*o α :=
  { MonoidHom.id α, OrderHom.id with }

Identity ordered monoid homomorphism

Informal description

The identity map from an ordered monoid $\alpha$ to itself, viewed as an ordered monoid homomorphism. It preserves both the multiplicative structure and the order relation.

OrderMonoidHom.coe_id theorem

: ⇑(OrderMonoidHom.id α) = id

Full source

@[to_additive (attr := simp)]
theorem coe_id : ⇑(OrderMonoidHom.id α) = id :=
  rfl

Identity Ordered Monoid Homomorphism is the Identity Function

Informal description

The underlying function of the identity ordered monoid homomorphism on $\alpha$ is equal to the identity function on $\alpha$.

OrderMonoidHom.instInhabited instance

: Inhabited (α →*o α)

Full source

@[to_additive]
instance : Inhabited (α →*o α) :=
  ⟨OrderMonoidHom.id α⟩

Inhabited Ordered Monoid Homomorphisms

Informal description

For any preordered monoid $\alpha$, the type of ordered monoid homomorphisms from $\alpha$ to itself is inhabited.

OrderMonoidHom.comp definition

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

Full source

/-- Composition of `OrderMonoidHom`s as an `OrderMonoidHom`. -/
@[to_additive "Composition of `OrderAddMonoidHom`s as an `OrderAddMonoidHom`"]
def comp (f : β →*o γ) (g : α →*o β) : α →*o γ :=
  { f.toMonoidHom.comp (g : α →* β), f.toOrderHom.comp (g : α →o β) with }

Composition of ordered monoid homomorphisms

Informal description

Given ordered monoid homomorphisms $ f \colon \beta \to^* \gamma $ and $ g \colon \alpha \to^* \beta $, their composition $ f \circ g \colon \alpha \to^* \gamma $ is defined as the ordered monoid homomorphism whose underlying function is the composition of the underlying functions of $ f $ and $ g $, and which preserves both the order and the monoid structure.

OrderMonoidHom.coe_comp theorem

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

Full source

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

Composition of Ordered Monoid Homomorphisms Preserves Underlying Function

Informal description

For ordered monoid homomorphisms $f \colon \beta \to^* \gamma$ and $g \colon \alpha \to^* \beta$, the underlying function of their composition $f \circ g \colon \alpha \to^* \gamma$ is equal to the composition of the underlying functions of $f$ and $g$, i.e., $(f \circ g)(x) = f(g(x))$ for all $x \in \alpha$.

OrderMonoidHom.comp_apply theorem

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

Full source

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

Composition of Ordered Monoid Homomorphisms Evaluates as Function Composition

Informal description

For any ordered monoid homomorphisms $f \colon \beta \to^* \gamma$ and $g \colon \alpha \to^* \beta$, and any element $a \in \alpha$, the composition $(f \circ g)(a)$ equals $f(g(a))$.

OrderMonoidHom.coe_comp_monoidHom theorem

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

Full source

@[to_additive]
theorem coe_comp_monoidHom (f : β →*o γ) (g : α →*o β) :
    (f.comp g : α →* γ) = (f : β →* γ).comp g :=
  rfl

Composition of Ordered Monoid Homomorphisms as Monoid Homomorphisms

Informal description

For any ordered monoid homomorphisms $ f \colon \beta \to^* \gamma $ and $ g \colon \alpha \to^* \beta $, the underlying monoid homomorphism of the composition $ f \circ g \colon \alpha \to^* \gamma $ is equal to the composition of the underlying monoid homomorphisms of $ f $ and $ g $. That is, $ (f \circ g) = f \circ g $ as monoid homomorphisms.

OrderMonoidHom.coe_comp_orderHom theorem

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

Full source

@[to_additive]
theorem coe_comp_orderHom (f : β →*o γ) (g : α →*o β) :
    (f.comp g : α →o γ) = (f : β →o γ).comp g :=
  rfl

Compatibility of Composition with Underlying Order Homomorphism in Ordered Monoid Homomorphisms

Informal description

For any ordered monoid homomorphisms $f \colon \beta \to^* \gamma$ and $g \colon \alpha \to^* \beta$, the underlying order homomorphism of the composition $f \circ g$ is equal to the composition of the underlying order homomorphisms of $f$ and $g$. That is, $(f \circ g) = f \circ g$ as order homomorphisms.

OrderMonoidHom.comp_assoc theorem

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

Full source

@[to_additive (attr := simp)]
theorem comp_assoc (f : γ →*o δ) (g : β →*o γ) (h : α →*o β) :
    (f.comp g).comp h = f.comp (g.comp h) :=
  rfl

Associativity of Composition for Ordered Monoid Homomorphisms

Informal description

For ordered monoid homomorphisms $f \colon \gamma \to^* \delta$, $g \colon \beta \to^* \gamma$, and $h \colon \alpha \to^* \beta$, the composition operation satisfies the associativity property: $$(f \circ g) \circ h = f \circ (g \circ h).$$

OrderMonoidHom.comp_id theorem

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

Full source

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

Composition with Identity Preserves Ordered Monoid Homomorphism

Informal description

For any ordered monoid homomorphism $f \colon \alpha \to^* \beta$, the composition of $f$ with the identity ordered monoid homomorphism on $\alpha$ is equal to $f$.

OrderMonoidHom.id_comp theorem

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

Full source

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

Identity Ordered Monoid Homomorphism is Left Neutral Element for Composition

Informal description

For any ordered monoid homomorphism $f \colon \alpha \to^* \beta$, the composition of the identity ordered monoid homomorphism on $\beta$ with $f$ is equal to $f$ itself, i.e., $\text{id}_\beta \circ f = f$.

OrderMonoidHom.cancel_right theorem

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

Full source

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

Right Cancellation Property for Ordered Monoid Homomorphisms

Informal description

Let $f \colon \alpha \to^* \beta$ be a surjective ordered monoid homomorphism, and let $g_1, g_2 \colon \beta \to^* \gamma$ be ordered monoid homomorphisms. Then $g_1 \circ f = g_2 \circ f$ if and only if $g_1 = g_2$.

OrderMonoidHom.cancel_left theorem

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

Full source

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

Left Cancellation Property for Ordered Monoid Homomorphisms

Informal description

Let $g \colon \beta \to^* \gamma$ be an injective ordered monoid homomorphism, and let $f_1, f_2 \colon \alpha \to^* \beta$ be ordered monoid homomorphisms. Then $g \circ f_1 = g \circ f_2$ if and only if $f_1 = f_2$.

OrderMonoidHom.instOne instance

: One (α →*o β)

Full source

/-- `1` is the homomorphism sending all elements to `1`. -/
@[to_additive "`0` is the homomorphism sending all elements to `0`."]
instance : One (α →*o β) :=
  ⟨{ (1 : α →* β) with monotone' := monotone_const }⟩

Constant One Ordered Monoid Homomorphism

Informal description

For any preordered monoids $\alpha$ and $\beta$, there is a constant ordered monoid homomorphism from $\alpha$ to $\beta$ that sends every element to the identity element $1$ of $\beta$.

OrderMonoidHom.coe_one theorem

: ⇑(1 : α →*o β) = 1

Full source

@[to_additive (attr := simp)]
theorem coe_one : ⇑(1 : α →*o β) = 1 :=
  rfl

Constant Ordered Monoid Homomorphism as Constant Function

Informal description

The underlying function of the constant ordered monoid homomorphism $1 : \alpha \to^* \beta$ (which maps every element to the identity element $1 \in \beta$) is equal to the constant function $1 : \alpha \to \beta$.

OrderMonoidHom.one_apply theorem

(a : α) : (1 : α →*o β) a = 1

Full source

@[to_additive (attr := simp)]
theorem one_apply (a : α) : (1 : α →*o β) a = 1 :=
  rfl

Evaluation of Constant Ordered Monoid Homomorphism at Identity

Informal description

For any element $a$ in a preordered monoid $\alpha$, the constant ordered monoid homomorphism $1 : \alpha \to^* \beta$ evaluates to the identity element $1$ in the preordered monoid $\beta$, i.e., $1(a) = 1$.

OrderMonoidHom.one_comp theorem

(f : α →*o β) : (1 : β →*o γ).comp f = 1

Full source

@[to_additive (attr := simp)]
theorem one_comp (f : α →*o β) : (1 : β →*o γ).comp f = 1 :=
  rfl

Composition with Constant Ordered Monoid Homomorphism Yields Constant Homomorphism

Informal description

Let $f \colon \alpha \to^* \beta$ be an ordered monoid homomorphism. Then the composition of the constant ordered monoid homomorphism $1 \colon \beta \to^* \gamma$ (which maps every element to the identity element $1 \in \gamma$) with $f$ is equal to the constant ordered monoid homomorphism $1 \colon \alpha \to^* \gamma$.

OrderMonoidHom.comp_one theorem

(f : β →*o γ) : f.comp (1 : α →*o β) = 1

Full source

@[to_additive (attr := simp)]
theorem comp_one (f : β →*o γ) : f.comp (1 : α →*o β) = 1 :=
  ext fun _ => map_one f

Composition with Constant Homomorphism Yields Constant Homomorphism

Informal description

For any ordered monoid homomorphism $f \colon \beta \to^* \gamma$, the composition of $f$ with the constant ordered monoid homomorphism $1 \colon \alpha \to^* \beta$ (which sends every element to the identity element of $\beta$) is equal to the constant ordered monoid homomorphism $1 \colon \alpha \to^* \gamma$.

OrderMonoidHom.instMulOfIsOrderedMonoid instance

[IsOrderedMonoid β] : Mul (α →*o β)

Full source

/-- For two ordered monoid morphisms `f` and `g`, their product is the ordered monoid morphism
sending `a` to `f a * g a`. -/
@[to_additive "For two ordered additive monoid morphisms `f` and `g`, their product is the ordered
additive monoid morphism sending `a` to `f a + g a`."]
instance [IsOrderedMonoid β] : Mul (α →*o β) :=
  ⟨fun f g => { (f * g : α →* β) with monotone' := f.monotone'.mul' g.monotone' }⟩

Pointwise Multiplication of Ordered Monoid Homomorphisms

Informal description

For any ordered monoid $\beta$, the set of ordered monoid homomorphisms from $\alpha$ to $\beta$ forms a monoid under pointwise multiplication. That is, given two ordered monoid homomorphisms $f, g: \alpha \to \beta$, their product $f \cdot g$ is the homomorphism defined by $(f \cdot g)(x) = f(x) \cdot g(x)$ for all $x \in \alpha$.

OrderMonoidHom.coe_mul theorem

[IsOrderedMonoid β] (f g : α →*o β) : ⇑(f * g) = f * g

Full source

@[to_additive (attr := simp)]
theorem coe_mul [IsOrderedMonoid β] (f g : α →*o β) : ⇑(f * g) = f * g :=
  rfl

Pointwise product of ordered monoid homomorphisms equals product of underlying functions

Informal description

Let $\alpha$ and $\beta$ be preordered monoids, with $\beta$ being an ordered monoid. For any two ordered monoid homomorphisms $f, g: \alpha \to \beta$, the underlying function of their pointwise product $f \cdot g$ is equal to the pointwise product of the underlying functions, i.e., $(f \cdot g)(x) = f(x) \cdot g(x)$ for all $x \in \alpha$.

OrderMonoidHom.mul_apply theorem

[IsOrderedMonoid β] (f g : α →*o β) (a : α) : (f * g) a = f a * g a

Full source

@[to_additive (attr := simp)]
theorem mul_apply [IsOrderedMonoid β] (f g : α →*o β) (a : α) : (f * g) a = f a * g a :=
  rfl

Pointwise Product Evaluation for Ordered Monoid Homomorphisms

Informal description

Let $\alpha$ and $\beta$ be preordered monoids, with $\beta$ being an ordered monoid. For any two ordered monoid homomorphisms $f, g: \alpha \to \beta$ and any element $a \in \alpha$, the evaluation of their pointwise product at $a$ satisfies $(f \cdot g)(a) = f(a) \cdot g(a)$.

OrderMonoidHom.mul_comp theorem

[IsOrderedMonoid γ] (g₁ g₂ : β →*o γ) (f : α →*o β) : (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

Full source

@[to_additive]
theorem mul_comp [IsOrderedMonoid γ] (g₁ g₂ : β →*o γ) (f : α →*o β) :
    (g₁ * g₂).comp f = g₁.comp f * g₂.comp f :=
  rfl

Composition Distributes Over Pointwise Product of Ordered Monoid Homomorphisms

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preordered monoids, with $\gamma$ being an ordered monoid. For any ordered monoid homomorphisms $g_1, g_2 \colon \beta \to^* \gamma$ and $f \colon \alpha \to^* \beta$, the composition of the pointwise product $g_1 \cdot g_2$ with $f$ is equal to the pointwise product of the compositions $g_1 \circ f$ and $g_2 \circ f$. That is, $$(g_1 \cdot g_2) \circ f = (g_1 \circ f) \cdot (g_2 \circ f).$$

OrderMonoidHom.comp_mul theorem

 [IsOrderedMonoid β] [IsOrderedMonoid γ] (g : β →*o γ) (f₁ f₂ : α →*o β) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Full source

@[to_additive]
theorem comp_mul [IsOrderedMonoid β] [IsOrderedMonoid γ] (g : β →*o γ) (f₁ f₂ : α →*o β) :
    g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ :=
  ext fun _ => map_mul g _ _

Composition Distributes Over Pointwise Product of Ordered Monoid Homomorphisms

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be ordered monoids. For any ordered monoid homomorphism $g \colon \beta \to^* \gamma$ and any two ordered monoid homomorphisms $f_1, f_2 \colon \alpha \to^* \beta$, the composition of $g$ with the pointwise product $f_1 \cdot f_2$ equals the pointwise product of the compositions $g \circ f_1$ and $g \circ f_2$. That is, $$ g \circ (f_1 \cdot f_2) = (g \circ f_1) \cdot (g \circ f_2). $$

OrderMonoidHom.toMonoidHom_eq_coe theorem

(f : α →*o β) : f.toMonoidHom = f

Full source

@[to_additive (attr := simp)]
theorem toMonoidHom_eq_coe (f : α →*o β) : f.toMonoidHom = f :=
  rfl

Equality of Ordered Monoid Homomorphism and its Underlying Monoid Homomorphism

Informal description

For any ordered monoid homomorphism $f \colon \alpha \to^* \beta$, the underlying monoid homomorphism obtained via `toMonoidHom` is equal to $f$ itself when viewed as a function.

OrderMonoidHom.toOrderHom_eq_coe theorem

(f : α →*o β) : f.toOrderHom = f

Full source

@[to_additive (attr := simp)]
theorem toOrderHom_eq_coe (f : α →*o β) : f.toOrderHom = f :=
  rfl

Ordered Monoid Homomorphism Coincides with its Order Homomorphism Component

Informal description

For any ordered monoid homomorphism $f \colon \alpha \to^* \beta$, the underlying order homomorphism of $f$ is equal to $f$ itself when viewed as a function.

OrderMonoidHom.mk' definition

(f : α → β) (hf : Monotone f) (map_mul : ∀ a b : α, f (a * b) = f a * f b) : α →*o β

Full source

/-- Makes an ordered group homomorphism from a proof that the map preserves multiplication. -/
@[to_additive
      "Makes an ordered additive group homomorphism from a proof that the map preserves
      addition."]
def mk' (f : α → β) (hf : Monotone f) (map_mul : ∀ a b : α, f (a * b) = f a * f b) : α →*o β :=
  { MonoidHom.mk' f map_mul with monotone' := hf }

Ordered monoid homomorphism from multiplication-preserving monotone function

Informal description

Given a function $ f \colon \alpha \to \beta $ between preordered monoids that is monotone and preserves multiplication (i.e., $ f(a \cdot b) = f(a) \cdot f(b) $ for all $ a, b \in \alpha $), this definition constructs an ordered monoid homomorphism from $ \alpha $ to $ \beta $. The preservation of the identity element is automatically derived from the preservation of multiplication.

OrderMonoidIso.instEquivLike instance

: EquivLike (α ≃*o β) α β

Full source

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

Ordered Monoid Isomorphisms as Bijections

Informal description

For any two ordered monoids (or groups) $\alpha$ and $\beta$, the type $\alpha \simeq^* \beta$ of order-preserving monoid isomorphisms can be injectively coerced to bijections between $\alpha$ and $\beta$. This means that every element of $\alpha \simeq^* \beta$ can be viewed as a bijective function from $\alpha$ to $\beta$ that preserves both the monoid structure and the order relation.

OrderMonoidIso.instOrderIsoClass instance

: OrderIsoClass (α ≃*o β) α β

Full source

@[to_additive]
instance : OrderIsoClass (α ≃*o β) α β where
  map_le_map_iff f := f.map_le_map_iff'

Ordered Monoid Isomorphisms as Order Isomorphisms

Informal description

For any two ordered monoids (or groups) $\alpha$ and $\beta$, the type $\alpha \simeq^* \beta$ of order-preserving monoid isomorphisms forms an order isomorphism class. This means that every element of $\alpha \simeq^* \beta$ is a bijective function that preserves both the monoid structure and the order relation, and reflects the order relation (i.e., $f(x) \leq f(y)$ implies $x \leq y$).

OrderMonoidIso.instMulEquivClass instance

: MulEquivClass (α ≃*o β) α β

Full source

@[to_additive]
instance : MulEquivClass (α ≃*o β) α β where
  map_mul f := map_mul f.toMulEquiv

Ordered Monoid Isomorphisms as Multiplicative Equivalences

Informal description

For any two ordered monoids (or groups) $\alpha$ and $\beta$, the type $\alpha \simeq^* \beta$ of order-preserving monoid isomorphisms forms a multiplicative equivalence class. This means that every element of $\alpha \simeq^* \beta$ is a bijective function that preserves the multiplicative structure, i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in \alpha$.

OrderMonoidIso.ext theorem

(h : ∀ a, f a = g a) : f = g

Full source

@[to_additive (attr := ext)]
theorem ext (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

Extensionality of Ordered Monoid Isomorphisms

Informal description

For any two ordered monoid isomorphisms $f, g : \alpha \simeq^* \beta$, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

OrderMonoidIso.toFun_eq_coe theorem

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

Full source

@[to_additive]
theorem toFun_eq_coe (f : α ≃*o β) : f.toFun = (f : α → β) :=
  rfl

Equality of Underlying Function and Coercion for Ordered Monoid Isomorphism

Informal description

For any ordered monoid isomorphism $f : \alpha \simeq^* \beta$, the underlying function `f.toFun` is equal to the coercion of $f$ to a function $\alpha \to \beta$.

OrderMonoidIso.coe_mk theorem

(f : α ≃* β) (h) : (OrderMonoidIso.mk f h : α → β) = f

Full source

@[to_additive (attr := simp)]
theorem coe_mk (f : α ≃* β) (h) : (OrderMonoidIso.mk f h : α → β) = f :=
  rfl

Underlying Function of Ordered Monoid Isomorphism Construction

Informal description

For any multiplicative isomorphism $f : \alpha \simeq^* \beta$ and any proof $h$ that $f$ is order-preserving, the underlying function of the ordered monoid isomorphism constructed via `OrderMonoidIso.mk f h` is equal to $f$ itself.

OrderMonoidIso.mk_coe theorem

(f : α ≃*o β) (h) : OrderMonoidIso.mk (f : α ≃* β) h = f

Full source

@[to_additive (attr := simp)]
theorem mk_coe (f : α ≃*o β) (h) : OrderMonoidIso.mk (f : α ≃* β) h = f := rfl

Construction of Ordered Monoid Isomorphism from Multiplicative Equivalence Preserves Identity

Informal description

For any ordered monoid isomorphism $f : \alpha \simeq^* \beta$ and any proof $h$ that $f$ is order-preserving, the construction of an ordered monoid isomorphism via `OrderMonoidIso.mk` applied to the underlying multiplicative equivalence $(f : \alpha \simeq^* \beta)$ and $h$ yields $f$ itself.

OrderMonoidIso.toOrderIso definition

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

Full source

/-- Reinterpret an ordered monoid isomorphism as an order isomorphism. -/
@[to_additive "Reinterpret an ordered additive monoid isomomorphism as an order isomomorphism."]
def toOrderIso (f : α ≃*o β) : α ≃o β :=
  { f with
    map_rel_iff' := map_le_map_iff f }

Ordered monoid isomorphism as order isomorphism

Informal description

Given an ordered monoid isomorphism $f : \alpha \simeq^* \beta$, the function `OrderMonoidIso.toOrderIso` reinterprets $f$ as an order isomorphism $\alpha \simeq^o \beta$, where the order-preserving property is derived from the fact that $f$ preserves both the multiplicative and order structures.

OrderMonoidIso.coe_mulEquiv theorem

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

Full source

@[to_additive (attr := simp)]
theorem coe_mulEquiv (f : α ≃*o β) : ((f : α ≃* β) : α → β) = f :=
  rfl

Coercion of Ordered Monoid Isomorphism to Function via Multiplicative Equivalence

Informal description

For any ordered monoid isomorphism $f : \alpha \simeq^* \beta$, the underlying multiplicative equivalence $f : \alpha \simeq^* \beta$ coerced to a function $\alpha \to \beta$ is equal to $f$ itself.

OrderMonoidIso.coe_orderIso theorem

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

Full source

@[to_additive (attr := simp)]
theorem coe_orderIso (f : α ≃*o β) : ((f : α →o β) : α → β) = f :=
  rfl

Coercion of Ordered Monoid Isomorphism to Function via Order Homomorphism

Informal description

For any ordered monoid isomorphism $f : \alpha \simeq^* \beta$, the underlying function obtained by first coercing $f$ to an order homomorphism $\alpha \to_o \beta$ and then to a function $\alpha \to \beta$ is equal to $f$ itself.

OrderMonoidIso.toMulEquiv_injective theorem

: Injective (toMulEquiv : _ → α ≃* β)

Full source

@[to_additive]
theorem toMulEquiv_injective : Injective (toMulEquiv : _ → α ≃* β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

Injectivity of the Multiplicative Equivalence Underlying Ordered Monoid Isomorphisms

Informal description

The function `toMulEquiv` that maps an ordered monoid isomorphism $f : \alpha \simeq^* \beta$ to its underlying multiplicative equivalence is injective. That is, if two ordered monoid isomorphisms $f$ and $g$ have the same multiplicative equivalence, then $f = g$.

OrderMonoidIso.toOrderIso_injective theorem

: Injective (toOrderIso : _ → α ≃o β)

Full source

@[to_additive]
theorem toOrderIso_injective : Injective (toOrderIso : _ → α ≃o β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

Injectivity of the Underlying Order Isomorphism Map for Ordered Monoid Isomorphisms

Informal description

The function that maps an ordered monoid isomorphism $f : \alpha \simeq^* \beta$ to its underlying order isomorphism $\alpha \simeq^o \beta$ is injective. In other words, if two ordered monoid isomorphisms induce the same order isomorphism, then they must be equal.

OrderMonoidIso.refl definition

: α ≃*o α

Full source

/-- The identity map as an ordered monoid isomorphism. -/
@[to_additive "The identity map as an ordered additive monoid isomorphism."]
protected def refl : α ≃*o α :=
  { MulEquiv.refl α with map_le_map_iff' := by simp }

Identity ordered monoid isomorphism

Informal description

The identity map on an ordered monoid $\alpha$, viewed as an ordered monoid isomorphism from $\alpha$ to itself. This map preserves both the multiplicative structure and the order relation, and is its own inverse.

OrderMonoidIso.coe_refl theorem

: ⇑(OrderMonoidIso.refl α) = id

Full source

@[to_additive (attr := simp)]
theorem coe_refl : ⇑(OrderMonoidIso.refl α) = id :=
  rfl

Identity Ordered Monoid Isomorphism as Identity Function

Informal description

The underlying function of the identity ordered monoid isomorphism on $\alpha$ is equal to the identity function $\text{id} : \alpha \to \alpha$.

OrderMonoidIso.instInhabited instance

: Inhabited (α ≃*o α)

Full source

@[to_additive]
instance : Inhabited (α ≃*o α) :=
  ⟨OrderMonoidIso.refl α⟩

Inhabited Ordered Monoid Isomorphisms

Informal description

For any ordered monoid $\alpha$, the type of ordered monoid isomorphisms from $\alpha$ to itself is inhabited.

OrderMonoidIso.trans definition

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

Full source

/-- Transitivity of multiplication-preserving order isomorphisms -/
@[to_additive (attr := trans) "Transitivity of addition-preserving order isomorphisms"]
def trans (f : α ≃*o β) (g : β ≃*o γ) : α ≃*o γ :=
  { (f : α ≃* β).trans g with map_le_map_iff' := by simp }

Composition of order-preserving monoid isomorphisms

Informal description

Given two order-preserving monoid isomorphisms $f: \alpha \simeq^* \beta$ and $g: \beta \simeq^* \gamma$, their composition $g \circ f$ forms an order-preserving monoid isomorphism $\alpha \simeq^* \gamma$. This means: 1. The composition preserves the multiplicative structure: $(g \circ f)(x \cdot y) = (g \circ f)(x) \cdot (g \circ f)(y)$ for all $x, y \in \alpha$, 2. The composition preserves the order: $x \leq y \implies (g \circ f)(x) \leq (g \circ f)(y)$ for all $x, y \in \alpha$, 3. The composition is bijective with an inverse that also preserves multiplication and order.

OrderMonoidIso.coe_trans theorem

(f : α ≃*o β) (g : β ≃*o γ) : (f.trans g : α → γ) = g ∘ f

Full source

@[to_additive (attr := simp)]
theorem coe_trans (f : α ≃*o β) (g : β ≃*o γ) : (f.trans g : α → γ) = g ∘ f :=
  rfl

Composition of Ordered Monoid Isomorphisms as Function Composition

Informal description

For any ordered monoid isomorphisms $f: \alpha \simeq^* \beta$ and $g: \beta \simeq^* \gamma$, the underlying function of their composition $f \circ g$ is equal to the composition of the underlying functions $g \circ f$.

OrderMonoidIso.trans_apply theorem

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

Full source

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

Composition of Ordered Monoid Isomorphisms Preserves Evaluation

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be ordered monoids (or groups), and let $f: \alpha \simeq^* \beta$ and $g: \beta \simeq^* \gamma$ be order-preserving monoid isomorphisms. For any element $a \in \alpha$, the composition $(f \circ g)(a)$ equals $g(f(a))$.

OrderMonoidIso.coe_trans_mulEquiv theorem

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

Full source

@[to_additive]
theorem coe_trans_mulEquiv (f : α ≃*o β) (g : β ≃*o γ) :
    (f.trans g : α ≃* γ) = (f : α ≃* β).trans g :=
  rfl

Composition of Ordered Monoid Isomorphisms Preserves Multiplicative Equivalence Structure

Informal description

For any order-preserving monoid isomorphisms $f: \alpha \simeq^* \beta$ and $g: \beta \simeq^* \gamma$, the underlying multiplicative equivalence of their composition $f \circ g$ is equal to the composition of the underlying multiplicative equivalences of $f$ and $g$. That is, $(f \circ g) = (f) \circ (g)$ as multiplicative equivalences.

OrderMonoidIso.coe_trans_orderIso theorem

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

Full source

@[to_additive]
theorem coe_trans_orderIso (f : α ≃*o β) (g : β ≃*o γ) :
    (f.trans g : α ≃o γ) = (f : α ≃o β).trans g :=
  rfl

Composition of Order-Preserving Monoid Isomorphisms as Order Isomorphisms

Informal description

For any two order-preserving monoid isomorphisms $f \colon \alpha \simeq^* \beta$ and $g \colon \beta \simeq^* \gamma$, the underlying order isomorphism of their composition $f \circ g$ is equal to the composition of their underlying order isomorphisms. That is, $(f \circ g)_{\text{order}} = f_{\text{order}} \circ g_{\text{order}}$.

OrderMonoidIso.trans_assoc theorem

(f : α ≃*o β) (g : β ≃*o γ) (h : γ ≃*o δ) : (f.trans g).trans h = f.trans (g.trans h)

Full source

@[to_additive (attr := simp)]
theorem trans_assoc (f : α ≃*o β) (g : β ≃*o γ) (h : γ ≃*o δ) :
    (f.trans g).trans h = f.trans (g.trans h) :=
  rfl

Associativity of Composition of Order-Preserving Monoid Isomorphisms

Informal description

For any order-preserving monoid isomorphisms $f: \alpha \simeq^* \beta$, $g: \beta \simeq^* \gamma$, and $h: \gamma \simeq^* \delta$, the composition of these isomorphisms is associative, i.e., $(f \circ g) \circ h = f \circ (g \circ h)$.

OrderMonoidIso.trans_refl theorem

(f : α ≃*o β) : f.trans (OrderMonoidIso.refl β) = f

Full source

@[to_additive (attr := simp)]
theorem trans_refl (f : α ≃*o β) : f.trans (OrderMonoidIso.refl β) = f :=
  rfl

Right identity law for composition of ordered monoid isomorphisms

Informal description

For any order-preserving monoid isomorphism $f \colon \alpha \simeq^* \beta$, the composition of $f$ with the identity isomorphism on $\beta$ is equal to $f$ itself, i.e., $f \circ \text{id}_\beta = f$.

OrderMonoidIso.refl_trans theorem

(f : α ≃*o β) : (OrderMonoidIso.refl α).trans f = f

Full source

@[to_additive (attr := simp)]
theorem refl_trans (f : α ≃*o β) : (OrderMonoidIso.refl α).trans f = f :=
  rfl

Identity isomorphism is a left identity for composition of ordered monoid isomorphisms

Informal description

For any ordered monoid isomorphism $f \colon \alpha \simeq^* \beta$, the composition of the identity isomorphism on $\alpha$ with $f$ is equal to $f$ itself. That is, $\text{id}_\alpha \circ f = f$.

OrderMonoidIso.cancel_right theorem

{g₁ g₂ : α ≃*o β} {f : β ≃*o γ} (hf : Function.Injective f) : g₁.trans f = g₂.trans f ↔ g₁ = g₂

Full source

@[to_additive (attr := simp)]
theorem cancel_right {g₁ g₂ : α ≃*o β} {f : β ≃*o γ} (hf : Function.Injective f) :
    g₁.trans f = g₂.trans f ↔ g₁ = g₂ :=
  ⟨fun h => ext fun a => hf <| by rw [← trans_apply, h, trans_apply], by rintro rfl; rfl⟩

Right Cancellation Property for Composition of Ordered Monoid Isomorphisms

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be ordered monoids (or groups), and let $f : \beta \simeq^* \gamma$ be an injective order-preserving monoid isomorphism. For any two order-preserving monoid isomorphisms $g_1, g_2 : \alpha \simeq^* \beta$, the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

OrderMonoidIso.cancel_left theorem

{g : α ≃*o β} {f₁ f₂ : β ≃*o γ} (hg : Function.Surjective g) : g.trans f₁ = g.trans f₂ ↔ f₁ = f₂

Full source

@[to_additive (attr := simp)]
theorem cancel_left {g : α ≃*o β} {f₁ f₂ : β ≃*o γ} (hg : Function.Surjective g) :
    g.trans f₁ = g.trans f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext <| hg.forall.2 <| DFunLike.ext_iff.1 h, fun _ => by congr⟩

Left Cancellation Property for Composition of Ordered Monoid Isomorphisms

Informal description

Let $g : \alpha \simeq^* \beta$ be a surjective ordered monoid isomorphism, and let $f_1, f_2 : \beta \simeq^* \gamma$ be two ordered monoid isomorphisms. Then the composition $g \circ f_1$ equals $g \circ f_2$ if and only if $f_1 = f_2$.

OrderMonoidIso.toMulEquiv_eq_coe theorem

(f : α ≃*o β) : f.toMulEquiv = f

Full source

@[to_additive (attr := simp)]
theorem toMulEquiv_eq_coe (f : α ≃*o β) : f.toMulEquiv = f :=
  rfl

Ordered Monoid Isomorphism as Multiplicative Equivalence: $f.\text{toMulEquiv} = f$

Informal description

For any ordered monoid isomorphism $f : \alpha \simeq^* \beta$, the underlying multiplicative equivalence obtained from $f$ is equal to $f$ itself.

OrderMonoidIso.toOrderIso_eq_coe theorem

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

Full source

@[to_additive (attr := simp)]
theorem toOrderIso_eq_coe (f : α ≃*o β) : f.toOrderIso = f :=
  rfl

Ordered Monoid Isomorphism as Order Isomorphism: $f.\text{toOrderIso} = f$

Informal description

For any ordered monoid isomorphism $f : \alpha \simeq^* \beta$, the underlying order isomorphism obtained from $f$ is equal to $f$ itself.

OrderMonoidIso.symm definition

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

Full source

/-- The inverse of an isomorphism is an isomorphism. -/
@[to_additive (attr := symm) "The inverse of an order isomorphism is an order isomorphism."]
def symm (f : α ≃*o β) : β ≃*o α :=
  ⟨f.toMulEquiv.symm, f.toOrderIso.symm.map_rel_iff⟩

Inverse of an ordered monoid isomorphism

Informal description

Given an ordered monoid isomorphism $f : \alpha \simeq^* \beta$, its inverse $f^{-1} : \beta \simeq^* \alpha$ is also an ordered monoid isomorphism, preserving both the multiplicative structure and the order relation.

OrderMonoidIso.Simps.apply definition

(h : α ≃*o β) : α → β

Full source

/-- See Note [custom simps projection]. -/
@[to_additive "See Note [custom simps projection]."]
def Simps.apply (h : α ≃*o β) : α → β :=
  h

Application of an ordered monoid isomorphism

Informal description

The function that applies an ordered monoid isomorphism $h : \alpha \simeq^* \beta$ to an element of $\alpha$, yielding an element of $\beta$.

OrderMonoidIso.Simps.symm_apply definition

(h : α ≃*o β) : β → α

Full source

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

Inverse application of an ordered monoid isomorphism

Informal description

Given an ordered monoid isomorphism $ h : \alpha \simeq^* \beta $, the function maps an element of $ \beta $ to its preimage in $ \alpha $ under $ h $.

OrderMonoidIso.invFun_eq_symm theorem

{f : α ≃*o β} : f.invFun = f.symm

Full source

@[to_additive]
theorem invFun_eq_symm {f : α ≃*o β} : f.invFun = f.symm := rfl

Inverse Function Equals Symmetric Isomorphism in Ordered Monoids

Informal description

For any ordered monoid isomorphism $f : \alpha \simeq^* \beta$, the inverse function $f^{-1}$ of $f$ is equal to the symmetric isomorphism $f^{\text{sym}} : \beta \simeq^* \alpha$.

OrderMonoidIso.coe_toEquiv_symm theorem

(f : α ≃*o β) : ((f : α ≃ β).symm : β → α) = f.symm

Full source

/-- `simp`-normal form of `invFun_eq_symm`. -/
@[to_additive (attr := simp)]
theorem coe_toEquiv_symm (f : α ≃*o β) : ((f : α ≃ β).symm : β → α) = f.symm := rfl

Inverse of Ordered Monoid Isomorphism as Equivalence Matches Algebraic Inverse

Informal description

For any ordered monoid isomorphism $f : \alpha \simeq^* \beta$, the inverse function of $f$ (when viewed as an equivalence $\alpha \simeq \beta$) is equal to $f^{-1}$ (the inverse isomorphism in $\beta \simeq^* \alpha$). That is, $(f^{-1} : \beta \to \alpha) = f^{-1}$.

OrderMonoidIso.equivLike_inv_eq_symm theorem

(f : α ≃*o β) : EquivLike.inv f = f.symm

Full source

@[to_additive (attr := simp)]
theorem equivLike_inv_eq_symm (f : α ≃*o β) : EquivLike.inv f = f.symm := rfl

Inverse of Ordered Monoid Isomorphism via `EquivLike` Equals Symmetric Isomorphism

Informal description

For any ordered monoid isomorphism $f : \alpha \simeq^* \beta$, the inverse function defined by the `EquivLike` structure coincides with the inverse isomorphism $f^{-1} : \beta \simeq^* \alpha$ defined by the `OrderMonoidIso` structure, i.e., $\text{inv}(f) = f^{-1}$.

OrderMonoidIso.toEquiv_symm theorem

(f : α ≃*o β) : (f.symm : β ≃ α) = (f : α ≃ β).symm

Full source

@[to_additive (attr := simp)]
theorem toEquiv_symm (f : α ≃*o β) : (f.symm : β ≃ α) = (f : α ≃ β).symm := rfl

Inverse of Ordered Monoid Isomorphism Equals Inverse of Underlying Equivalence

Informal description

For any ordered monoid isomorphism $f : \alpha \simeq^* \beta$, the underlying equivalence of the inverse isomorphism $f^{-1} : \beta \simeq^* \alpha$ is equal to the inverse of the underlying equivalence of $f$. In other words, $(f^{-1} : \beta \simeq \alpha) = (f : \alpha \simeq \beta)^{-1}$.

OrderMonoidIso.symm_symm theorem

(f : α ≃*o β) : f.symm.symm = f

Full source

@[to_additive (attr := simp)]
theorem symm_symm (f : α ≃*o β) : f.symm.symm = f := rfl

Double Inverse of Ordered Monoid Isomorphism

Informal description

For any ordered monoid isomorphism $f : \alpha \simeq^* \beta$, the inverse of the inverse of $f$ is equal to $f$ itself, i.e., $(f^{-1})^{-1} = f$.

OrderMonoidIso.symm_bijective theorem

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

Full source

@[to_additive]
theorem symm_bijective : Function.Bijective (symm : (α ≃*o β) → β ≃*o α) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Operation on Ordered Monoid Isomorphisms

Informal description

The function that maps an ordered monoid isomorphism $f : \alpha \simeq^* \beta$ to its inverse $f^{-1} : \beta \simeq^* \alpha$ is bijective.

OrderMonoidIso.refl_symm theorem

: (OrderMonoidIso.refl α).symm = .refl α

Full source

@[to_additive (attr := simp)]
theorem refl_symm : (OrderMonoidIso.refl α).symm = .refl α := rfl

Inverse of Identity Ordered Monoid Isomorphism is Identity

Informal description

The inverse of the identity ordered monoid isomorphism on $\alpha$ is equal to the identity ordered monoid isomorphism on $\alpha$.

OrderMonoidIso.apply_symm_apply theorem

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

Full source

/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`. -/
@[to_additive (attr := simp) "`e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`."]
theorem apply_symm_apply (e : α ≃*o β) (y : β) : e (e.symm y) = y :=
  e.toEquiv.apply_symm_apply y

Right Inverse Property of Ordered Monoid Isomorphisms

Informal description

For any ordered monoid isomorphism $e : \alpha \simeq^* \beta$ and any element $y \in \beta$, applying $e$ to the inverse image $e^{-1}(y)$ recovers the original element $y$, i.e., $e(e^{-1}(y)) = y$.

OrderMonoidIso.symm_apply_apply theorem

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

Full source

/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`. -/
@[to_additive (attr := simp) "`e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`."]
theorem symm_apply_apply (e : α ≃*o β) (x : α) : e.symm (e x) = x :=
  e.toEquiv.symm_apply_apply x

Inverse of Ordered Monoid Isomorphism Recovers Original Element

Informal description

For any ordered monoid isomorphism $e : \alpha \simeq^* \beta$ and any element $x \in \alpha$, the inverse isomorphism $e^{-1}$ satisfies $e^{-1}(e(x)) = x$.

OrderMonoidIso.symm_comp_self theorem

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

Full source

@[to_additive (attr := simp)]
theorem symm_comp_self (e : α ≃*o β) : e.symm ∘ e = id :=
  funext e.symm_apply_apply

Inverse Composition Yields Identity for Ordered Monoid Isomorphisms

Informal description

For any ordered monoid isomorphism $e : \alpha \simeq^* \beta$, the composition of $e$ with its inverse $e^{-1}$ is the identity function on $\alpha$, i.e., $e^{-1} \circ e = \text{id}$.

OrderMonoidIso.self_comp_symm theorem

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

Full source

@[to_additive (attr := simp)]
theorem self_comp_symm (e : α ≃*o β) : e ∘ e.symm = id :=
  funext e.apply_symm_apply

Composition of Ordered Monoid Isomorphism with its Inverse Yields Identity

Informal description

For any ordered monoid isomorphism $e : \alpha \simeq^* \beta$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity function on $\beta$, i.e., $e \circ e^{-1} = \text{id}$.

OrderMonoidIso.apply_eq_iff_symm_apply theorem

(e : α ≃*o β) {x : α} {y : β} : e x = y ↔ x = e.symm y

Full source

@[to_additive]
theorem apply_eq_iff_symm_apply (e : α ≃*o β) {x : α} {y : β} : e x = y ↔ x = e.symm y :=
  e.toEquiv.apply_eq_iff_eq_symm_apply

Ordered Monoid Isomorphism Application Equality: $e(x) = y \leftrightarrow x = e^{-1}(y)$

Informal description

For any ordered monoid isomorphism $e : \alpha \simeq^* \beta$ and elements $x \in \alpha$, $y \in \beta$, the equality $e(x) = y$ holds if and only if $x = e^{-1}(y)$, where $e^{-1}$ is the inverse isomorphism of $e$.

OrderMonoidIso.symm_apply_eq theorem

(e : α ≃*o β) {x y} : e.symm x = y ↔ x = e y

Full source

@[to_additive]
theorem symm_apply_eq (e : α ≃*o β) {x y} : e.symm x = y ↔ x = e y :=
  e.toEquiv.symm_apply_eq

Inverse Characterization for Ordered Monoid Isomorphisms: $e^{-1}(x) = y \leftrightarrow x = e(y)$

Informal description

For any ordered monoid isomorphism $e : \alpha \simeq^* \beta$ and elements $x \in \beta$, $y \in \alpha$, the equality $e^{-1}(x) = y$ holds if and only if $x = e(y)$.

OrderMonoidIso.comp_symm_eq theorem

(e : α ≃*o β) (f : β → α) (g : α → α) : g ∘ e.symm = f ↔ g = f ∘ e

Full source

@[to_additive]
theorem comp_symm_eq (e : α ≃*o β) (f : β → α) (g : α → α) :
    g ∘ e.symmg ∘ e.symm = f ↔ g = f ∘ e :=
  e.toEquiv.comp_symm_eq f g

Composition with Inverse Isomorphism Condition for Ordered Monoids

Informal description

Let $\alpha$ and $\beta$ be ordered monoids (or groups), and let $e : \alpha \simeq^* \beta$ be an order-preserving monoid isomorphism. For any functions $f : \beta \to \alpha$ and $g : \alpha \to \alpha$, the composition $g \circ e^{-1}$ equals $f$ if and only if $g$ equals $f \circ e$.

OrderMonoidIso.symm_comp_eq theorem

(e : α ≃*o β) (f : α → α) (g : α → β) : e.symm ∘ g = f ↔ g = e ∘ f

Full source

@[to_additive]
theorem symm_comp_eq (e : α ≃*o β) (f : α → α) (g : α → β) :
    e.symm ∘ ge.symm ∘ g = f ↔ g = e ∘ f :=
  e.toEquiv.symm_comp_eq f g

Characterization of Composition with Inverse Ordered Monoid Isomorphism: $e^{-1} \circ g = f \leftrightarrow g = e \circ f$

Informal description

Let $e : \alpha \simeq^* \beta$ be an ordered monoid isomorphism, and let $f : \alpha \to \alpha$ and $g : \alpha \to \beta$ be functions. Then the composition $e^{-1} \circ g$ equals $f$ if and only if $g$ equals $e \circ f$.

OrderMonoidIso.strictMono theorem

: StrictMono f

Full source

@[to_additive]
protected lemma strictMono : StrictMono f :=
  strictMono_of_le_iff_le fun _ _ ↦ (map_le_map_iff _).symm

Ordered Monoid Isomorphisms are Strictly Monotone

Informal description

Let $f : \alpha \to \beta$ be an ordered monoid isomorphism between two preordered monoids (or groups). Then $f$ is strictly monotone, meaning that for any $x, y \in \alpha$, if $x < y$ then $f(x) < f(y)$.

OrderMonoidIso.strictMono_symm theorem

: StrictMono f.symm

Full source

@[to_additive]
protected lemma strictMono_symm : StrictMono f.symm :=
  strictMono_of_le_iff_le <| fun a b ↦ by
    rw [← map_le_map_iff f]
    convert Iff.rfl <;>
    exact f.toEquiv.apply_symm_apply _

Strict Monotonicity of the Inverse of an Ordered Monoid Isomorphism

Informal description

Let $f : \alpha \simeq^* \beta$ be an ordered monoid isomorphism between two preordered monoids (or groups). Then the inverse function $f^{-1} : \beta \to \alpha$ is strictly monotone, meaning that for any $x, y \in \beta$, if $x < y$ then $f^{-1}(x) < f^{-1}(y)$.

OrderMonoidIso.mk' definition

(f : α ≃ β) (hf : ∀ {a b}, f a ≤ f b ↔ a ≤ b) (map_mul : ∀ a b : α, f (a * b) = f a * f b) : α ≃*o β

Full source

/-- Makes an ordered group isomorphism from a proof that the map preserves multiplication. -/
@[to_additive
      "Makes an ordered additive group isomorphism from a proof that the map preserves
      addition."]
def mk' (f : α ≃ β) (hf : ∀ {a b}, f a ≤ f b ↔ a ≤ b) (map_mul : ∀ a b : α, f (a * b) = f a * f b) :
    α ≃*o β :=
  { MulEquiv.mk' f map_mul with map_le_map_iff' := hf }

Ordered monoid isomorphism from bijection preserving order and multiplication

Informal description

Given a bijection $f : \alpha \to \beta$ between two preordered monoids (or groups) that satisfies: 1. $f$ preserves the order relation (i.e., $f(a) \leq f(b) \leftrightarrow a \leq b$ for all $a, b \in \alpha$), 2. $f$ preserves the multiplication operation (i.e., $f(a \cdot b) = f(a) \cdot f(b)$ for all $a, b \in \alpha$), this constructs an ordered monoid isomorphism between $\alpha$ and $\beta$.

OrderMonoidWithZeroHom.instFunLike instance

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

Full source

instance : FunLike (α →*₀o β) α β where
  coe f := f.toFun
  coe_injective' f g h := by
    obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
    congr

Function-Like Structure for Order-Preserving Monoid with Zero Homomorphisms

Informal description

For any two preordered monoids with zero $\alpha$ and $\beta$, the type of order-preserving monoid with zero homomorphisms $\alpha \to*₀o \beta$ can be treated as a function-like type, where each homomorphism can be coerced to a function from $\alpha$ to $\beta$.

OrderMonoidWithZeroHom.instMonoidWithZeroHomClass instance

: MonoidWithZeroHomClass (α →*₀o β) α β

Full source

instance : MonoidWithZeroHomClass (α →*₀o β) α β where
  map_mul f := f.map_mul'
  map_one f := f.map_one'
  map_zero f := f.map_zero'

Order-Preserving Monoid with Zero Homomorphisms as MonoidWithZeroHomClass

Informal description

For any two preordered monoids with zero $\alpha$ and $\beta$, the type of order-preserving monoid with zero homomorphisms $\alpha \to*₀o \beta$ forms a `MonoidWithZeroHomClass`, meaning its elements preserve the multiplicative monoid with zero structure (including multiplication, zero, and one).

OrderMonoidWithZeroHom.instOrderHomClass instance

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

Full source

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

Order-Preserving Monoid with Zero Homomorphisms as Order-Preserving Maps

Informal description

For any two preordered monoids with zero $\alpha$ and $\beta$, the type of order-preserving monoid with zero homomorphisms $\alpha \to*₀o \beta$ forms an `OrderHomClass`, meaning its elements preserve both the order relation and the multiplicative monoid with zero structure.

OrderMonoidWithZeroHom.ext theorem

(h : ∀ a, f a = g a) : f = g

Full source

@[ext]
theorem ext (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

Extensionality of Order-Preserving Monoid with Zero Homomorphisms

Informal description

For any two order-preserving monoid with zero homomorphisms $f, g \colon \alpha \to*₀o \beta$, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

OrderMonoidWithZeroHom.toFun_eq_coe theorem

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

Full source

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

Equality of Underlying Function and Coercion for Order-Preserving Monoid with Zero Homomorphisms

Informal description

For any order-preserving monoid with zero homomorphism $f \colon \alpha \to*₀o \beta$, the underlying function $f.\text{toFun}$ is equal to the coercion of $f$ to a function $\alpha \to \beta$.

OrderMonoidWithZeroHom.coe_mk theorem

(f : α →*₀ β) (h) : (OrderMonoidWithZeroHom.mk f h : α → β) = f

Full source

@[simp]
theorem coe_mk (f : α →*₀ β) (h) : (OrderMonoidWithZeroHom.mk f h : α → β) = f :=
  rfl

Coercion of Constructed Ordered Monoid with Zero Homomorphism Equals Original Function

Informal description

For any monoid with zero homomorphism $f \colon \alpha \to*₀ \beta$ and order-preserving property $h$, the coercion of the constructed ordered monoid with zero homomorphism $\text{OrderMonoidWithZeroHom.mk}\ f\ h$ to a function $\alpha \to \beta$ equals $f$.

OrderMonoidWithZeroHom.mk_coe theorem

(f : α →*₀o β) (h) : OrderMonoidWithZeroHom.mk (f : α →*₀ β) h = f

Full source

@[simp]
theorem mk_coe (f : α →*₀o β) (h) : OrderMonoidWithZeroHom.mk (f : α →*₀ β) h = f := rfl

Construction of Ordered Monoid with Zero Homomorphism from Underlying Homomorphism Preserves Identity

Informal description

For any order-preserving monoid with zero homomorphism $f \colon \alpha \to*₀o \beta$ and order-preserving property $h$, the construction of an ordered monoid with zero homomorphism from the underlying monoid with zero homomorphism $(f \colon \alpha \to*₀ \beta)$ and $h$ yields $f$ itself.

OrderMonoidWithZeroHom.toOrderMonoidHom definition

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

Full source

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

Reinterpretation of ordered monoid with zero homomorphism as ordered monoid homomorphism

Informal description

Given an ordered monoid with zero homomorphism $f : \alpha \to \beta$, this function reinterprets $f$ as an ordered monoid homomorphism by forgetting the preservation of the zero element.

OrderMonoidWithZeroHom.coe_monoidWithZeroHom theorem

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

Full source

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

Underlying Monoid with Zero Homomorphism of Ordered Homomorphism is Itself

Informal description

For any order-preserving monoid with zero homomorphism $f \colon \alpha \to*₀o \beta$, the underlying monoid with zero homomorphism $(f \colon \alpha \to*₀ \beta)$ is equal to $f$ when both are viewed as functions from $\alpha$ to $\beta$.

OrderMonoidWithZeroHom.coe_orderMonoidHom theorem

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

Full source

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

Underlying Function of Ordered Monoid Homomorphism is Itself

Informal description

For any ordered monoid with zero homomorphism $f \colon \alpha \to*₀o \beta$, the underlying function of $f$ when viewed as an ordered monoid homomorphism (via the forgetful functor) is equal to $f$ itself.

OrderMonoidWithZeroHom.toOrderMonoidHom_injective theorem

: Injective (toOrderMonoidHom : _ → α →*o β)

Full source

theorem toOrderMonoidHom_injective : Injective (toOrderMonoidHom : _ → α →*o β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

Injectivity of the Reinterpretation from Ordered Monoid with Zero Homomorphisms to Ordered Monoid Homomorphisms

Informal description

The function `toOrderMonoidHom`, which maps an ordered monoid with zero homomorphism $f \colon \alpha \to*₀o \beta$ to an ordered monoid homomorphism, is injective. That is, if $f$ and $g$ are ordered monoid with zero homomorphisms such that their reinterpretations as ordered monoid homomorphisms are equal, then $f = g$.

OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective theorem

: Injective (toMonoidWithZeroHom : _ → α →*₀ β)

Full source

theorem toMonoidWithZeroHom_injective : Injective (toMonoidWithZeroHom : _ → α →*₀ β) :=
  fun f g h => ext <| by convert DFunLike.ext_iff.1 h using 0

Injectivity of the Canonical Map from Order-Preserving to Plain Monoid with Zero Homomorphisms

Informal description

The canonical map from order-preserving monoid with zero homomorphisms $\alpha \to*₀o \beta$ to monoid with zero homomorphisms $\alpha \to*₀ \beta$ is injective. In other words, if two order-preserving monoid with zero homomorphisms $f$ and $g$ are equal as monoid with zero homomorphisms, then they are equal as order-preserving monoid with zero homomorphisms.

OrderMonoidWithZeroHom.copy definition

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

Full source

/-- Copy of an `OrderMonoidWithZeroHom` 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.toOrderMonoidHom.copy f' h, f.toMonoidWithZeroHom.copy f' h with toFun := f' }

Copy of an ordered monoid with zero homomorphism with a new function

Informal description

Given an ordered monoid with zero homomorphism $f \colon \alpha \to \beta$ between preordered monoids with zero $\alpha$ and $\beta$, and a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, the function `OrderMonoidWithZeroHom.copy` constructs a new ordered monoid with zero homomorphism with the underlying function $f'$ that preserves both the multiplicative, zero, and order structures. This is useful for fixing definitional equalities while maintaining the homomorphism structure.

OrderMonoidWithZeroHom.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 Ordered Monoid with Zero Homomorphism Equals Input Function

Informal description

Given an ordered monoid with zero homomorphism $f \colon \alpha \to \beta$ between preordered monoids with zero $\alpha$ and $\beta$, a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, and a proof $h$ that $f' = f$, the underlying function of the copied homomorphism $f.copy\ f'\ h$ is equal to $f'$.

OrderMonoidWithZeroHom.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 Ordered Monoid with Zero Homomorphism Equals Original

Informal description

Let $\alpha$ and $\beta$ be preordered monoids with zero, and let $f \colon \alpha \to \beta$ be an ordered monoid with zero homomorphism. For any function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with underlying function $f'$ is equal to $f$ itself.

OrderMonoidWithZeroHom.id definition

: α →*₀o α

Full source

/-- The identity map as an ordered monoid with zero homomorphism. -/
protected def id : α →*₀o α :=
  { MonoidWithZeroHom.id α, OrderHom.id with }

Identity ordered monoid with zero homomorphism

Informal description

The identity function on a preordered monoid with zero $\alpha$, viewed as a bundled ordered monoid with zero homomorphism from $\alpha$ to itself. That is, the function $\operatorname{id} : \alpha \to \alpha$ together with proofs that it preserves multiplication, zero, one, and the order relation.

OrderMonoidWithZeroHom.coe_id theorem

: ⇑(OrderMonoidWithZeroHom.id α) = id

Full source

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

Identity Ordered Monoid with Zero Homomorphism is Identity Function

Informal description

The underlying function of the identity ordered monoid with zero homomorphism from a preordered monoid with zero $\alpha$ to itself is equal to the identity function $\operatorname{id} : \alpha \to \alpha$.

OrderMonoidWithZeroHom.instInhabited instance

: Inhabited (α →*₀o α)

Full source

instance : Inhabited (α →*₀o α) :=
  ⟨OrderMonoidWithZeroHom.id α⟩

Inhabited Type of Ordered Monoid with Zero Endomorphisms

Informal description

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

OrderMonoidWithZeroHom.comp definition

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

Full source

/-- Composition of `OrderMonoidWithZeroHom`s as an `OrderMonoidWithZeroHom`. -/
def comp (f : β →*₀o γ) (g : α →*₀o β) : α →*₀o γ :=
  { f.toMonoidWithZeroHom.comp (g : α →*₀ β), f.toOrderMonoidHom.comp (g : α →*o β) with }

Composition of ordered monoid with zero homomorphisms

Informal description

Given ordered monoid with zero homomorphisms $ f \colon \beta \to^*_0 \gamma $ and $ g \colon \alpha \to^*_0 \beta $, their composition $ f \circ g \colon \alpha \to^*_0 \gamma $ is defined as the ordered monoid with zero homomorphism whose underlying function is the composition of the underlying functions of $ f $ and $ g $, and which preserves both the order and the monoid with zero structure.

OrderMonoidWithZeroHom.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 Ordered Monoid with Zero Homomorphisms Preserves Underlying Function

Informal description

For any ordered monoid with zero homomorphisms $ f \colon \beta \to^*_0 \gamma $ and $ g \colon \alpha \to^*_0 \beta $, the underlying function of their composition $ f \circ g \colon \alpha \to^*_0 \gamma $ is equal to the composition of the underlying functions $ f \circ g \colon \alpha \to \gamma $.

OrderMonoidWithZeroHom.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 Ordered Monoid with Zero Homomorphisms Preserves Application

Informal description

For any ordered monoid with zero homomorphisms $f \colon \beta \to^*_0 \gamma$ and $g \colon \alpha \to^*_0 \beta$, and for any element $a \in \alpha$, the composition $(f \circ g)(a)$ equals $f(g(a))$.

OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom theorem

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

Full source

theorem coe_comp_monoidWithZeroHom (f : β →*₀o γ) (g : α →*₀o β) :
    (f.comp g : α →*₀ γ) = (f : β →*₀ γ).comp g :=
  rfl

Composition of Underlying Monoid with Zero Homomorphisms Preserves Order-Preserving Homomorphisms

Informal description

For any two order-preserving monoid with zero homomorphisms $f \colon \beta \to^*_0 \gamma$ and $g \colon \alpha \to^*_0 \beta$, the underlying monoid with zero homomorphism of their composition $f \circ g \colon \alpha \to^*_0 \gamma$ is equal to the composition of the underlying monoid with zero homomorphisms of $f$ and $g$.

OrderMonoidWithZeroHom.coe_comp_orderMonoidHom theorem

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

Full source

theorem coe_comp_orderMonoidHom (f : β →*₀o γ) (g : α →*₀o β) :
    (f.comp g : α →*o γ) = (f : β →*o γ).comp g :=
  rfl

Compatibility of Composition with Underlying Ordered Monoid Homomorphisms

Informal description

Let $f \colon \beta \to^*_0 \gamma$ and $g \colon \alpha \to^*_0 \beta$ be ordered monoid with zero homomorphisms. Then the underlying ordered monoid homomorphism of their composition $f \circ g \colon \alpha \to^*_0 \gamma$ is equal to the composition of the underlying ordered monoid homomorphisms of $f$ and $g$.

OrderMonoidWithZeroHom.comp_assoc theorem

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

Full source

@[simp]
theorem comp_assoc (f : γ →*₀o δ) (g : β →*₀o γ) (h : α →*₀o β) :
    (f.comp g).comp h = f.comp (g.comp h) :=
  rfl

Associativity of Composition for Ordered Monoid with Zero Homomorphisms

Informal description

For any ordered monoid with zero homomorphisms $f \colon \gamma \to^*_0 \delta$, $g \colon \beta \to^*_0 \gamma$, and $h \colon \alpha \to^*_0 \beta$, the composition of homomorphisms is associative, i.e., $(f \circ g) \circ h = f \circ (g \circ h)$.

OrderMonoidWithZeroHom.comp_id theorem

(f : α →*₀o β) : f.comp (OrderMonoidWithZeroHom.id α) = f

Full source

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

Right Identity Law for Ordered Monoid with Zero Homomorphisms

Informal description

For any ordered monoid with zero homomorphism $f \colon \alpha \to^*_0 \beta$, the composition of $f$ with the identity homomorphism on $\alpha$ equals $f$. That is, $f \circ \mathrm{id} = f$.

OrderMonoidWithZeroHom.id_comp theorem

(f : α →*₀o β) : (OrderMonoidWithZeroHom.id β).comp f = f

Full source

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

Identity Homomorphism is Left Neutral Element for Composition

Informal description

For any ordered monoid with zero homomorphism $f \colon \alpha \to^*_0 \beta$, the composition of the identity homomorphism on $\beta$ with $f$ equals $f$ itself, i.e., $\operatorname{id}_\beta \circ f = f$.

OrderMonoidWithZeroHom.cancel_right theorem

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

Full source

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

Right Cancellation Property for Ordered Monoid with Zero Homomorphisms

Informal description

Let $f \colon \alpha \to^*_0 \beta$ be a surjective ordered monoid with zero homomorphism, and let $g_1, g_2 \colon \beta \to^*_0 \gamma$ be two ordered monoid with zero homomorphisms. Then the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

OrderMonoidWithZeroHom.cancel_left theorem

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

Full source

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

Left Cancellation Property for Ordered Monoid with Zero Homomorphisms

Informal description

Let $g \colon \beta \to^*_0 \gamma$ be an injective ordered monoid with zero homomorphism, and let $f_1, f_2 \colon \alpha \to^*_0 \beta$ be two ordered monoid with zero homomorphisms. Then the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.

OrderMonoidWithZeroHom.instMul instance

: Mul (α →*₀o β)

Full source

/-- For two ordered monoid morphisms `f` and `g`, their product is the ordered monoid morphism
sending `a` to `f a * g a`. -/
instance : Mul (α →*₀o β) :=
  ⟨fun f g => { (f * g : α →*₀ β) with monotone' := f.monotone'.mul' g.monotone' }⟩

Multiplication of Ordered Monoid with Zero Homomorphisms

Informal description

For two ordered monoid with zero homomorphisms $f$ and $g$ between preordered monoids with zero $\alpha$ and $\beta$, their product is the ordered monoid with zero homomorphism that sends each element $a \in \alpha$ to $f(a) \cdot g(a) \in \beta$.

OrderMonoidWithZeroHom.coe_mul theorem

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

Full source

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

Pointwise Product of Ordered Monoid with Zero Homomorphisms

Informal description

For any two ordered monoid with zero homomorphisms $f, g : \alpha \to \beta$, the underlying function of their product $f * g$ is equal to the pointwise product of the underlying functions of $f$ and $g$. That is, $(f * g)(a) = f(a) * g(a)$ for all $a \in \alpha$.

OrderMonoidWithZeroHom.mul_apply theorem

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

Full source

@[simp]
theorem mul_apply (f g : α →*₀o β) (a : α) : (f * g) a = f a * g a :=
  rfl

Evaluation of Product of Ordered Monoid with Zero Homomorphisms

Informal description

For any two order-preserving monoid with zero homomorphisms $f, g \colon \alpha \to \beta$ and any element $a \in \alpha$, the evaluation of their product homomorphism at $a$ is equal to the product of their evaluations, i.e., $(f \cdot g)(a) = f(a) \cdot g(a)$.

OrderMonoidWithZeroHom.mul_comp theorem

(g₁ g₂ : β →*₀o γ) (f : α →*₀o β) : (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

Full source

theorem mul_comp (g₁ g₂ : β →*₀o γ) (f : α →*₀o β) : (g₁ * g₂).comp f = g₁.comp f * g₂.comp f :=
  rfl

Composition Distributes Over Multiplication of Ordered Monoid with Zero Homomorphisms

Informal description

For any ordered monoid with zero homomorphisms $ g_1, g_2 \colon \beta \to^*_0 \gamma $ and $ f \colon \alpha \to^*_0 \beta $, the composition of the product $ g_1 \cdot g_2 $ with $ f $ is equal to the product of the compositions $ g_1 \circ f $ and $ g_2 \circ f $. That is, $(g_1 \cdot g_2) \circ f = (g_1 \circ f) \cdot (g_2 \circ f)$.

OrderMonoidWithZeroHom.comp_mul theorem

(g : β →*₀o γ) (f₁ f₂ : α →*₀o β) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Full source

theorem comp_mul (g : β →*₀o γ) (f₁ f₂ : α →*₀o β) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ :=
  ext fun _ => map_mul g _ _

Composition Distributes over Multiplication of Ordered Monoid with Zero Homomorphisms

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preordered monoids with zero. For any order-preserving monoid with zero homomorphism $g \colon \beta \to^*_0 \gamma$ and any two order-preserving monoid with zero homomorphisms $f_1, f_2 \colon \alpha \to^*_0 \beta$, the composition of $g$ with the product homomorphism $f_1 \cdot f_2$ equals the product of the compositions $g \circ f_1$ and $g \circ f_2$. That is, $$ g \circ (f_1 \cdot f_2) = (g \circ f_1) \cdot (g \circ f_2). $$

OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_coe theorem

(f : α →*₀o β) : f.toMonoidWithZeroHom = f

Full source

@[simp]
theorem toMonoidWithZeroHom_eq_coe (f : α →*₀o β) : f.toMonoidWithZeroHom = f := by
  rfl

Equality of Underlying Monoid with Zero Homomorphism and Original Function

Informal description

For any order-preserving monoid with zero homomorphism $f \colon \alpha \to*₀o \beta$, the underlying monoid with zero homomorphism $f$ (obtained via `toMonoidWithZeroHom`) is equal to $f$ itself when viewed as a function.

OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe theorem

(f : α →*₀o β) : f.toOrderMonoidHom = f

Full source

@[simp]
theorem toOrderMonoidHom_eq_coe (f : α →*₀o β) : f.toOrderMonoidHom = f :=
  rfl

Equality of Ordered Monoid Homomorphism and Original Function in Ordered Monoid with Zero Homomorphisms

Informal description

For any ordered monoid with zero homomorphism $f \colon \alpha \to*₀o \beta$, the underlying ordered monoid homomorphism obtained by forgetting the zero-preservation property is equal to $f$ itself when viewed as a function.

OrderMonoidIso.unitsWithZero definition

{α : Type*} [Group α] [Preorder α] : (WithZero α)ˣ ≃*o α

Full source

/-- Any ordered group is isomorphic to the units of itself adjoined with `0`. -/
@[simps!]
def OrderMonoidIso.unitsWithZero {α : Type*} [Group α] [Preorder α] : (WithZero α)ˣ(WithZero α)ˣ ≃*o α where
  toMulEquiv := WithZero.unitsWithZeroEquiv
  map_le_map_iff' {a b} := by simp [WithZero.unitsWithZeroEquiv]

Isomorphism between units of $\alpha$ with zero and $\alpha$

Informal description

For any ordered group $\alpha$, there is an order-preserving monoid isomorphism between the group of units of $\alpha$ with zero adjoined (denoted $(\alpha \cup \{0\})^\times$) and $\alpha$ itself. More precisely, the isomorphism $(\alpha \cup \{0\})^\times \simeq \alpha$ satisfies: 1. It is a bijection between the group of units of $\alpha \cup \{0\}$ and $\alpha$, 2. It preserves the multiplication operation, 3. It preserves the order structure (i.e., $a \leq b$ if and only if $f(a) \leq f(b)$).

Mathlib.Algebra.Order.Hom.Monoid

Types of morphisms

Notation

Implementation notes

Removed typeclasses

Tags