Theorems · Definition · functional analysis

Ideal.toCharacterSpace

{A : Type u_1} →
  [inst : NormedCommRing A] →
    [inst_1 : NormedAlgebra ℂ A] → [CompleteSpace A] → (I : Ideal A) → [I.IsMaximal] → ↑(WeakDual.characterSpace ℂ A)

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.

Defined in

Mathlib.Analysis.CStarAlgebra.GelfandDuality

Cited by

2 results in Mathlib

Foundations

Depth 298 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedCommRingNormedAlgebraCompleteSpaceIdeal.IsMaximal