English
There is a canonical equivalence lifting nonunital maps to unital maps on unitizations; this is the universal property of Unitization.
Русский
Существует каноническое эквивалентное отображение, поднимающее неединичные отображения к единичным отображениям на единичизациях; это универсальное свойство единичизации.
LaTeX
$$$\text{ lift } : (A \to_{NU}^R C) \cong (Unitization(R,A) \to_{Alg}^R C)$$$
Lean4
/-- Non-unital algebra homomorphisms from `A` into a unital `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 lift : (A →ₙₐ[R] C) ≃ (Unitization R A →ₐ[R] C)
where
toFun := NonUnitalAlgHom.toAlgHom
invFun φ := φ.toNonUnitalAlgHom.comp (inrNonUnitalAlgHom R A)
left_inv φ := by ext; simp [NonUnitalAlgHomClass.toNonUnitalAlgHom]
right_inv φ := by ext; simp [NonUnitalAlgHomClass.toNonUnitalAlgHom]
