Gelfand Duality #
gelfand_transform is an algebra homomorphism from a topological
C(character_space 𝕜 A, 𝕜). In the case where
A is a commutative complex Banach algebra, then
the Gelfand transform is actually spectrum-preserving (
A is a commutative C⋆-algebra over
ℂ, then the Gelfand transform is a surjective isometry,
and even an equivalence between C⋆-algebras.
Main definitions #
ideal.to_character_space: constructs an element of the character space from a maximal ideal in a commutative complex Banach algebra
weak_dual.character_space.comp_continuous_map: The functorial map taking
ψ : A →⋆ₐ[ℂ] Bto a continuous function
character_space ℂ B → character_space ℂ Agiven by pre-composition with
Main statements #
spectrum.gelfand_transform_eq: the Gelfand transform is spectrum-preserving when the algebra is a commutative complex Banach algebra.
gelfand_transform_isometry: the Gelfand transform is an isometry when the algebra is a commutative (unital) C⋆-algebra over
gelfand_transform_bijective: the Gelfand transform is bijective when the algebra is a commutative (unital) C⋆-algebra over
star_alg_equivis defined, realize
- Prove that if
Ais the unital C⋆-algebra over
ℂgenerated by a fixed normal element
xin a larger C⋆-algebra
character_space ℂ Ais homeomorphic to
spectrum ℂ x.
- From the previous result, construct the continuous functional calculus.
- Show that if
Xis a compact Hausdorff space, then
Xis (canonically) homeomorphic to
character_space ℂ C(X, ℂ).
- Conclude using the previous fact that the functors
character_space ℂ ⬝along with the canonical homeomorphisms described above constitute a natural contravariant equivalence of the categories of compact Hausdorff spaces (with continuous maps) and commutative unital C⋆-algebras (with unital ⋆-algebra homomoprhisms); this is known as Gelfand duality.
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
a : A is not a unit, then some character takes the value zero at
a. This is equivlaent
gelfand_transform ℂ A a takes the value zero at some character.
The Gelfand transform as a
star_alg_equiv between a commutative unital C⋆-algebra over
and the continuous functions on its
The functorial map taking
ψ : A →⋆ₐ[ℂ] B to a continuous function
character_space ℂ B → character_space ℂ A obtained by pre-composition with
weak_dual.character_space.comp_continuous_map sends the identity to the identity.
weak_dual.character_space.comp_continuous_map is functorial.