English
The starLift construction intertwines with ext lemmas to produce star-algebra extensionality results.
Русский
Конструкция starLift взаимодействует с леммами экстензии, создавая результаты экстензии звездной алгебры.
LaTeX
$$$\text{ext}_{\mathrm{star}} : \ldots$$$
Lean4
/-- Non-unital star algebra homomorphisms from `A` into a unital star `R`-algebra `C` lift uniquely
to `Unitization R A →⋆ₐ[R] C`. This is the universal property of the unitization. -/
@[simps! apply symm_apply apply_apply]
def starLift : (A →⋆ₙₐ[R] C) ≃ (Unitization R A →⋆ₐ[R] C) :=
{ toFun := fun φ ↦
{ toAlgHom := Unitization.lift φ.toNonUnitalAlgHom
map_star' := fun x => by simp [map_star] }
invFun := fun φ ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A), left_inv := fun φ => by ext; simp,
right_inv := fun φ => Unitization.algHom_ext'' <| by simp }
