English
If there exists a left inverse g of f: G →* N (i.e., g ∘ f = id_G), then G is canonically isomorphic to the range of f via a multiplicative equivalence.
Русский
Если существует левый обратный g к f: G →* N (то есть g ∘ f = id_G), то G изоморфна образу f через мультипликативное эквививентное отображение.
LaTeX
$$$$ \\exists\, g: N \\to G \\text{ with } g \\circ f = \\mathrm{id}_G \\;\Longrightarrow\\; G \\cong_* \\mathrm{Im}(f) $$$$
Lean4
/-- Computable alternative to `MonoidHom.ofInjective`. -/
@[to_additive /-- Computable alternative to `AddMonoidHom.ofInjective`. -/
]
def ofLeftInverse {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) : G ≃* f.range :=
{ f.rangeRestrict with
toFun := f.rangeRestrict
invFun := g ∘ f.range.subtype
left_inv := h
right_inv := by
rintro ⟨x, y, rfl⟩
solve_by_elim }
