Gelfand Duality

The gelfandTransform is an algebra homomorphism from a topological 𝕜-algebra A to C(characterSpace 𝕜 A, 𝕜). In the case where A is a commutative complex Banach algebra, then the Gelfand transform is actually spectrum-preserving (spectrum.gelfandTransform_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.

Consider the contravariant functors between compact Hausdorff spaces and commutative unital C⋆algebras F : Cpct → CommCStarAlg := X ↦ C(X, ℂ) and G : CommCStarAlg → Cpct := A → characterSpace ℂ A whose actions on morphisms are given by WeakDual.CharacterSpace.compContinuousMap and ContinuousMap.compStarAlgHom', respectively.

Then η₁ : id → F ∘ G := gelfandStarTransform and η₂ : id → G ∘ F := WeakDual.CharacterSpace.homeoEval are the natural isomorphisms implementing Gelfand Duality, i.e., the (contravariant) equivalence of these categories.

Main definitions

• Ideal.toCharacterSpace : constructs an element of the character space from a maximal ideal in a commutative complex Banach algebra
• WeakDual.CharacterSpace.compContinuousMap: The functorial map taking ψ : A →⋆ₐ[𝕜] B to a continuous function characterSpace 𝕜 B → characterSpace 𝕜 A given by pre-composition with ψ.

Main statements

• spectrum.gelfandTransform_eq : the Gelfand transform is spectrum-preserving when the algebra is a commutative complex Banach algebra.
• gelfandTransform_isometry : the Gelfand transform is an isometry when the algebra is a commutative (unital) C⋆-algebra over ℂ.
• gelfandTransform_bijective : the Gelfand transform is bijective when the algebra is a commutative (unital) C⋆-algebra over ℂ.
• gelfandStarTransform_naturality: The gelfandStarTransform is a natural isomorphism
• WeakDual.CharacterSpace.homeoEval_naturality: This map implements a natural isomorphism

TODO

• After defining the category of commutative unital C⋆-algebras, bundle the existing unbundled Gelfand duality into an actual equivalence (duality) of categories associated to the functors C(·, ℂ) and characterSpace ℂ · and the natural isomorphisms gelfandStarTransform and WeakDual.CharacterSpace.homeoEval.

Tags

Gelfand transform, character space, C⋆-algebra

noncomputable def Ideal.toCharacterSpace {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (I : Ideal A) [I.IsMaximal] : ↑(WeakDual.characterSpace ℂ 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 WeakDual.CharacterSpace.equivAlgHom, is given by the composition of the quotient map and the Gelfand-Mazur isomorphism NormedRing.algEquivComplexOfComplete.

Equations

• I.toCharacterSpace = WeakDual.CharacterSpace.equivAlgHom.symm ((↑(NormedRing.algEquivComplexOfComplete ⋯).symm).comp (Ideal.Quotient.mkₐ ℂ I))

theorem Ideal.toCharacterSpace_apply_eq_zero_of_mem {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (I : Ideal A) [I.IsMaximal] {a : A} (ha : a ∈ I) : I.toCharacterSpace a = 0

theorem WeakDual.CharacterSpace.exists_apply_eq_zero {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] {a : A} (ha : ¬IsUnit a) : ∃ (f : ↑(WeakDual.characterSpace ℂ A)), f a = 0

If a : A is not a unit, then some character takes the value zero at a. This is equivalent to gelfandTransform ℂ A a takes the value zero at some character.

theorem WeakDual.CharacterSpace.mem_spectrum_iff_exists {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] {a : A} {z : ℂ} : z ∈ spectrum ℂ a ↔ ∃ (f : ↑(WeakDual.characterSpace ℂ A)), f a = z

theorem spectrum.gelfandTransform_eq {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) : spectrum ℂ ((WeakDual.gelfandTransform ℂ A) a) = spectrum ℂ a

The Gelfand transform is spectrum-preserving.

instance instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] : Nonempty ↑(WeakDual.characterSpace ℂ A)

Equations

• ⋯ = ⋯

theorem gelfandTransform_map_star {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] (a : A) : (WeakDual.gelfandTransform ℂ A) (star a) = star ((WeakDual.gelfandTransform ℂ A) a)

theorem gelfandTransform_isometry (A : Type u_1) [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] : Isometry ⇑(WeakDual.gelfandTransform ℂ A)

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

theorem gelfandTransform_bijective (A : Type u_1) [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] : Function.Bijective ⇑(WeakDual.gelfandTransform ℂ A)

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

@[simp]

theorem gelfandStarTransform_symm_apply (A : Type u_1) [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] : ∀ (a : C(↑(WeakDual.characterSpace ℂ A), ℂ)), (gelfandStarTransform A).symm a = (↑(RingEquiv.ofBijective { toAlgHom := WeakDual.gelfandTransform ℂ A, map_star' := ⋯ } ⋯)).symm a

@[simp]

theorem gelfandStarTransform_apply_apply (A : Type u_1) [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] (a : A) (φ : ↑(WeakDual.characterSpace ℂ A)) : ((gelfandStarTransform A) a) φ = φ a

noncomputable def gelfandStarTransform (A : Type u_1) [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] : A ≃⋆ₐ[ℂ] C(↑(WeakDual.characterSpace ℂ A), ℂ)

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

Equations

• gelfandStarTransform A = StarAlgEquiv.ofBijective (let_fun this := let __src := WeakDual.gelfandTransform ℂ A; { toAlgHom := __src, map_star' := ⋯ }; this) ⋯

@[simp]

theorem WeakDual.CharacterSpace.compContinuousMap_apply {A : Type u_1} {B : Type u_2} {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [StarRing A] [NormedRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] [StarRing B] (ψ : A →⋆ₐ[𝕜] B) (φ : ↑(WeakDual.characterSpace 𝕜 B)) : (WeakDual.CharacterSpace.compContinuousMap ψ) φ = WeakDual.CharacterSpace.equivAlgHom.symm ((WeakDual.CharacterSpace.equivAlgHom φ).comp ψ.toAlgHom)

noncomputable def WeakDual.CharacterSpace.compContinuousMap {A : Type u_1} {B : Type u_2} {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [StarRing A] [NormedRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] [StarRing B] (ψ : A →⋆ₐ[𝕜] B) : C(↑(WeakDual.characterSpace 𝕜 B), ↑(WeakDual.characterSpace 𝕜 A))

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeakDual.CharacterSpace.compContinuousMap_id (A : Type u_1) {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [StarRing A] : WeakDual.CharacterSpace.compContinuousMap (StarAlgHom.id 𝕜 A) = ContinuousMap.id ↑(WeakDual.characterSpace 𝕜 A)

WeakDual.CharacterSpace.compContinuousMap sends the identity to the identity.

@[simp]

theorem WeakDual.CharacterSpace.compContinuousMap_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [StarRing A] [NormedRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] [StarRing B] [NormedRing C] [NormedAlgebra 𝕜 C] [CompleteSpace C] [StarRing C] (ψ₂ : B →⋆ₐ[𝕜] C) (ψ₁ : A →⋆ₐ[𝕜] B) : WeakDual.CharacterSpace.compContinuousMap (ψ₂.comp ψ₁) = (WeakDual.CharacterSpace.compContinuousMap ψ₁).comp (WeakDual.CharacterSpace.compContinuousMap ψ₂)

WeakDual.CharacterSpace.compContinuousMap is functorial.

theorem gelfandStarTransform_naturality {A : Type u_1} {B : Type u_2} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] [NormedCommRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [StarRing B] [CstarRing B] [StarModule ℂ B] (φ : A →⋆ₐ[ℂ] B) : (↑(gelfandStarTransform B)).comp φ = (ContinuousMap.compStarAlgHom' ℂ ℂ (WeakDual.CharacterSpace.compContinuousMap φ)).comp ↑(gelfandStarTransform A)

Consider the contravariant functors between compact Hausdorff spaces and commutative unital C⋆algebras F : Cpct → CommCStarAlg := X ↦ C(X, ℂ) and G : CommCStarAlg → Cpct := A → characterSpace ℂ A whose actions on morphisms are given by WeakDual.CharacterSpace.compContinuousMap and ContinuousMap.compStarAlgHom', respectively.

Then η : id → F ∘ G := gelfandStarTransform is a natural isomorphism implementing (half of) the duality between these categories. That is, for commutative unital C⋆-algebras A and B and φ : A →⋆ₐ[ℂ] B the following diagram commutes:

A  --- η A ---> C(characterSpace ℂ A, ℂ)

|                     |

φ                  (F ∘ G) φ

|                     |
V                     V

B  --- η B ---> C(characterSpace ℂ B, ℂ)

theorem WeakDual.CharacterSpace.homeoEval_naturality {X : Type u_1} {Y : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] (f : C(X, Y)) : (WeakDual.CharacterSpace.homeoEval Y 𝕜).toContinuousMap.comp f = (WeakDual.CharacterSpace.compContinuousMap (ContinuousMap.compStarAlgHom' 𝕜 𝕜 f)).comp (WeakDual.CharacterSpace.homeoEval X 𝕜).toContinuousMap

Consider the contravariant functors between compact Hausdorff spaces and commutative unital C⋆algebras F : Cpct → CommCStarAlg := X ↦ C(X, ℂ) and G : CommCStarAlg → Cpct := A → characterSpace ℂ A whose actions on morphisms are given by WeakDual.CharacterSpace.compContinuousMap and ContinuousMap.compStarAlgHom', respectively.

Then η : id → G ∘ F := WeakDual.CharacterSpace.homeoEval is a natural isomorphism implementing (half of) the duality between these categories. That is, for compact Hausdorff spaces X and Y, f : C(X, Y) the following diagram commutes:

X  --- η X ---> characterSpace ℂ C(X, ℂ)

|                     |

f                  (G ∘ F) f

|                     |
V                     V

Y  --- η Y ---> characterSpace ℂ C(Y, ℂ)