English
There is a noncomputable lifting construction IsUnit.liftRight that, given a monoid hom f and a proof that every f x is a unit, yields a monoid homomorphism M →* Nˣ extending f to units.
Русский
Существуют непосредственные подстановки IsUnit.liftRight: если f : M →* N и для каждого x есть единица f(x), то получается моноидоморфизм M →* Nˣ расширяющий f до единиц.
LaTeX
$$$\\operatorname{IsUnit.liftRight}(f,hf) : M \\to^* N^{\\times}$$$
Lean4
/-- 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. -/
@[to_additive /-- 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. -/
]
noncomputable def liftRight (f : M →* N) (hf : ∀ x, IsUnit (f x)) : M →* Nˣ :=
(Units.liftRight f fun x => (hf x).unit) fun _ => rfl
