mathlib3 documentation

Gelfand Duality #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ψ.