starLift_range — Mathlib

English

The unitization of a nonunital star subalgebra yields a canonical star algebra homomorphism to its adjoin.

Русский

Единичизация неединичного звездного подалгебра образует каноническое звездное гомоморфизм к его порождающему адъюнту.

LaTeX

$$$\mathrm{unitization} : \mathrm{Unitization}\;R\;s \to_\star[R] A$$$

Lean4

theorem starLift_range (f : A →⋆ₙₐ[R] C) :
    (starLift f).range = StarAlgebra.adjoin R (NonUnitalStarAlgHom.range f : Set C) :=
  eq_of_forall_ge_iff fun c ↦ by
    rw [starLift_range_le, StarAlgebra.adjoin_le_iff]
    rfl

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