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.
Typeclasses #
Notation #
→+o→+o
: Bundled ordered additive monoid homs. Also use for additive groups homs.→*o→*o
: Bundled ordered monoid homs. Also use for groups homs.→*₀o→*₀o
: Bundled ordered monoid with zero homs. Also use for groups with zero homs.
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.
Tags #
ordered monoid, ordered group, monoid with zero
An
OrderAddMonoidHom
is a monotone function.monotone' : Monotone (↑toAddMonoidHom).toFun
α →+o β→+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 β)→+o β)
,
you should parametrize over (F : Type _) [OrderAddMonoidHomClass F α β] (f : F)
.
When you extend this structure, make sure to extend OrderAddMonoidHomClass
.
Instances For
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))
An
OrderAddMonoidHom
is a monotone function.monotone : ∀ (f : F), Monotone ↑f
OrderAddMonoidHomClass F α β
states that F
is a type of ordered monoid homomorphisms.
You should also extend this typeclass when you extend OrderAddMonoidHom
.
Instances
An
OrderMonoidHom
is a monotone function.monotone' : Monotone (↑toMonoidHom).toFun
α →*o β→*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 β)→*o β)
,
you should parametrize over (F : Type _) [OrderMonoidHomClass F α β] (f : F)
.
When you extend this structure, make sure to extend OrderMonoidHomClass
.
Instances For
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))
An
OrderMonoidHom
is a monotone function.monotone : ∀ (f : F), Monotone ↑f
OrderMonoidHomClass F α β
states that F
is a type of ordered monoid homomorphisms.
You should also extend this typeclass when you extend OrderMonoidHom
.
Instances
Turn an element of a type F
satisfying OrderAddMonoidHomClass F α β
into an actual
OrderAddMonoidHom
. This is declared as the default coercion from F
to α →+o β→+o β
.
Equations
- One or more equations did not get rendered due to their size.
Turn an element of a type F
satisfying OrderMonoidHomClass F α β
into an actual
OrderMonoidHom
. This is declared as the default coercion from F
to α →*o β→*o β
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- OrderAddMonoidHomClass.toOrderHomClass = let src := inst; RelHomClass.mk (_ : ∀ (f : F), Monotone ↑f)
Equations
- OrderMonoidHomClass.toOrderHomClass = let src := inst; RelHomClass.mk (_ : ∀ (f : F), Monotone ↑f)
Any type satisfying OrderAddMonoidHomClass
can be cast into OrderAddMonoidHom
via
OrderAddMonoidHomClass.toOrderAddMonoidHom
Equations
- instCoeTCOrderAddMonoidHom = { coe := OrderAddMonoidHomClass.toOrderAddMonoidHom }
Any type satisfying OrderMonoidHomClass
can be cast into OrderMonoidHom
via
OrderMonoidHomClass.toOrderMonoidHom
.
Equations
- instCoeTCOrderMonoidHom = { coe := OrderMonoidHomClass.toOrderMonoidHom }
An
OrderMonoidWithZeroHom
is a monotone function.monotone' : Monotone (↑toMonoidWithZeroHom).toFun
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 parametrize over (F : Type _) [OrderMonoidWithZeroHomClass F α β] (f : F)
.
When you extend this structure, make sure to extend OrderMonoidWithZeroHomClass
.
Instances For
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))
An
OrderMonoidWithZeroHom
is a monotone function.monotone : ∀ (f : F), Monotone ↑f
OrderMonoidWithZeroHomClass F α β
states that F
is a type of
ordered monoid with zero homomorphisms.
You should also extend this typeclass when you extend OrderMonoidWithZeroHom
.
Instances
Turn an element of a type F
satisfying OrderMonoidWithZeroHomClass F α β
into an actual
OrderMonoidWithZeroHom
. This is declared as the default coercion from F
to α →+*₀o β→+*₀o β
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- OrderMonoidWithZeroHomClass.toOrderMonoidHomClass = let src := inst; OrderMonoidHomClass.mk (_ : ∀ (f : F), Monotone ↑f)
Equations
- instCoeTCOrderMonoidWithZeroHom = { coe := OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom }
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ZeroHom.toFun (↑f.toAddMonoidHom) 0 = 0) = (_ : ZeroHom.toFun (↑f.toAddMonoidHom) 0 = 0)
Equations
- OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom = OrderAddMonoidHomClass.mk (_ : ∀ (f : α →+o β), Monotone (↑f.toAddMonoidHom).toFun)
Equations
- OrderMonoidHom.instOrderMonoidHomClassOrderMonoidHom = OrderMonoidHomClass.mk (_ : ∀ (f : α →*o β), Monotone (↑f.toMonoidHom).toFun)
Reinterpret an ordered additive monoid homomorphism as an order homomorphism.
Equations
- OrderAddMonoidHom.toOrderHom f = { toFun := (↑f.toAddMonoidHom).toFun, monotone' := (_ : Monotone (↑f.toAddMonoidHom).toFun) }
Reinterpret an ordered monoid homomorphism as an order homomorphism.
Equations
- OrderMonoidHom.toOrderHom f = { toFun := (↑f.toMonoidHom).toFun, monotone' := (_ : Monotone (↑f.toMonoidHom).toFun) }
Equations
- (_ : ZeroHom.toFun (↑(AddMonoidHom.copy f.toAddMonoidHom f' h)) 0 = 0) = (_ : ZeroHom.toFun (↑(AddMonoidHom.copy f.toAddMonoidHom f' h)) 0 = 0)
Copy of an OrderAddMonoidHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Equations
- One or more equations did not get rendered due to their size.
Copy of an OrderMonoidHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Equations
- One or more equations did not get rendered due to their size.
The identity map as an ordered additive monoid homomorphism.
Equations
- One or more equations did not get rendered due to their size.
The identity map as an ordered monoid homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Equations
- OrderAddMonoidHom.instInhabitedOrderAddMonoidHom α = { default := OrderAddMonoidHom.id α }
Equations
- OrderMonoidHom.instInhabitedOrderMonoidHom α = { default := OrderMonoidHom.id α }
Composition of OrderAddMonoidHom
s as an OrderAddMonoidHom
Equations
- One or more equations did not get rendered due to their size.
Composition of OrderMonoidHom
s as an OrderMonoidHom
.
Equations
- One or more equations did not get rendered due to their size.
0
is the homomorphism sending all elements to 0
.
Equations
- One or more equations did not get rendered due to their size.
1
is the homomorphism sending all elements to 1
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Equations
- (_ : Monotone fun x => ZeroHom.toFun (↑f.toAddMonoidHom) x + ↑↑g x) = (_ : Monotone fun x => ZeroHom.toFun (↑f.toAddMonoidHom) x + ↑↑g x)
For two ordered monoid morphisms f
and g
, their product is the ordered monoid morphism
sending a
to f a * g a
.
Equations
- One or more equations did not get rendered due to their size.
Makes an ordered additive group homomorphism from a proof that the map preserves addition.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Makes an ordered group homomorphism from a proof that the map preserves multiplication.
Equations
- One or more equations did not get rendered due to their size.
Equations
- OrderMonoidWithZeroHom.instOrderMonoidWithZeroHomClassOrderMonoidWithZeroHom = OrderMonoidWithZeroHomClass.mk (_ : ∀ (f : α →*₀o β), Monotone (↑f.toMonoidWithZeroHom).toFun)
Reinterpret an ordered monoid with zero homomorphism as an order monoid homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Copy of an OrderMonoidWithZeroHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Equations
- One or more equations did not get rendered due to their size.
The identity map as an ordered monoid with zero homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Equations
- OrderMonoidWithZeroHom.instInhabitedOrderMonoidWithZeroHom α = { default := OrderMonoidWithZeroHom.id α }
Composition of OrderMonoidWithZeroHom
s as an OrderMonoidWithZeroHom
.
Equations
- One or more equations did not get rendered due to their size.
For two ordered monoid morphisms f
and g
, their product is the ordered monoid morphism
sending a
to f a * g a
.
Equations
- One or more equations did not get rendered due to their size.