English
Let φ be a character (a unital algebra homomorphism from A to 𝕜). Then there is a canonical associated algebra homomorphism toAlgHom(φ) : A →𝕜 𝕜, defined by the same underlying map as φ and preserving 1 (map_one) and commuting with scalar multiplication.
Русский
Пусть φ — характер (унитальный алгебра-гомоморфизм из A в 𝕜). Тогда существует канонически связанный алгебра-гомоморфизм toAlgHom(φ) : A →𝕜 𝕜, который имеет ту же кольцевую структуру, сохраняет единицу и коммутирует со скалярами.
LaTeX
$$$\forall \phi \in \mathrm{characterSpace}_{\mathbb{k}}(A),\; (\mathrm{toAlgHom}(\phi): A \to_{\mathbb{k}} \mathbb{k})\text{ is the unital algebra hom given by } a \mapsto \phi(a).$$$
Lean4
/-- An element of the character space of a unital algebra, as an algebra homomorphism. -/
@[simps]
def toAlgHom (φ : characterSpace 𝕜 A) : A →ₐ[𝕜] 𝕜 :=
{ toNonUnitalAlgHom φ with
map_one' := map_one φ
commutes' := AlgHomClass.commutes φ }
