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 #
ideal.to_character_space
: constructs an element of the character space from a maximal ideal in a commutative complex Banach algebraweak_dual.character_space.comp_continuous_map
: The functorial map takingΟ : A βββ[β] B
to a continuous functioncharacter_space β B β character_space β A
given 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β
.
TODO #
- After
star_alg_equiv
is defined, realizegelfand_transform
as astar_alg_equiv
. - Prove that if
A
is the unital Cβ-algebra overβ
generated by a fixed normal elementx
in a larger Cβ-algebraB
, thencharacter_space β A
is homeomorphic tospectrum β x
. - From the previous result, construct the continuous functional calculus.
- Show that if
X
is a compact Hausdorff space, thenX
is (canonically) homeomorphic tocharacter_space β C(X, β)
. - Conclude using the previous fact that the functors
C(β¬, β)
andcharacter_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.
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
.
Equations
- gelfand_star_transform A = star_alg_equiv.of_bijective (show A βββ[β] C(β₯(weak_dual.character_space β A), β), from {to_fun := (weak_dual.gelfand_transform β A).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _, map_star' := _}) _
The functorial map taking Ο : A βββ[β] B
to a continuous function
character_space β B β character_space β A
obtained by pre-composition with Ο
.
Equations
weak_dual.character_space.comp_continuous_map
sends the identity to the identity.
weak_dual.character_space.comp_continuous_map
is functorial.