Lift monoid homomorphisms to group homomorphisms of their units subgroups. #
The add_group
homomorphism on add_unit
s induced by an add_monoid_hom
.
Coercion units M → M
as a monoid homomorphism.
Equations
- units.coe_hom M = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _}
Coercion add_units M → M
as an add_monoid homomorphism.
If a map g : M → add_units N
agrees with a homomorphism f : M →+ N
, then this map
is an add_monoid homomorphism too.
If f
is a homomorphism from an additive group G
to an additive monoid M
,
then its image lies in the add_units
of M
,
and f.to_hom_units
is the corresponding homomorphism from G
to add_units M
.
If f
is a homomorphism from a group G
to a monoid M
,
then its image lies in the units of M
,
and f.to_hom_units
is the corresponding monoid homomorphism from G
to units M
.
If a homomorphism f : M →* N
sends each element to an is_unit
, then it can be lifted
to f : M →* units N
. See also units.lift_right
for a computable version.
Equations
- is_unit.lift_right f hf = units.lift_right f (λ (x : M), classical.some _) _
If a homomorphism f : M →+ N
sends each element to an is_add_unit
, then it can be
lifted to f : M →+ add_units N
. See also add_units.lift_right
for a computable version.