Ordered monoid and group homomorphisms

This file defines morphisms between (additive) ordered monoids with zero.

Types of morphisms

• OrderMonoidWithZeroHom: Ordered monoid with zero homomorphisms.

Notation

• →*₀o: Bundled ordered monoid with zero homs. Also use for group with zero homs.

TODO

• ≃*₀o: Bundled ordered monoid with zero isos. Also use for group with zero isos.

Tags

monoid with zero

structure OrderMonoidWithZeroHom (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] extends α →*₀ β : Type (max u_6 u_7)

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

• toFun : α → β
• map_zero' : (↑self.toMonoidWithZeroHom).toFun 0 = 0
• map_one' : (↑self.toMonoidWithZeroHom).toFun 1 = 1
• map_mul' (x y : α) : (↑self.toMonoidWithZeroHom).toFun (x * y) = (↑self.toMonoidWithZeroHom).toFun x * (↑self.toMonoidWithZeroHom).toFun y
• monotone' : Monotone (↑self.toMonoidWithZeroHom).toFun

  An OrderMonoidWithZeroHom is a monotone function.

def «term_→*₀o_» : Lean.TrailingParserDescr

Infix notation for OrderMonoidWithZeroHom.

Equations

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

def OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] [OrderHomClass F α β] [MonoidWithZeroHomClass F α β] (f : F) : α →*₀o β

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

Equations

• ↑f = { toMonoidWithZeroHom := ↑f, monotone' := ⋯ }

instance instCoeTCOrderMonoidWithZeroHomOfOrderHomClassOfMonoidWithZeroHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] [OrderHomClass F α β] [MonoidWithZeroHomClass F α β] : CoeTC F (α →*₀o β)

Equations

• instCoeTCOrderMonoidWithZeroHomOfOrderHomClassOfMonoidWithZeroHomClass = { coe := OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom }

instance OrderMonoidWithZeroHom.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] : FunLike (α →*₀o β) α β

Equations

• OrderMonoidWithZeroHom.instFunLike = { coe := fun (f : α →*₀o β) => (↑f.toMonoidWithZeroHom).toFun, coe_injective' := ⋯ }

instance OrderMonoidWithZeroHom.instMonoidWithZeroHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] : MonoidWithZeroHomClass (α →*₀o β) α β

instance OrderMonoidWithZeroHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] : OrderHomClass (α →*₀o β) α β

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

theorem OrderMonoidWithZeroHom.ext_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] {f g : α →*₀o β} : f = g ↔ ∀ (a : α), f a = g a

theorem OrderMonoidWithZeroHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) : (↑f.toMonoidWithZeroHom).toFun = ⇑f

@[simp]

theorem OrderMonoidWithZeroHom.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (h : Monotone (↑f).toFun) : ⇑{ toMonoidWithZeroHom := f, monotone' := h } = ⇑f

@[simp]

theorem OrderMonoidWithZeroHom.mk_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) (h : Monotone (↑↑f).toFun) : { toMonoidWithZeroHom := ↑f, monotone' := h } = f

def OrderMonoidWithZeroHom.toOrderMonoidHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) : α →*o β

Reinterpret an ordered monoid with zero homomorphism as an order monoid homomorphism.

Equations

• f.toOrderMonoidHom = { toFun := (↑f.toMonoidWithZeroHom).toFun, map_one' := ⋯, map_mul' := ⋯, monotone' := ⋯ }

@[simp]

theorem OrderMonoidWithZeroHom.coe_monoidWithZeroHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) : ⇑↑f = ⇑f

@[simp]

theorem OrderMonoidWithZeroHom.coe_orderMonoidHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) : ⇑↑f = ⇑f

theorem OrderMonoidWithZeroHom.toOrderMonoidHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] : Function.Injective toOrderMonoidHom

theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] : Function.Injective toMonoidWithZeroHom

def OrderMonoidWithZeroHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) (f' : α → β) (h : f' = ⇑f) : α →*o β

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

Equations

• f.copy f' h = { toFun := f', map_one' := ⋯, map_mul' := ⋯, monotone' := ⋯ }

@[simp]

theorem OrderMonoidWithZeroHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem OrderMonoidWithZeroHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = ↑f

def OrderMonoidWithZeroHom.id (α : Type u_2) [Preorder α] [MulZeroOneClass α] : α →*₀o α

The identity map as an ordered monoid with zero homomorphism.

Equations

• OrderMonoidWithZeroHom.id α = { toMonoidWithZeroHom := MonoidWithZeroHom.id α, monotone' := ⋯ }

@[simp]

theorem OrderMonoidWithZeroHom.coe_id (α : Type u_2) [Preorder α] [MulZeroOneClass α] : ⇑(OrderMonoidWithZeroHom.id α) = id

instance OrderMonoidWithZeroHom.instInhabited (α : Type u_2) [Preorder α] [MulZeroOneClass α] : Inhabited (α →*₀o α)

Equations

• OrderMonoidWithZeroHom.instInhabited α = { default := OrderMonoidWithZeroHom.id α }

def OrderMonoidWithZeroHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) : α →*₀o γ

Composition of OrderMonoidWithZeroHoms as an OrderMonoidWithZeroHom.

Equations

• f.comp g = { toMonoidWithZeroHom := f.comp ↑g, monotone' := ⋯ }

@[simp]

theorem OrderMonoidWithZeroHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem OrderMonoidWithZeroHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) (a : α) : (f.comp g) a = f (g a)

theorem OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) : ↑(f.comp g) = (↑f).comp ↑g

theorem OrderMonoidWithZeroHom.coe_comp_orderMonoidHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) : ↑(f.comp g) = (↑f).comp ↑g

@[simp]

theorem OrderMonoidWithZeroHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] [MulZeroOneClass δ] (f : γ →*₀o δ) (g : β →*₀o γ) (h : α →*₀o β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem OrderMonoidWithZeroHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) : f.comp (OrderMonoidWithZeroHom.id α) = f

@[simp]

theorem OrderMonoidWithZeroHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) : (OrderMonoidWithZeroHom.id β).comp f = f

@[simp]

theorem OrderMonoidWithZeroHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] {g₁ g₂ : β →*₀o γ} {f : α →*₀o β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem OrderMonoidWithZeroHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] {g : β →*₀o γ} {f₁ f₂ : α →*₀o β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

instance OrderMonoidWithZeroHom.instMul {α : Type u_2} {β : Type u_3} [LinearOrderedCommMonoidWithZero α] [LinearOrderedCommMonoidWithZero β] : Mul (α →*₀o β)

For two ordered monoid morphisms f and g, their product is the ordered monoid morphism sending a to f a * g a.

Equations

• OrderMonoidWithZeroHom.instMul = { mul := fun (f g : α →*₀o β) => let __src := ↑f * ↑g; { toMonoidWithZeroHom := __src, monotone' := ⋯ } }

@[simp]

theorem OrderMonoidWithZeroHom.coe_mul {α : Type u_2} {β : Type u_3} [LinearOrderedCommMonoidWithZero α] [LinearOrderedCommMonoidWithZero β] (f g : α →*₀o β) : ⇑(f * g) = ⇑f * ⇑g

@[simp]

theorem OrderMonoidWithZeroHom.mul_apply {α : Type u_2} {β : Type u_3} [LinearOrderedCommMonoidWithZero α] [LinearOrderedCommMonoidWithZero β] (f g : α →*₀o β) (a : α) : (f * g) a = f a * g a

theorem OrderMonoidWithZeroHom.mul_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LinearOrderedCommMonoidWithZero α] [LinearOrderedCommMonoidWithZero β] [LinearOrderedCommMonoidWithZero γ] (g₁ g₂ : β →*₀o γ) (f : α →*₀o β) : (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

theorem OrderMonoidWithZeroHom.comp_mul {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LinearOrderedCommMonoidWithZero α] [LinearOrderedCommMonoidWithZero β] [LinearOrderedCommMonoidWithZero γ] (g : β →*₀o γ) (f₁ f₂ : α →*₀o β) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

@[simp]

theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_coe {α : Type u_2} {β : Type u_3} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} (f : α →*₀o β) : f.toMonoidWithZeroHom = ↑f

@[simp]

theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_mk {α : Type u_2} {β : Type u_3} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} (f : α →*₀ β) (hf : Monotone ⇑f) : ↑{ toMonoidWithZeroHom := f, monotone' := hf } = f

@[simp]

theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} {hγ : Preorder γ} {hγ' : MulZeroOneClass γ} (f : β →*₀o γ) (g : α →*₀o β) : ↑(f.comp g) = (↑f).comp ↑g

@[simp]

theorem OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} (f : α →*₀o β) : f.toOrderMonoidHom = ↑f

@[simp]

theorem OrderMonoidWithZeroHom.toOrderMonoidHom_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} {hγ : Preorder γ} {hγ' : MulZeroOneClass γ} (f : β →*₀o γ) (g : α →*₀o β) : ↑(f.comp g) = (↑f).comp ↑g

def OrderMonoidIso.unitsWithZero {α : Type u_6} [Group α] [Preorder α] : (WithZero α)ˣ ≃*o α

Any ordered group is isomorphic to the units of itself adjoined with 0.

Equations

• OrderMonoidIso.unitsWithZero = { toMulEquiv := WithZero.unitsWithZeroEquiv, map_le_map_iff' := ⋯ }

@[simp]

theorem OrderMonoidIso.val_unitsWithZero_symm_apply {α : Type u_6} [Group α] [Preorder α] (a : α) : ↑(unitsWithZero.symm a) = ↑a

@[simp]

theorem OrderMonoidIso.val_inv_unitsWithZero_symm_apply {α : Type u_6} [Group α] [Preorder α] (a : α) : ↑(unitsWithZero.symm a)⁻¹ = (↑a)⁻¹

@[simp]

theorem OrderMonoidIso.unitsWithZero_apply {α : Type u_6} [Group α] [Preorder α] (a : (WithZero α)ˣ) : unitsWithZero a = WithZero.unzero ⋯

def OrderMonoidIso.withZero {G : Type u_6} {H : Type u_7} [Group G] [PartialOrder G] [Group H] [PartialOrder H] : (G ≃*o H) ≃ (WithZero G ≃*o WithZero H)

A version of Equiv.optionCongr for WithZero on OrderMonoidIso.

Equations

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

@[simp]

theorem OrderMonoidIso.withZero_symm_apply_apply {G : Type u_6} {H : Type u_7} [Group G] [PartialOrder G] [Group H] [PartialOrder H] (e : WithZero G ≃*o WithZero H) (x : G) : (withZero.symm e) x = WithZero.unzero ⋯

@[simp]

theorem OrderMonoidIso.withZero_symm_apply_symm_apply {G : Type u_6} {H : Type u_7} [Group G] [PartialOrder G] [Group H] [PartialOrder H] (e : WithZero G ≃*o WithZero H) (x : H) : (withZero.symm e).symm x = WithZero.unzero ⋯

@[simp]

theorem OrderMonoidIso.withZero_apply_symm_apply {G : Type u_6} {H : Type u_7} [Group G] [PartialOrder G] [Group H] [PartialOrder H] (e : G ≃*o H) (a : WithZero H) : (withZero e).symm a = (WithZero.map' ↑(↑e).symm) a

@[simp]

theorem OrderMonoidIso.withZero_apply_apply {G : Type u_6} {H : Type u_7} [Group G] [PartialOrder G] [Group H] [PartialOrder H] (e : G ≃*o H) (a : WithZero G) : (withZero e) a = (WithZero.map' ↑↑e) a

def OrderMonoidIso.withZeroUnits {α : Type u_6} [LinearOrderedCommGroupWithZero α] [DecidablePred fun (a : α) => a = 0] : WithZero αˣ ≃*o α

Any linearly ordered group with zero is isomorphic to adjoining 0 to the units of itself.

Equations

• OrderMonoidIso.withZeroUnits = { toMulEquiv := WithZero.withZeroUnitsEquiv, map_le_map_iff' := ⋯ }

@[simp]

theorem OrderMonoidIso.withZeroUnits_symm_apply {α : Type u_6} [LinearOrderedCommGroupWithZero α] [DecidablePred fun (a : α) => a = 0] (a : α) : withZeroUnits.symm a = if h : a = 0 then 0 else ↑(Units.mk0 a h)

@[simp]

theorem OrderMonoidIso.withZeroUnits_apply {α : Type u_6} [LinearOrderedCommGroupWithZero α] [DecidablePred fun (a : α) => a = 0] (n : WithZero αˣ) : withZeroUnits n = WithZero.recZeroCoe 0 Units.val n