Gelfand Duality

The gelfandTransform 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.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.

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 ℂ.

TODO

• After StarAlgEquiv is defined, realize gelfandTransform as a StarAlgEquiv.
• Prove that if A is the unital C⋆-algebra over ℂ generated by a fixed normal element x in a larger C⋆-algebra B, then characterSpace ℂ 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 characterSpace ℂ C(X, ℂ).
• Conclude using the previous fact that the functors C(·, ℂ) and characterSpace ℂ · 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 homomorphisms); this is known as Gelfand duality.

Tags

Gelfand transform, character space, C⋆-algebra

noncomputable def Ideal.toCharacterSpace {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (I : Ideal A) [Ideal.IsMaximal I] : ↑(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.

theorem Ideal.toCharacterSpace_apply_eq_zero_of_mem {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (I : Ideal A) [Ideal.IsMaximal I] {a : A} (ha : a ∈ I) : ↑(Ideal.toCharacterSpace I) 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, ↑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, ↑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 instNonemptyElemWeakDualComplexInstCommSemiringComplexToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplexToContinuousAddToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToTopologicalSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingComplexToTopologicalRingToDivisionRingToNormedDivisionRingTo_topologicalDivisionRingTo_continuousConstSMulToSMulIdUniformContinuousConstSMulTo_uniformAddGroupToSeminormedAddCommGroupToNonUnitalSeminormedRingToNonUnitalNormedRingToNormedRingToContinuousMulToNonUnitalNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToNormedRingToModuleToSeminormedAddCommGroupToNonUnitalSeminormedRingToNonUnitalNormedRingToNormedSpace'ToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingCharacterSpace {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] : Nonempty ↑(WeakDual.characterSpace ℂ A)

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), ℂ)), ↑(StarAlgEquiv.symm (gelfandStarTransform A)) a = ↑(↑(RingEquiv.ofBijective { toAlgHom := { toRingHom := ↑(WeakDual.gelfandTransform ℂ A), commutes' := (_ : ∀ (r : ℂ), OneHom.toFun (↑↑↑(WeakDual.gelfandTransform ℂ A)) (↑(algebraMap ℂ A) r) = ↑(algebraMap ℂ C(↑(WeakDual.characterSpace ℂ A), ℂ)) r) }, map_star' := (_ : ∀ (x : A), ↑(WeakDual.gelfandTransform ℂ A) (star x) = star (↑(WeakDual.gelfandTransform ℂ A) x)) } (_ : Function.Bijective ↑(WeakDual.gelfandTransform ℂ A)))).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.

@[simp]

theorem WeakDual.CharacterSpace.compContinuousMap_apply {A : Type u_1} {B : Type u_2} [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 (AlgHom.comp (↑WeakDual.CharacterSpace.equivAlgHom φ) ψ.toAlgHom)

noncomputable def WeakDual.CharacterSpace.compContinuousMap {A : Type u_1} {B : Type u_2} [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 ψ.

@[simp]

theorem WeakDual.CharacterSpace.compContinuousMap_id (A : Type u_1) [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} [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 (StarAlgHom.comp ψ₂ ψ₁) = ContinuousMap.comp (WeakDual.CharacterSpace.compContinuousMap ψ₁) (WeakDual.CharacterSpace.compContinuousMap ψ₂)

WeakDual.CharacterSpace.compContinuousMap is functorial.