English
Nonunital algebra homomorphisms A →⋆ₙₐ[R] C lift uniquely to unital algebra homomorphisms Unitization R A →⋆ₐ[R] C; this gives a universal property of unitization.
Русский
Неединаковные алгебра-гомоморфизмы A →⋆ₙₐ[R] C поднимаются уникально к единичным алгебра-гомоморфизмам Unitization R A →⋆ₐ[R] C; это универсальное свойство единичизации.
LaTeX
$$$(A \to_{NU}^R C) \simeq (Unitization(R,A) \to_{R\text{-Alg}} C).$$$
Lean4
/-- See note [partially-applied ext lemmas] -/
@[ext 1100]
theorem algHom_ext' {φ ψ : Unitization R A →ₐ[R] C}
(h : φ.toNonUnitalAlgHom.comp (inrNonUnitalAlgHom R A) = ψ.toNonUnitalAlgHom.comp (inrNonUnitalAlgHom R A)) :
φ = ψ :=
algHom_ext'' (NonUnitalAlgHom.congr_fun h)
