English
StarMap is defined by lifting a nonunital star map to a unital star map between unitizations.
Русский
StarMap определяется подъемом неединичного звездного отображения к единичному звездному отображению между единичизациями.
LaTeX
$$$\text{starMap}(\varphi) = \text{lift}(\varphi)\,.$$$
Lean4
/-- The functorial map on morphisms between the category of non-unital C⋆-algebras with non-unital
star homomorphisms and unital C⋆-algebras with unital star homomorphisms.
This sends `φ : A →⋆ₙₐ[R] B` to a map `Unitization R A →⋆ₐ[R] Unitization R B` given by the formula
`(r, a) ↦ (r, φ a)` (or perhaps more precisely,
`algebraMap R _ r + ↑a ↦ algebraMap R _ r + ↑(φ a)`). -/
@[simps!]
def starMap (φ : A →⋆ₙₐ[R] B) : Unitization R A →⋆ₐ[R] Unitization R B :=
Unitization.starLift <| (Unitization.inrNonUnitalStarAlgHom R B).comp φ
