English
If g is a left inverse of f (i.e., g ∘ f = id_A), then restricting the codomain of f to its range yields a star algebra isomorphism between A and range(f).
Русский
Если g является левым обратным к f (g ∘ f = id_A), то ограничение кодом f до диапазона даёт звездоалгебраическое изоморфизм между A и range(f).
LaTeX
$$$A \cong_R \mathrm{range}(f)$ via \mathrm{rangeRestrict}(f) with inverse g \circ \iota_{\mathrm{range}(f)}$ where ι is the inclusion.$$
Lean4
/-- Restrict a non-unital star algebra homomorphism with a left inverse to an algebra isomorphism
to its range.
This is a computable alternative to `StarAlgEquiv.ofInjective`. -/
def ofLeftInverse' {g : B → A} {f : F} (h : Function.LeftInverse g f) : A ≃⋆ₐ[R] NonUnitalStarAlgHom.range f :=
{
NonUnitalStarAlgHom.rangeRestrict
f with
toFun := NonUnitalStarAlgHom.rangeRestrict f
invFun := g ∘ (NonUnitalStarSubalgebraClass.subtype <| NonUnitalStarAlgHom.range f)
left_inv := h
right_inv := fun x =>
Subtype.ext <|
let ⟨x', hx'⟩ := (NonUnitalStarAlgHom.mem_range f).mp x.prop
show f (g x) = x by rw [← hx', h x'] }
