# mathlib3documentation

analysis.normed_space.star.gelfand_duality

# 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 #

• 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 →⋆ₐ[ℂ] B to a continuous function character_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, realize gelfand_transform as a star_alg_equiv.
• Prove that if A is the unital C⋆-algebra over ℂ generated by a fixed normal element x in a larger C⋆-algebra B, then character_space ℂ A is homeomorphic to spectrum ℂ x.
• From the previous result, construct the continuous functional calculus.
• Show that if X is a compact Hausdorff space, then X is (canonically) homeomorphic to character_space ℂ C(X, ℂ).
• Conclude using the previous fact that the functors C(⬝, ℂ) and 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.

## Tags #

Gelfand transform, character space, C⋆-algebra

noncomputable def ideal.to_character_space {A : Type u_1} [ A] (I : ideal A) [I.is_maximal] :

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.

Equations
theorem ideal.to_character_space_apply_eq_zero_of_mem {A : Type u_1} [ A] (I : ideal A) [I.is_maximal] {a : A} (ha : a I) :
theorem weak_dual.character_space.exists_apply_eq_zero {A : Type u_1} [ A] {a : A} (ha : ¬) :
(f : , f a = 0

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.

theorem weak_dual.character_space.mem_spectrum_iff_exists {A : Type u_1} [ A] {a : A} {z : } :
z (f : , f a = z
theorem spectrum.gelfand_transform_eq {A : Type u_1} [ A] (a : A) :
a) =

The Gelfand transform is spectrum-preserving.

@[protected, instance]
theorem gelfand_transform_map_star {A : Type u_1} [ A] [star_ring A] [cstar_ring A] [ A] (a : A) :
theorem gelfand_transform_isometry (A : Type u_1) [ A] [star_ring A] [cstar_ring A] [ A] :

The Gelfand transform is an isometry when the algebra is a C⋆-algebra over ℂ.

theorem gelfand_transform_bijective (A : Type u_1) [ A] [star_ring A] [cstar_ring A] [ A] :

The Gelfand transform is bijective when the algebra is a C⋆-algebra over ℂ.

@[simp]
theorem gelfand_star_transform_apply_apply (A : Type u_1) [ A] [star_ring A] [cstar_ring A] [ A] (a : A) (φ : ) :
a) φ = φ a
noncomputable def gelfand_star_transform (A : Type u_1) [ A] [star_ring A] [cstar_ring A] [ A] :

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

Equations
@[simp]
theorem gelfand_star_transform_symm_apply (A : Type u_1) [ A] [star_ring A] [cstar_ring A] [ A] (ᾰ : C(, )) :
.symm) = ((ring_equiv.of_bijective {to_fun := , map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _, map_star' := _} _).symm)
@[simp]
theorem weak_dual.character_space.comp_continuous_map_apply {A : Type u_1} {B : Type u_2} [normed_ring A] [ A] [star_ring A] [normed_ring B] [ B] [star_ring B] (ψ : A →⋆ₐ[] B) (φ : ) :
noncomputable def weak_dual.character_space.comp_continuous_map {A : Type u_1} {B : Type u_2} [normed_ring A] [ A] [star_ring A] [normed_ring B] [ B] [star_ring B] (ψ : A →⋆ₐ[] B) :

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

Equations
@[simp]

weak_dual.character_space.comp_continuous_map sends the identity to the identity.

@[simp]
theorem weak_dual.character_space.comp_continuous_map_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [normed_ring A] [ A] [star_ring A] [normed_ring B] [ B] [star_ring B] [normed_ring C] [ C] [star_ring C] (ψ₂ : B →⋆ₐ[] C) (ψ₁ : A →⋆ₐ[] B) :

weak_dual.character_space.comp_continuous_map is functorial.