English
Given a left inverse h of f, one can construct an algebra equivalence between A and the range of f using the left inverse and the restricted map.
Русский
Пусть h — левый обратный к f. Тогда существует алгебраическое эквивалентство между A и образoм f, получаемое из ограниченного отображения и левого обратного.
LaTeX
$$$\text{ofLeftInverse}(h) : A \simeq_R f.range$$$
Lean4
/-- Restrict an algebra homomorphism with a left inverse to an algebra isomorphism to its range.
This is a computable alternative to `AlgEquiv.ofInjective`. -/
def ofLeftInverse {g : B → A} {f : A →ₐ[R] B} (h : Function.LeftInverse g f) : A ≃ₐ[R] f.range :=
{ f.rangeRestrict with
toFun := f.rangeRestrict
invFun := g ∘ f.range.val
left_inv := h
right_inv := fun x =>
Subtype.ext <|
let ⟨x', hx'⟩ := f.mem_range.mp x.prop
show f (g x) = x by rw [← hx', h x'] }
