equivAlgHom — Mathlib

English

There is a natural equivalence between the space of characters on a normed algebra and the space of algebra homomorphisms from the algebra to the base field.

Русский

Существует естественное эквивалентное соотношение между пространством характеров и алгебраических гомоморфизмов в базовое поле.

LaTeX

$$characterSpace 𝕜 A ≃ (A →ₐ[𝕜] 𝕜)$$

Lean4

/-- The equivalence between characters and algebra homomorphisms into the base field. -/
def equivAlgHom : characterSpace 𝕜 A ≃ (A →ₐ[𝕜] 𝕜)
    where
  toFun := toAlgHom
  invFun
    f :=
    { val := f.toContinuousLinearMap
      property := by rw [eq_set_map_one_map_mul]; exact ⟨map_one f, map_mul f⟩ }

Похожие утверждения