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
: Bundled ordered additive monoid homs. Also use for additive groups homs.→*o
: Bundled ordered monoid homs. Also use for groups homs.→*₀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
- toFun : α → β
- map_zero' : ZeroHom.toFun (↑s.toAddMonoidHom) 0 = 0
- map_add' : ∀ (x y : α), ZeroHom.toFun (↑s.toAddMonoidHom) (x + y) = ZeroHom.toFun (↑s.toAddMonoidHom) x + ZeroHom.toFun (↑s.toAddMonoidHom) y
- monotone' : Monotone s.toFun
An
OrderAddMonoidHom
is a monotone function.
α →+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*) [OrderAddMonoidHomClass F α β] (f : F)
.
When you extend this structure, make sure to extend OrderAddMonoidHomClass
.
Instances For
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
- map_zero : ∀ (f : F), ↑f 0 = 0
- monotone : ∀ (f : F), Monotone ↑f
An
OrderAddMonoidHom
is a monotone function.
OrderAddMonoidHomClass F α β
states that F
is a type of ordered monoid homomorphisms.
You should also extend this typeclass when you extend OrderAddMonoidHom
.
Instances
- toFun : α → β
- map_one' : OneHom.toFun (↑s.toMonoidHom) 1 = 1
- map_mul' : ∀ (x y : α), OneHom.toFun (↑s.toMonoidHom) (x * y) = OneHom.toFun (↑s.toMonoidHom) x * OneHom.toFun (↑s.toMonoidHom) y
- monotone' : Monotone s.toFun
An
OrderMonoidHom
is a monotone function.
α →*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*) [OrderMonoidHomClass F α β] (f : F)
.
When you extend this structure, make sure to extend OrderMonoidHomClass
.
Instances For
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
- map_one : ∀ (f : F), ↑f 1 = 1
- monotone : ∀ (f : F), Monotone ↑f
An
OrderMonoidHom
is a monotone function.
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 β
.
Instances For
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 β
.
Instances For
Any type satisfying OrderAddMonoidHomClass
can be cast into OrderAddMonoidHom
via
OrderAddMonoidHomClass.toOrderAddMonoidHom
Any type satisfying OrderMonoidHomClass
can be cast into OrderMonoidHom
via
OrderMonoidHomClass.toOrderMonoidHom
.
- toFun : α → β
- map_zero' : ZeroHom.toFun (↑s.toMonoidWithZeroHom) 0 = 0
- map_one' : ZeroHom.toFun (↑s.toMonoidWithZeroHom) 1 = 1
- map_mul' : ∀ (x y : α), ZeroHom.toFun (↑s.toMonoidWithZeroHom) (x * y) = ZeroHom.toFun (↑s.toMonoidWithZeroHom) x * ZeroHom.toFun (↑s.toMonoidWithZeroHom) y
- monotone' : Monotone s.toFun
An
OrderMonoidWithZeroHom
is a monotone function.
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
.
Instances For
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
- map_one : ∀ (f : F), ↑f 1 = 1
- map_zero : ∀ (f : F), ↑f 0 = 0
- monotone : ∀ (f : F), Monotone ↑f
An
OrderMonoidWithZeroHom
is a monotone function.
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 β
.
Instances For
Reinterpret an ordered additive monoid homomorphism as an order homomorphism.
Instances For
Reinterpret an ordered monoid homomorphism as an order homomorphism.
Instances For
Copy of an OrderAddMonoidHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Instances For
Copy of an OrderMonoidHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Instances For
The identity map as an ordered additive monoid homomorphism.
Instances For
The identity map as an ordered monoid homomorphism.
Instances For
Composition of OrderAddMonoidHom
s as an OrderAddMonoidHom
Instances For
Composition of OrderMonoidHom
s as an OrderMonoidHom
.
Instances For
0
is the homomorphism sending all elements to 0
.
1
is the homomorphism sending all elements to 1
.
For two ordered additive monoid morphisms f
and g
, their product is the ordered
additive monoid morphism sending a
to f a + g a
.
For two ordered monoid morphisms f
and g
, their product is the ordered monoid morphism
sending a
to f a * g a
.
Makes an ordered additive group homomorphism from a proof that the map preserves addition.
Instances For
Makes an ordered group homomorphism from a proof that the map preserves multiplication.
Instances For
Reinterpret an ordered monoid with zero homomorphism as an order monoid homomorphism.
Instances For
Copy of an OrderMonoidWithZeroHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Instances For
The identity map as an ordered monoid with zero homomorphism.
Instances For
Composition of OrderMonoidWithZeroHom
s as an OrderMonoidWithZeroHom
.
Instances For
For two ordered monoid morphisms f
and g
, their product is the ordered monoid morphism
sending a
to f a * g a
.