Ordered monoid and group homomorphisms #
This file defines morphisms between (additive) ordered monoids.
Types of morphisms #
OrderAddMonoidHom: Ordered additive monoid homomorphisms.OrderMonoidHom: Ordered monoid homomorphisms.OrderMonoidWithZeroHom: Ordered monoid with zero homomorphisms.OrderAddMonoidIso: Ordered additive monoid isomorphisms.OrderMonoidIso: Ordered monoid isomorphisms.
Notation #
→+o: Bundled ordered additive monoid homs. Also use for additive group homs.→*o: Bundled ordered monoid homs. Also use for group homs.→*₀o: Bundled ordered monoid with zero homs. Also use for group with zero homs.≃+o: Bundled ordered additive monoid isos. Also use for additive group isos.≃*o: Bundled ordered monoid isos. Also use for group isos.≃*₀o: Bundled ordered monoid with zero isos. Also use for group with zero isos.
Implementation notes #
There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.
There is no OrderGroupHom -- the idea is that OrderMonoidHom is used.
The constructor for OrderMonoidHom needs a proof of map_one as well as map_mul; a separate
constructor OrderMonoidHom.mk' will construct ordered group homs (i.e. ordered monoid homs
between ordered groups) given only a proof that multiplication is preserved,
Implicit {} brackets are often used instead of type class [] brackets. This is done when the
instances can be inferred because they are implicit arguments to the type OrderMonoidHom. When
they can be inferred from the type it is faster to use this method than to use type class inference.
Removed typeclasses #
This file used to define typeclasses for order-preserving (additive) monoid homomorphisms:
OrderAddMonoidHomClass, OrderMonoidHomClass, and OrderMonoidWithZeroHomClass.
In https://github.com/leanprover-community/mathlib4/pull/10544 we migrated from these typeclasses
to assumptions like [FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N],
making some definitions and lemmas irrelevant.
Tags #
ordered monoid, ordered group, monoid with zero
structure
OrderAddMonoidHom
(α : Type u_6)
(β : Type u_7)
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
extends α →+ β :
Type (max u_6 u_7)
α →+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).
- toFun : α → β
- map_add' (x y : α) : (↑self.toAddMonoidHom).toFun (x + y) = (↑self.toAddMonoidHom).toFun x + (↑self.toAddMonoidHom).toFun y
- monotone' : Monotone (↑self.toAddMonoidHom).toFun
An
OrderAddMonoidHomis a monotone function.
Infix notation for OrderAddMonoidHom.
Equations
- «term_→+o_» = Lean.ParserDescr.trailingNode `«term_→+o_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →+o ") (Lean.ParserDescr.cat `term 25))
structure
OrderAddMonoidIso
(α : Type u_6)
(β : Type u_7)
[Preorder α]
[Preorder β]
[Add α]
[Add β]
extends α ≃+ β :
Type (max u_6 u_7)
α ≃+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).
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
An
OrderAddMonoidIsorespects≤.
Infix notation for OrderAddMonoidIso.
Equations
- «term_≃+o_» = Lean.ParserDescr.trailingNode `«term_≃+o_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃+o ") (Lean.ParserDescr.cat `term 25))
structure
OrderMonoidHom
(α : Type u_6)
(β : Type u_7)
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
extends α →* β :
Type (max u_6 u_7)
α →*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).
- toFun : α → β
- map_mul' (x y : α) : (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
- monotone' : Monotone (↑self.toMonoidHom).toFun
An
OrderMonoidHomis a monotone function.
Infix notation for OrderMonoidHom.
Equations
- «term_→*o_» = Lean.ParserDescr.trailingNode `«term_→*o_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →*o ") (Lean.ParserDescr.cat `term 25))
def
OrderMonoidHomClass.toOrderMonoidHom
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
[FunLike F α β]
[OrderHomClass F α β]
[MonoidHomClass F α β]
(f : F)
:
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 β.
Equations
- ↑f = { toMonoidHom := ↑f, monotone' := ⋯ }
def
OrderMonoidHomClass.toOrderAddMonoidHom
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
[FunLike F α β]
[OrderHomClass F α β]
[AddMonoidHomClass F α β]
(f : F)
:
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 β.
Equations
- ↑f = { toAddMonoidHom := ↑f, monotone' := ⋯ }
instance
instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
[FunLike F α β]
[OrderHomClass F α β]
[MonoidHomClass F α β]
:
Any type satisfying OrderMonoidHomClass can be cast into OrderMonoidHom via
OrderMonoidHomClass.toOrderMonoidHom.
instance
instCoeTCOrderAddMonoidHomOfOrderHomClassOfAddMonoidHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
[FunLike F α β]
[OrderHomClass F α β]
[AddMonoidHomClass F α β]
:
Any type satisfying OrderAddMonoidHomClass can be cast into OrderAddMonoidHom via
OrderAddMonoidHomClass.toOrderAddMonoidHom
structure
OrderMonoidIso
(α : Type u_6)
(β : Type u_7)
[Preorder α]
[Preorder β]
[Mul α]
[Mul β]
extends α ≃* β :
Type (max u_6 u_7)
α ≃*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).
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
An
OrderMonoidIsorespects≤.
Infix notation for OrderMonoidIso.
Equations
- «term_≃*o_» = Lean.ParserDescr.trailingNode `«term_≃*o_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃*o ") (Lean.ParserDescr.cat `term 25))
def
OrderMonoidIsoClass.toOrderMonoidIso
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
[EquivLike F α β]
[OrderIsoClass F α β]
[MulEquivClass F α β]
(f : F)
:
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 β.
Equations
- ↑f = { toMulEquiv := ↑f, map_le_map_iff' := ⋯ }
def
OrderMonoidIsoClass.toOrderAddMonoidIso
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
[EquivLike F α β]
[OrderIsoClass F α β]
[AddEquivClass F α β]
(f : F)
:
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 β.
Equations
- ↑f = { toAddEquiv := ↑f, map_le_map_iff' := ⋯ }
instance
instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass_1
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
[FunLike F α β]
[OrderHomClass F α β]
[MonoidHomClass F α β]
:
Any type satisfying OrderMonoidHomClass can be cast into OrderMonoidHom via
OrderMonoidHomClass.toOrderMonoidHom.
instance
instCoeTCOrderAddMonoidHomOfOrderHomClassOfAddMonoidHomClass_1
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
[FunLike F α β]
[OrderHomClass F α β]
[AddMonoidHomClass F α β]
:
Any type satisfying OrderAddMonoidHomClass can be cast into OrderAddMonoidHom via
OrderAddMonoidHomClass.toOrderAddMonoidHom
instance
instCoeTCOrderMonoidIsoOfOrderIsoClassOfMulEquivClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
[EquivLike F α β]
[OrderIsoClass F α β]
[MulEquivClass F α β]
:
Any type satisfying OrderMonoidIsoClass can be cast into OrderMonoidIso via
OrderMonoidIsoClass.toOrderMonoidIso.
instance
instCoeTCOrderAddMonoidIsoOfOrderIsoClassOfAddEquivClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
[EquivLike F α β]
[OrderIsoClass F α β]
[AddEquivClass F α β]
:
Any type satisfying OrderAddMonoidIsoClass can be cast into OrderAddMonoidIso via
OrderAddMonoidIsoClass.toOrderAddMonoidIso
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.
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)
:
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 α β]
:
theorem
map_nonneg
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[Preorder α]
[Zero α]
[Preorder β]
[Zero β]
[OrderHomClass F α β]
[ZeroHomClass F α β]
(f : F)
{a : α}
(ha : 0 ≤ a)
:
See also NonnegHomClass.apply_nonneg.
theorem
map_nonpos
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[FunLike F α β]
[Preorder α]
[Zero α]
[Preorder β]
[Zero β]
[OrderHomClass F α β]
[ZeroHomClass F α β]
(f : F)
{a : α}
(ha : a ≤ 0)
:
theorem
monotone_iff_map_nonneg
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[i : FunLike F α β]
(f : F)
[iamhc : AddMonoidHomClass F α β]
:
theorem
antitone_iff_map_nonpos
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[i : FunLike F α β]
(f : F)
[iamhc : AddMonoidHomClass F α β]
:
theorem
monotone_iff_map_nonpos
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[i : FunLike F α β]
(f : F)
[iamhc : AddMonoidHomClass F α β]
:
theorem
antitone_iff_map_nonneg
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[i : FunLike F α β]
(f : F)
[iamhc : AddMonoidHomClass F α β]
:
theorem
strictMono_iff_map_pos
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[i : FunLike F α β]
(f : F)
[iamhc : AddMonoidHomClass F α β]
:
theorem
strictAnti_iff_map_neg
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[i : FunLike F α β]
(f : F)
[iamhc : AddMonoidHomClass F α β]
:
theorem
strictMono_iff_map_neg
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[i : FunLike F α β]
(f : F)
[iamhc : AddMonoidHomClass F α β]
:
theorem
strictAnti_iff_map_pos
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[i : FunLike F α β]
(f : F)
[iamhc : AddMonoidHomClass F α β]
:
instance
OrderMonoidHom.instFunLike
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
:
Equations
- OrderMonoidHom.instFunLike = { coe := fun (f : α →*o β) => (↑f.toMonoidHom).toFun, coe_injective' := ⋯ }
instance
OrderAddMonoidHom.instFunLike
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
:
Equations
- OrderAddMonoidHom.instFunLike = { coe := fun (f : α →+o β) => (↑f.toAddMonoidHom).toFun, coe_injective' := ⋯ }
instance
OrderMonoidHom.instOrderHomClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
:
OrderHomClass (α →*o β) α β
instance
OrderAddMonoidHom.instOrderHomClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
:
OrderHomClass (α →+o β) α β
instance
OrderMonoidHom.instMonoidHomClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
:
MonoidHomClass (α →*o β) α β
instance
OrderAddMonoidHom.instAddMonoidHomClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
:
AddMonoidHomClass (α →+o β) α β
theorem
OrderMonoidHom.ext
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
{f g : α →*o β}
(h : ∀ (a : α), f a = g a)
:
theorem
OrderAddMonoidHom.ext
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
{f g : α →+o β}
(h : ∀ (a : α), f a = g a)
:
theorem
OrderMonoidHom.ext_iff
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
{f g : α →*o β}
:
theorem
OrderAddMonoidHom.ext_iff
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
{f g : α →+o β}
:
theorem
OrderMonoidHom.toFun_eq_coe
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(f : α →*o β)
:
theorem
OrderAddMonoidHom.toFun_eq_coe
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(f : α →+o β)
:
@[simp]
theorem
OrderMonoidHom.coe_mk
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(f : α →* β)
(h : Monotone (↑f).toFun)
:
@[simp]
theorem
OrderAddMonoidHom.coe_mk
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(f : α →+ β)
(h : Monotone (↑f).toFun)
:
@[simp]
theorem
OrderMonoidHom.mk_coe
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(f : α →*o β)
(h : Monotone (↑↑f).toFun)
:
@[simp]
theorem
OrderAddMonoidHom.mk_coe
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(f : α →+o β)
(h : Monotone (↑↑f).toFun)
:
def
OrderMonoidHom.toOrderHom
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(f : α →*o β)
:
Reinterpret an ordered monoid homomorphism as an order homomorphism.
Equations
- f.toOrderHom = { toFun := (↑f.toMonoidHom).toFun, monotone' := ⋯ }
def
OrderAddMonoidHom.toOrderHom
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(f : α →+o β)
:
Reinterpret an ordered additive monoid homomorphism as an order homomorphism.
Equations
- f.toOrderHom = { toFun := (↑f.toAddMonoidHom).toFun, monotone' := ⋯ }
@[simp]
theorem
OrderMonoidHom.coe_monoidHom
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(f : α →*o β)
:
@[simp]
theorem
OrderAddMonoidHom.coe_addMonoidHom
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(f : α →+o β)
:
@[simp]
theorem
OrderMonoidHom.coe_orderHom
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(f : α →*o β)
:
@[simp]
theorem
OrderAddMonoidHom.coe_orderHom
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(f : α →+o β)
:
theorem
OrderMonoidHom.toMonoidHom_injective
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
:
theorem
OrderAddMonoidHom.toAddMonoidHom_injective
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
:
theorem
OrderMonoidHom.toOrderHom_injective
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
:
theorem
OrderAddMonoidHom.toOrderHom_injective
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
:
def
OrderMonoidHom.copy
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(f : α →*o β)
(f' : α → β)
(h : f' = ⇑f)
:
Copy of an OrderMonoidHom with a new toFun equal to the old one. Useful to fix
definitional equalities.
def
OrderAddMonoidHom.copy
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(f : α →+o β)
(f' : α → β)
(h : f' = ⇑f)
:
Copy of an OrderAddMonoidHom with a new toFun equal to the old one. Useful to fix
definitional equalities.
@[simp]
theorem
OrderMonoidHom.coe_copy
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(f : α →*o β)
(f' : α → β)
(h : f' = ⇑f)
:
@[simp]
theorem
OrderAddMonoidHom.coe_copy
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(f : α →+o β)
(f' : α → β)
(h : f' = ⇑f)
:
theorem
OrderMonoidHom.copy_eq
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(f : α →*o β)
(f' : α → β)
(h : f' = ⇑f)
:
theorem
OrderAddMonoidHom.copy_eq
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(f : α →+o β)
(f' : α → β)
(h : f' = ⇑f)
:
The identity map as an ordered monoid homomorphism.
Equations
- OrderMonoidHom.id α = { toMonoidHom := MonoidHom.id α, monotone' := ⋯ }
The identity map as an ordered additive monoid homomorphism.
Equations
- OrderAddMonoidHom.id α = { toAddMonoidHom := AddMonoidHom.id α, monotone' := ⋯ }
@[simp]
@[simp]
Equations
- OrderMonoidHom.instInhabited α = { default := OrderMonoidHom.id α }
Equations
- OrderAddMonoidHom.instInhabited α = { default := OrderAddMonoidHom.id α }
def
OrderMonoidHom.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulOneClass α]
[MulOneClass β]
[MulOneClass γ]
(f : β →*o γ)
(g : α →*o β)
:
Composition of OrderMonoidHoms as an OrderMonoidHom.
def
OrderAddMonoidHom.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[AddZeroClass α]
[AddZeroClass β]
[AddZeroClass γ]
(f : β →+o γ)
(g : α →+o β)
:
Composition of OrderAddMonoidHoms as an OrderAddMonoidHom
@[simp]
theorem
OrderMonoidHom.coe_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulOneClass α]
[MulOneClass β]
[MulOneClass γ]
(f : β →*o γ)
(g : α →*o β)
:
@[simp]
theorem
OrderAddMonoidHom.coe_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[AddZeroClass α]
[AddZeroClass β]
[AddZeroClass γ]
(f : β →+o γ)
(g : α →+o β)
:
@[simp]
theorem
OrderMonoidHom.comp_apply
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulOneClass α]
[MulOneClass β]
[MulOneClass γ]
(f : β →*o γ)
(g : α →*o β)
(a : α)
:
@[simp]
theorem
OrderAddMonoidHom.comp_apply
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[AddZeroClass α]
[AddZeroClass β]
[AddZeroClass γ]
(f : β →+o γ)
(g : α →+o β)
(a : α)
:
theorem
OrderMonoidHom.coe_comp_monoidHom
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulOneClass α]
[MulOneClass β]
[MulOneClass γ]
(f : β →*o γ)
(g : α →*o β)
:
theorem
OrderAddMonoidHom.coe_comp_addMonoidHom
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[AddZeroClass α]
[AddZeroClass β]
[AddZeroClass γ]
(f : β →+o γ)
(g : α →+o β)
:
theorem
OrderMonoidHom.coe_comp_orderHom
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulOneClass α]
[MulOneClass β]
[MulOneClass γ]
(f : β →*o γ)
(g : α →*o β)
:
theorem
OrderAddMonoidHom.coe_comp_orderHom
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[AddZeroClass α]
[AddZeroClass β]
[AddZeroClass γ]
(f : β →+o γ)
(g : α →+o β)
:
@[simp]
theorem
OrderMonoidHom.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[Preorder α]
[Preorder β]
[Preorder γ]
[Preorder δ]
[MulOneClass α]
[MulOneClass β]
[MulOneClass γ]
[MulOneClass δ]
(f : γ →*o δ)
(g : β →*o γ)
(h : α →*o β)
:
@[simp]
theorem
OrderAddMonoidHom.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[Preorder α]
[Preorder β]
[Preorder γ]
[Preorder δ]
[AddZeroClass α]
[AddZeroClass β]
[AddZeroClass γ]
[AddZeroClass δ]
(f : γ →+o δ)
(g : β →+o γ)
(h : α →+o β)
:
@[simp]
theorem
OrderMonoidHom.comp_id
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(f : α →*o β)
:
@[simp]
theorem
OrderAddMonoidHom.comp_id
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(f : α →+o β)
:
@[simp]
theorem
OrderMonoidHom.id_comp
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(f : α →*o β)
:
@[simp]
theorem
OrderAddMonoidHom.id_comp
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(f : α →+o β)
:
@[simp]
theorem
OrderMonoidHom.cancel_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulOneClass α]
[MulOneClass β]
[MulOneClass γ]
{g₁ g₂ : β →*o γ}
{f : α →*o β}
(hf : Function.Surjective ⇑f)
:
@[simp]
theorem
OrderAddMonoidHom.cancel_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[AddZeroClass α]
[AddZeroClass β]
[AddZeroClass γ]
{g₁ g₂ : β →+o γ}
{f : α →+o β}
(hf : Function.Surjective ⇑f)
:
@[simp]
theorem
OrderMonoidHom.cancel_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulOneClass α]
[MulOneClass β]
[MulOneClass γ]
{g : β →*o γ}
{f₁ f₂ : α →*o β}
(hg : Function.Injective ⇑g)
:
@[simp]
theorem
OrderAddMonoidHom.cancel_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[AddZeroClass α]
[AddZeroClass β]
[AddZeroClass γ]
{g : β →+o γ}
{f₁ f₂ : α →+o β}
(hg : Function.Injective ⇑g)
:
instance
OrderMonoidHom.instOne
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
:
1 is the homomorphism sending all elements to 1.
Equations
- OrderMonoidHom.instOne = { one := let __src := 1; { toMonoidHom := __src, monotone' := ⋯ } }
instance
OrderAddMonoidHom.instZero
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
:
0 is the homomorphism sending all elements to 0.
Equations
- OrderAddMonoidHom.instZero = { zero := let __src := 0; { toAddMonoidHom := __src, monotone' := ⋯ } }
@[simp]
theorem
OrderMonoidHom.coe_one
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
:
@[simp]
theorem
OrderAddMonoidHom.coe_zero
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
:
@[simp]
theorem
OrderMonoidHom.one_apply
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulOneClass α]
[MulOneClass β]
(a : α)
:
@[simp]
theorem
OrderAddMonoidHom.zero_apply
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[AddZeroClass α]
[AddZeroClass β]
(a : α)
:
@[simp]
theorem
OrderMonoidHom.one_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulOneClass α]
[MulOneClass β]
[MulOneClass γ]
(f : α →*o β)
:
@[simp]
theorem
OrderAddMonoidHom.zero_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[AddZeroClass α]
[AddZeroClass β]
[AddZeroClass γ]
(f : α →+o β)
:
@[simp]
theorem
OrderMonoidHom.comp_one
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[MulOneClass α]
[MulOneClass β]
[MulOneClass γ]
(f : β →*o γ)
:
@[simp]
theorem
OrderAddMonoidHom.comp_zero
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Preorder α]
[Preorder β]
[Preorder γ]
[AddZeroClass α]
[AddZeroClass β]
[AddZeroClass γ]
(f : β →+o γ)
:
instance
OrderMonoidHom.instMulOfIsOrderedMonoid
{α : Type u_2}
{β : Type u_3}
[CommMonoid α]
[PartialOrder α]
[CommMonoid β]
[PartialOrder β]
[IsOrderedMonoid β]
:
For two ordered monoid morphisms f and g, their product is the ordered monoid morphism
sending a to f a * g a.
Equations
- OrderMonoidHom.instMulOfIsOrderedMonoid = { mul := fun (f g : α →*o β) => let __src := ↑f * ↑g; { toMonoidHom := __src, monotone' := ⋯ } }
instance
OrderAddMonoidHom.instAddOfIsOrderedAddMonoid
{α : Type u_2}
{β : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[AddCommMonoid β]
[PartialOrder β]
[IsOrderedAddMonoid β]
:
For two ordered additive monoid morphisms f and g, their product is the ordered
additive monoid morphism sending a to f a + g a.
Equations
- OrderAddMonoidHom.instAddOfIsOrderedAddMonoid = { add := fun (f g : α →+o β) => let __src := ↑f + ↑g; { toAddMonoidHom := __src, monotone' := ⋯ } }
@[simp]
theorem
OrderMonoidHom.coe_mul
{α : Type u_2}
{β : Type u_3}
[CommMonoid α]
[PartialOrder α]
[CommMonoid β]
[PartialOrder β]
[IsOrderedMonoid β]
(f g : α →*o β)
:
@[simp]
theorem
OrderAddMonoidHom.coe_add
{α : Type u_2}
{β : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[AddCommMonoid β]
[PartialOrder β]
[IsOrderedAddMonoid β]
(f g : α →+o β)
:
@[simp]
theorem
OrderMonoidHom.mul_apply
{α : Type u_2}
{β : Type u_3}
[CommMonoid α]
[PartialOrder α]
[CommMonoid β]
[PartialOrder β]
[IsOrderedMonoid β]
(f g : α →*o β)
(a : α)
:
@[simp]
theorem
OrderAddMonoidHom.add_apply
{α : Type u_2}
{β : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[AddCommMonoid β]
[PartialOrder β]
[IsOrderedAddMonoid β]
(f g : α →+o β)
(a : α)
:
theorem
OrderMonoidHom.mul_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CommMonoid α]
[PartialOrder α]
[CommMonoid β]
[PartialOrder β]
[CommMonoid γ]
[PartialOrder γ]
[IsOrderedMonoid γ]
(g₁ g₂ : β →*o γ)
(f : α →*o β)
:
theorem
OrderAddMonoidHom.add_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[AddCommMonoid α]
[PartialOrder α]
[AddCommMonoid β]
[PartialOrder β]
[AddCommMonoid γ]
[PartialOrder γ]
[IsOrderedAddMonoid γ]
(g₁ g₂ : β →+o γ)
(f : α →+o β)
:
theorem
OrderMonoidHom.comp_mul
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CommMonoid α]
[PartialOrder α]
[CommMonoid β]
[PartialOrder β]
[CommMonoid γ]
[PartialOrder γ]
[IsOrderedMonoid β]
[IsOrderedMonoid γ]
(g : β →*o γ)
(f₁ f₂ : α →*o β)
:
theorem
OrderAddMonoidHom.comp_add
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[AddCommMonoid α]
[PartialOrder α]
[AddCommMonoid β]
[PartialOrder β]
[AddCommMonoid γ]
[PartialOrder γ]
[IsOrderedAddMonoid β]
[IsOrderedAddMonoid γ]
(g : β →+o γ)
(f₁ f₂ : α →+o β)
:
@[simp]
theorem
OrderMonoidHom.toMonoidHom_eq_coe
{α : Type u_2}
{β : Type u_3}
{x✝ : Preorder α}
{x✝¹ : Preorder β}
{x✝² : MulOneClass α}
{x✝³ : MulOneClass β}
(f : α →*o β)
:
@[simp]
theorem
OrderAddMonoidHom.toAddMonoidHom_eq_coe
{α : Type u_2}
{β : Type u_3}
{x✝ : Preorder α}
{x✝¹ : Preorder β}
{x✝² : AddZeroClass α}
{x✝³ : AddZeroClass β}
(f : α →+o β)
:
@[simp]
theorem
OrderMonoidHom.toOrderHom_eq_coe
{α : Type u_2}
{β : Type u_3}
{x✝ : Preorder α}
{x✝¹ : Preorder β}
{x✝² : MulOneClass α}
{x✝³ : MulOneClass β}
(f : α →*o β)
:
@[simp]
theorem
OrderAddMonoidHom.toOrderHom_eq_coe
{α : Type u_2}
{β : Type u_3}
{x✝ : Preorder α}
{x✝¹ : Preorder β}
{x✝² : AddZeroClass α}
{x✝³ : AddZeroClass β}
(f : α →+o β)
:
def
OrderMonoidHom.mk'
{α : Type u_2}
{β : Type u_3}
{x✝ : CommGroup α}
{x✝¹ : PartialOrder α}
{x✝² : CommGroup β}
{x✝³ : PartialOrder β}
(f : α → β)
(hf : Monotone f)
(map_mul : ∀ (a b : α), f (a * b) = f a * f b)
:
Makes an ordered group homomorphism from a proof that the map preserves multiplication.
Equations
- OrderMonoidHom.mk' f hf map_mul = { toMonoidHom := MonoidHom.mk' f map_mul, monotone' := hf }
def
OrderAddMonoidHom.mk'
{α : Type u_2}
{β : Type u_3}
{x✝ : AddCommGroup α}
{x✝¹ : PartialOrder α}
{x✝² : AddCommGroup β}
{x✝³ : PartialOrder β}
(f : α → β)
(hf : Monotone f)
(map_mul : ∀ (a b : α), f (a + b) = f a + f b)
:
Makes an ordered additive group homomorphism from a proof that the map preserves addition.
Equations
- OrderAddMonoidHom.mk' f hf map_mul = { toAddMonoidHom := AddMonoidHom.mk' f map_mul, monotone' := hf }
instance
OrderMonoidIso.instOrderIsoClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[Mul α]
[Mul β]
:
OrderIsoClass (α ≃*o β) α β
instance
OrderAddMonoidIso.instOrderIsoClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[Add α]
[Add β]
:
OrderIsoClass (α ≃+o β) α β
instance
OrderMonoidIso.instMulEquivClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[Mul α]
[Mul β]
:
MulEquivClass (α ≃*o β) α β
instance
OrderAddMonoidIso.instAddEquivClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[Add α]
[Add β]
:
AddEquivClass (α ≃+o β) α β
The identity map as an ordered monoid isomorphism.
Equations
- OrderMonoidIso.refl α = { toMulEquiv := MulEquiv.refl α, map_le_map_iff' := ⋯ }
The identity map as an ordered additive monoid isomorphism.
Equations
- OrderAddMonoidIso.refl α = { toAddEquiv := AddEquiv.refl α, map_le_map_iff' := ⋯ }
@[simp]
@[simp]
Equations
- OrderMonoidIso.instInhabited α = { default := OrderMonoidIso.refl α }
Equations
- OrderAddMonoidIso.instInhabited α = { default := OrderAddMonoidIso.refl α }
@[simp]
@[simp]
theorem
OrderMonoidIso.strictMono
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[Mul α]
[Mul β]
(f : α ≃*o β)
:
StrictMono ⇑f
theorem
OrderAddMonoidIso.strictMono
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[Add α]
[Add β]
(f : α ≃+o β)
:
StrictMono ⇑f
def
OrderMonoidIso.mk'
{α : Type u_2}
{β : Type u_3}
{x✝ : CommGroup α}
{x✝¹ : PartialOrder α}
{x✝² : CommGroup β}
{x✝³ : PartialOrder β}
(f : α ≃ β)
(hf : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b)
(map_mul : ∀ (a b : α), f (a * b) = f a * f b)
:
Makes an ordered group isomorphism from a proof that the map preserves multiplication.
Equations
- OrderMonoidIso.mk' f hf map_mul = { toMulEquiv := MulEquiv.mk' f map_mul, map_le_map_iff' := ⋯ }
def
OrderAddMonoidIso.mk'
{α : Type u_2}
{β : Type u_3}
{x✝ : AddCommGroup α}
{x✝¹ : PartialOrder α}
{x✝² : AddCommGroup β}
{x✝³ : PartialOrder β}
(f : α ≃ β)
(hf : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b)
(map_mul : ∀ (a b : α), f (a + b) = f a + f b)
:
Makes an ordered additive group isomorphism from a proof that the map preserves addition.
Equations
- OrderAddMonoidIso.mk' f hf map_mul = { toAddEquiv := AddEquiv.mk' f map_mul, map_le_map_iff' := ⋯ }
instance
OrderMonoidWithZeroHom.instFunLike
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[MulZeroOneClass α]
[MulZeroOneClass β]
:
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)
:
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
- 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 β)
:
@[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.
@[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
- OrderMonoidWithZeroHom.id α = { toMonoidWithZeroHom := MonoidWithZeroHom.id α, monotone' := ⋯ }
@[simp]
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 β)
:
Composition of OrderMonoidWithZeroHoms as an OrderMonoidWithZeroHom.
@[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
- 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 β)
:
@[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.toOrderMonoidHom_eq_coe
{α : Type u_2}
{β : Type u_3}
{hα : Preorder α}
{hα' : MulZeroOneClass α}
{hβ : Preorder β}
{hβ' : MulZeroOneClass β}
(f : α →*₀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]
@[simp]
theorem
OrderMonoidIso.val_inv_unitsWithZero_symm_apply
{α : Type u_6}
[Group α]
[Preorder α]
(a : α)
: