Lift monoid homomorphisms to group homomorphisms of their units subgroups.
The group homomorphism on units induced by a
units M → M as a monoid homomorphism.
add_units M → M as an add_monoid homomorphism.
If a map
g : M → units N agrees with a homomorphism
f : M →* N, then
this map is a monoid homomorphism too.
If a map
g : M → add_units N agrees with a homomorphism
f : M →+ N, then this map
is an add_monoid homomorphism too.
f is a homomorphism from an additive group
G to an additive monoid
then its image lies in the
f.to_hom_units is the corresponding homomorphism from
f is a homomorphism from a group
G to a monoid
then its image lies in the units of
f.to_hom_units is the corresponding monoid homomorphism from
If a homomorphism
f : M →* N sends each element to an
is_unit, then it can be lifted
f : M →* units N. See also
units.lift_right for a computable version.