Monoid homomorphisms and units #
This file allows to lift monoid homomorphisms to group homomorphisms of their units subgroups. It
also contains unrelated results about Units
that depend on MonoidHom
.
Main declarations #
Units.map
: Turn an homomorphism fromα
toβ
monoids into an homomorphism fromαˣ
toβˣ
.MonoidHom.toHomUnits
: Turn an homomorphism from a groupα
toβ
into an homomorphism fromα
toβˣ
.
TODO #
The results that don't mention homomorphisms should be proved (earlier?) in a different file and be
used to golf the basic Group
lemmas.
If two homomorphisms from a subtraction monoid to an additive monoid are equal at an
additive unit x
, then they are equal at -x
.
If two homomorphisms from a division monoid to a monoid are equal at a unit x
, then they are
equal at x⁻¹⁻¹
.
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.
If a map g : M → AddUnits N→ AddUnits N
agrees with a homomorphism f : M →+ N→+ N
, then this map
is an AddMonoid homomorphism too.
Equations
- One or more equations did not get rendered due to their size.
If a map g : M → Nˣ→ Nˣ
agrees with a homomorphism f : M →* N→* N
, then
this map is a monoid homomorphism too.
Equations
- One or more equations did not get rendered due to their size.
If f
is a homomorphism from an additive group G
to an additive monoid M
,
then its image lies in the AddUnits
of M
,
and f.toHomUnits
is the corresponding homomorphism from G
to AddUnits M
.
Equations
- One or more equations did not get rendered due to their size.
If f
is a homomorphism from a group G
to a monoid M
,
then its image lies in the units of M
,
and f.toHomUnits
is the corresponding monoid homomorphism from G
to Mˣ
.
Equations
- One or more equations did not get rendered due to their size.
If a homomorphism f : M →+ N→+ N
sends each element to an IsAddUnit
, then it can be
lifted to f : M →+ AddUnits N→+ AddUnits N
. See also AddUnits.liftRight
for a computable version.
Equations
- IsAddUnit.liftRight f hf = AddUnits.liftRight f (fun x => IsAddUnit.addUnit (hf x)) (_ : ∀ (x : M), ↑(IsAddUnit.addUnit (hf x)) = ↑(IsAddUnit.addUnit (hf x)))
Equations
- (_ : ↑(IsAddUnit.addUnit (hf x)) = ↑(IsAddUnit.addUnit (hf x))) = (_ : ↑(IsAddUnit.addUnit (hf x)) = ↑(IsAddUnit.addUnit (hf x)))
If a homomorphism f : M →* N→* N
sends each element to an IsUnit
, then it can be lifted
to f : M →* Nˣ→* Nˣ
. See also Units.liftRight
for a computable version.
Equations
- IsUnit.liftRight f hf = Units.liftRight f (fun x => IsUnit.unit (hf x)) (_ : ∀ (x : M), ↑(IsUnit.unit (hf x)) = ↑(IsUnit.unit (hf x)))
The element of the additive group of additive units, corresponding to an element of
an additive monoid which is an additive unit. As opposed to IsAddUnit.addUnit
, the negation is
computable and comes from the negation on α
. This is useful to transfer properties of negation
in AddUnits α
to α
. See also toAddUnits
.
The element of the group of units, corresponding to an element of a monoid which is a unit. As
opposed to IsUnit.unit
, the inverse is computable and comes from the inversion on α
. This is
useful to transfer properties of inversion in Units α
to α
. See also toUnits
.