English
If f : G →* M is a group-to-monoid homomorphism, then its image lies in the units of M, and f.toHomUnits defines a monoid homomorphism G →* Mˣ extracting the corresponding unit-valued map.
Русский
Пусть f : G →* M — гомоморфизм между группой G и моноидом M. Тогда образ f лежит в единицах M, и f.toHomUnits задаёт гомоморфизм G →* Mˣ, соответствующий маппингу в единицы.
LaTeX
$$$f: G \\to^* M \\implies f( g ) \\in M^{\\times} \\text{ for all } g, \\quad f^{\\mathrm{toHomUnits}}: G \\to^* M^{\\times},$$$
Lean4
/-- 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ˣ`. -/
@[to_additive /-- 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`. -/
]
def toHomUnits (f : G →* M) : G →* Mˣ :=
Units.liftRight f (fun g => ⟨f g, f g⁻¹, map_mul_eq_one f (mul_inv_cancel _), map_mul_eq_one f (inv_mul_cancel _)⟩)
fun _ => rfl
