English
Every maximal ideal I in a commutative complex Banach algebra produces a character, i.e., a nonzero algebra homomorphism to ℂ, via the quotient and the Gelfand–Mazur isomorphism.
Русский
Каждая максимальная идеал I в коммутативной комплексной банаховой алгебре порождает характер, то есть ненуломое алгебраическое гомоморфное отображение в ℂ, через фактор-оно и тождество Гельфанда– mazура.
LaTeX
$$$$I \to\text{CharacterSpace}$$$$
Lean4
/-- Every maximal ideal in a commutative complex Banach algebra gives rise to a character on that
algebra. In particular, the character, which may be identified as an algebra homomorphism due to
`WeakDual.CharacterSpace.equivAlgHom`, is given by the composition of the quotient map and
the Gelfand-Mazur isomorphism `NormedRing.algEquivComplexOfComplete`. -/
noncomputable def toCharacterSpace : characterSpace ℂ A :=
CharacterSpace.equivAlgHom.symm <|
((NormedRing.algEquivComplexOfComplete
(letI := Quotient.field I;
isUnit_iff_ne_zero (G₀ := A ⧸ I))).symm :
A ⧸ I →ₐ[ℂ] ℂ).comp <|
Quotient.mkₐ ℂ I
