ofInjective — Mathlib

English

The range of a StarAlgHom φ equals the top subalgebra of A mapped by φ.

Русский

Образ StarAlgHom φ равен верхнему подалгебре, отображаемому φ.

LaTeX

$$$ \\mathrm{range}(\\varphi) = (\\top : StarSubalgebra R A).map \\varphi $$$

Lean4

/-- The `StarAlgEquiv` onto the range corresponding to an injective `StarAlgHom`. -/
@[simps]
noncomputable def _root_.StarAlgEquiv.ofInjective (f : A →⋆ₐ[R] B) (hf : Function.Injective f) : A ≃⋆ₐ[R] f.range :=
  { AlgEquiv.ofInjective (f : A →ₐ[R] B) hf with
    toFun := f.rangeRestrict
    map_star' := fun a => Subtype.ext (map_star f a)
    map_smul' := fun r a => Subtype.ext (map_smul f r a) }

Похожие утверждения