ker_isMaximal — Mathlib

English

The character space equals the set of all multiplicative unital linear functionals on A; equivalently, characters are exactly unital algebra homomorphisms A → 𝕜.

Русский

Множество характеров равно множеству всех мультипликативных линейных функционалов A → 𝕜; иначе говоря, характеры — это точно унитальные алгебра-гомоморфизмы A → 𝕜.

LaTeX

$$$\mathrm{Char}_{\mathbb{k}}(A) = \{ \phi: A \to \mathbb{k} \mid \phi \text{ multiplicative and unital} \}.$$$

Lean4

/-- The `RingHom.ker` of `φ : characterSpace 𝕜 A` is maximal. -/
instance ker_isMaximal (φ : characterSpace 𝕜 A) : (RingHom.ker φ).IsMaximal :=
  RingHom.ker_isMaximal_of_surjective φ fun z ↦ ⟨algebraMap 𝕜 A z, by simp [AlgHomClass.commutes]⟩

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