English
If g is a left inverse of f: R →+* S, then there is a RingEquiv between R and the range of f, whose forward map is f and whose inverse is g restricted to the range.
Русский
Если g — левообратная к f: R →+* S, то существует кольцевое равнообразие между R и образом f, переходом которого является f, а обратное — ограничение g на образе.
LaTeX
$$$ \\exists \\mathrm{RingEquiv} \\; R \\; (f: R \\to+* S) \\; (g: S \\to R) \\; (h: \\mathrm{LeftInverse} \\, g \\, f) : R \\cong+* f.range $$$
Lean4
/-- Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
`RingHom.range`. -/
def ofLeftInverse {g : S → R} {f : R →+* S} (h : Function.LeftInverse g f) : R ≃+* f.range :=
{ f.rangeRestrict with
toFun := fun x => f.rangeRestrict x
invFun := fun x => (g ∘ f.range.subtype) x
left_inv := h
right_inv := fun x =>
Subtype.ext <|
let ⟨x', hx'⟩ := RingHom.mem_range.mp x.prop
show f (g x) = x by rw [← hx', h x'] }
