mathlib3 documentation

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} [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] (I : ideal A) [I.is_maximal] :

↥(weak_dual.character_space ℂ A)

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

I.to_character_space = ⇑(weak_dual.character_space.equiv_alg_hom.symm) (↑((normed_ring.alg_equiv_complex_of_complete _).symm).comp (ideal.quotient.mkₐ ℂ I))

theorem ideal.to_character_space_apply_eq_zero_of_mem {A : Type u_1} [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] (I : ideal A) [I.is_maximal] {a : A} (ha : a ∈ I) :

⇑(I.to_character_space) a = 0

theorem weak_dual.character_space.exists_apply_eq_zero {A : Type u_1} [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] {a : A} (ha : ¬is_unit a) :

∃ (f : ↥(weak_dual.character_space ℂ A)), ⇑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} [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] {a : A} {z : ℂ} :

z ∈ spectrum ℂ a ↔ ∃ (f : ↥(weak_dual.character_space ℂ A)), ⇑f a = z

theorem spectrum.gelfand_transform_eq {A : Type u_1} [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] (a : A) :

spectrum ℂ (⇑(weak_dual.gelfand_transform ℂ A) a) = spectrum ℂ a

The Gelfand transform is spectrum-preserving.

@[protected, instance]

def weak_dual.character_space.nonempty {A : Type u_1} [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] [nontrivial A] :

nonempty ↥(weak_dual.character_space ℂ A)

theorem gelfand_transform_map_star {A : Type u_1} [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] [star_ring A] [cstar_ring A] [star_module ℂ A] (a : A) :

⇑(weak_dual.gelfand_transform ℂ A) (has_star.star a) = has_star.star (⇑(weak_dual.gelfand_transform ℂ A) a)

theorem gelfand_transform_isometry (A : Type u_1) [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] [star_ring A] [cstar_ring A] [star_module ℂ A] :

isometry ⇑(weak_dual.gelfand_transform ℂ A)

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

theorem gelfand_transform_bijective (A : Type u_1) [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] [star_ring A] [cstar_ring A] [star_module ℂ A] :

function.bijective ⇑(weak_dual.gelfand_transform ℂ 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) [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] [star_ring A] [cstar_ring A] [star_module ℂ A] (a : A) (φ : ↥(weak_dual.character_space ℂ A)) :

⇑(⇑(gelfand_star_transform A) a) φ = ⇑φ a

noncomputable def gelfand_star_transform (A : Type u_1) [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] [star_ring A] [cstar_ring A] [star_module ℂ A] :

A ≃⋆ₐ[ℂ ] C(↥(weak_dual.character_space ℂ 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

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' := _}) _

@[simp]

theorem gelfand_star_transform_symm_apply (A : Type u_1) [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A] [star_ring A] [cstar_ring A] [star_module ℂ A] (ᾰ : C(↥(weak_dual.character_space ℂ A), ℂ )) :

⇑((gelfand_star_transform A).symm) ᾰ = ⇑((ring_equiv.of_bijective {to_fun := ⇑(weak_dual.gelfand_transform ℂ A), 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] [normed_algebra ℂ A] [complete_space A] [star_ring A] [normed_ring B] [normed_algebra ℂ B] [complete_space B] [star_ring B] (ψ : A →⋆ₐ[ℂ ] B) (φ : ↥(weak_dual.character_space ℂ B)) :

⇑(weak_dual.character_space.comp_continuous_map ψ) φ = ⇑(weak_dual.character_space.equiv_alg_hom.symm) ((⇑weak_dual.character_space.equiv_alg_hom φ).comp ψ.to_alg_hom)

noncomputable def weak_dual.character_space.comp_continuous_map {A : Type u_1} {B : Type u_2} [normed_ring A] [normed_algebra ℂ A] [complete_space A] [star_ring A] [normed_ring B] [normed_algebra ℂ B] [complete_space B] [star_ring B] (ψ : A →⋆ₐ[ℂ ] B) :

C(↥(weak_dual.character_space ℂ B), ↥(weak_dual.character_space ℂ A))

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 ψ = {to_fun := λ (φ : ↥(weak_dual.character_space ℂ B)), ⇑(weak_dual.character_space.equiv_alg_hom.symm) ((⇑weak_dual.character_space.equiv_alg_hom φ).comp ψ.to_alg_hom), continuous_to_fun := _}

@[simp]

theorem weak_dual.character_space.comp_continuous_map_id (A : Type u_1) [normed_ring A] [normed_algebra ℂ A] [complete_space A] [star_ring A] :

weak_dual.character_space.comp_continuous_map (star_alg_hom.id ℂ A) = continuous_map.id ↥(weak_dual.character_space ℂ A)

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] [normed_algebra ℂ A] [complete_space A] [star_ring A] [normed_ring B] [normed_algebra ℂ B] [complete_space B] [star_ring B] [normed_ring C] [normed_algebra ℂ C] [complete_space C] [star_ring C] (ψ₂ : B →⋆ₐ[ℂ ] C) (ψ₁ : A →⋆ₐ[ℂ ] B) :

weak_dual.character_space.comp_continuous_map (ψ₂.comp ψ₁) = (weak_dual.character_space.comp_continuous_map ψ₁).comp (weak_dual.character_space.comp_continuous_map ψ₂)

weak_dual.character_space.comp_continuous_map is functorial.