mathlib documentation

Gelfand Duality #

The gelfand_transform is an algebra homomorphism from a topological π•œ-algebra A to C(character_space π•œ A, π•œ). In the case where A is a commutative complex Banach algebra, then the Gelfand transform is actually spectrum-preserving (spectrum.gelfand_transform_eq). Moreover, when A is a commutative C⋆-algebra over β„‚, then the Gelfand transform is a surjective isometry, and even an equivalence between C⋆-algebras.

Main definitions #

Main statements #


Tags #

Gelfand transform, character space, C⋆-algebra

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 weak_dual.character_space.equiv_alg_hom, is given by the composition of the quotient map and the Gelfand-Mazur isomorphism normed_ring.alg_equiv_complex_of_complete.


If a : A is not a unit, then some character takes the value zero at a. This is equivlaent to gelfand_transform β„‚ A a takes the value zero at some character.

The Gelfand transform is spectrum-preserving.

The Gelfand transform is an isometry when the algebra is a C⋆-algebra over β„‚.

The Gelfand transform is bijective when the algebra is a C⋆-algebra over β„‚.

The Gelfand transform as a star_alg_equiv between a commutative unital C⋆-algebra over β„‚ and the continuous functions on its character_space.


The functorial map taking ψ : A →⋆ₐ[β„‚] B to a continuous function character_space β„‚ B β†’ character_space β„‚ A obtained by pre-composition with ψ.