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_mul' (x y : α) : (↑self.toMonoidWithZeroHom).toFun (x * y) = (↑self.toMonoidWithZeroHom).toFun x * (↑self.toMonoidWithZeroHom).toFun y
- monotone' : Monotone (↑self.toMonoidWithZeroHom).toFun
An
OrderMonoidWithZeroHomis a monotone function.
Instances For
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)
:
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
Instances For
instance
instCoeTCOrderMonoidWithZeroHomOfOrderHomClassOfMonoidWithZeroHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
[FunLike F α β]
[OrderHomClass F α β]
[MonoidWithZeroHomClass F α β]
:
Equations
instance
OrderMonoidWithZeroHom.instFunLike
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
:
Equations
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)
:
theorem
OrderMonoidWithZeroHom.ext_iff
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
{f g : α →*₀o β}
:
theorem
OrderMonoidWithZeroHom.toFun_eq_coe
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
(f : α →*₀o β)
:
@[simp]
theorem
OrderMonoidWithZeroHom.coe_mk
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
(f : α →*₀ β)
(h : Monotone (↑f).toFun)
:
@[simp]
theorem
OrderMonoidWithZeroHom.mk_coe
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
(f : α →*₀o β)
(h : Monotone (↑↑f).toFun)
:
def
OrderMonoidWithZeroHom.toOrderMonoidHom
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
(f : α →*₀o β)
:
Reinterpret an ordered monoid with zero homomorphism as an order monoid homomorphism.
Equations
Instances For
@[simp]
theorem
OrderMonoidWithZeroHom.coe_monoidWithZeroHom
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
(f : α →*₀o β)
:
@[simp]
theorem
OrderMonoidWithZeroHom.coe_orderMonoidHom
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
(f : α →*₀o β)
:
theorem
OrderMonoidWithZeroHom.toOrderMonoidHom_injective
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
:
theorem
OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
:
def
OrderMonoidWithZeroHom.copy
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
(f : α →*₀o β)
(f' : α → β)
(h : f' = ⇑f)
:
Copy of an OrderMonoidWithZeroHom with a new toFun equal to the old one. Useful to fix
definitional equalities.
Equations
Instances For
@[simp]
theorem
OrderMonoidWithZeroHom.coe_copy
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
(f : α →*₀o β)
(f' : α → β)
(h : f' = ⇑f)
:
theorem
OrderMonoidWithZeroHom.copy_eq
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
(f : α →*₀o β)
(f' : α → β)
(h : f' = ⇑f)
:
The identity map as an ordered monoid with zero homomorphism.
Equations
Instances For
@[simp]
Equations
def
OrderMonoidWithZeroHom.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulZeroOneClass α]
[MulZeroOneClass β]
[MulZeroOneClass γ]
(f : β →*₀o γ)
(g : α →*₀o β)
:
Composition of OrderMonoidWithZeroHoms as an OrderMonoidWithZeroHom.
Equations
Instances For
@[simp]
theorem
OrderMonoidWithZeroHom.coe_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulZeroOneClass α]
[MulZeroOneClass β]
[MulZeroOneClass γ]
(f : β →*₀o γ)
(g : α →*₀o β)
:
@[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 : α)
:
theorem
OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulZeroOneClass α]
[MulZeroOneClass β]
[MulZeroOneClass γ]
(f : β →*₀o γ)
(g : α →*₀o β)
:
theorem
OrderMonoidWithZeroHom.coe_comp_orderMonoidHom
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulZeroOneClass α]
[MulZeroOneClass β]
[MulZeroOneClass γ]
(f : β →*₀o γ)
(g : α →*₀o β)
:
@[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 β)
:
@[simp]
theorem
OrderMonoidWithZeroHom.comp_id
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
(f : α →*₀o β)
:
@[simp]
theorem
OrderMonoidWithZeroHom.id_comp
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
(f : α →*₀o β)
:
@[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)
:
@[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)
:
instance
OrderMonoidWithZeroHom.instMul
{α : Type u_2}
{β : Type u_3}
[LinearOrderedCommMonoidWithZero α]
[LinearOrderedCommMonoidWithZero β]
:
For two ordered monoid morphisms f and g, their product is the ordered monoid morphism
sending a to f a * g a.
Equations
@[simp]
theorem
OrderMonoidWithZeroHom.coe_mul
{α : Type u_2}
{β : Type u_3}
[LinearOrderedCommMonoidWithZero α]
[LinearOrderedCommMonoidWithZero β]
(f g : α →*₀o β)
:
@[simp]
theorem
OrderMonoidWithZeroHom.mul_apply
{α : Type u_2}
{β : Type u_3}
[LinearOrderedCommMonoidWithZero α]
[LinearOrderedCommMonoidWithZero β]
(f g : α →*₀o β)
(a : α)
:
theorem
OrderMonoidWithZeroHom.mul_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[LinearOrderedCommMonoidWithZero α]
[LinearOrderedCommMonoidWithZero β]
[LinearOrderedCommMonoidWithZero γ]
(g₁ g₂ : β →*₀o γ)
(f : α →*₀o β)
:
theorem
OrderMonoidWithZeroHom.comp_mul
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[LinearOrderedCommMonoidWithZero α]
[LinearOrderedCommMonoidWithZero β]
[LinearOrderedCommMonoidWithZero γ]
(g : β →*₀o γ)
(f₁ f₂ : α →*₀o β)
:
@[simp]
theorem
OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_coe
{α : Type u_2}
{β : Type u_3}
{hα : Preorder α}
{hα' : MulZeroOneClass α}
{hβ : Preorder β}
{hβ' : MulZeroOneClass β}
(f : α →*₀o β)
:
@[simp]
theorem
OrderMonoidWithZeroHom.toMonoidWithZeroHom_mk
{α : Type u_2}
{β : Type u_3}
{hα : Preorder α}
{hα' : MulZeroOneClass α}
{hβ : Preorder β}
{hβ' : MulZeroOneClass β}
(f : α →*₀ β)
(hf : Monotone ⇑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 β)
:
@[simp]
theorem
OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe
{α : Type u_2}
{β : Type u_3}
{hα : Preorder α}
{hα' : MulZeroOneClass α}
{hβ : Preorder β}
{hβ' : MulZeroOneClass β}
(f : α →*₀o β)
:
@[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 β)
:
Any ordered group is isomorphic to the units of itself adjoined with 0.
Equations
Instances For
@[simp]
@[simp]
theorem
OrderMonoidIso.val_inv_unitsWithZero_symm_apply
{α : Type u_6}
[Group α]
[Preorder α]
(a : α)
:
def
OrderMonoidIso.withZero
{G : Type u_6}
{H : Type u_7}
[Group G]
[PartialOrder G]
[Group H]
[PartialOrder H]
:
A version of Equiv.optionCongr for WithZero on OrderMonoidIso.
Equations
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
def
OrderMonoidIso.withZeroUnits
{α : Type u_6}
[LinearOrderedCommGroupWithZero α]
[DecidablePred fun (a : α) => a = 0]
:
Any linearly ordered group with zero is isomorphic to adjoining 0 to the units of itself.
Equations
Instances For
@[simp]
theorem
OrderMonoidIso.withZeroUnits_symm_apply
{α : Type u_6}
[LinearOrderedCommGroupWithZero α]
[DecidablePred fun (a : α) => a = 0]
(a : α)
:
@[simp]
theorem
OrderMonoidIso.withZeroUnits_apply
{α : Type u_6}
[LinearOrderedCommGroupWithZero α]
[DecidablePred fun (a : α) => a = 0]
(n : WithZero αˣ)
: