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 a homomorphism fromα
toβ
monoids into a homomorphism fromαˣ
toβˣ
.MonoidHom.toHomUnits
: Turn a homomorphism from a groupα
toβ
into a 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⁻¹
.
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
.
Instances For
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ˣ
.
Instances For
If a homomorphism f : M →+ N
sends each element to an IsAddUnit
, then it can be
lifted to f : M →+ AddUnits N
. See also AddUnits.liftRight
for a computable version.
Instances For
If a homomorphism f : M →* N
sends each element to an IsUnit
, then it can be lifted
to f : M →* Nˣ
. See also Units.liftRight
for a computable version.
Instances For
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
.
Instances For
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
.
Instances For
The AddGroup
version of this lemma is sub_add_cancel''
The Group
version of this lemma is div_mul_cancel'''