Documentation

Mathlib.Analysis.CStarAlgebra.GelfandDuality

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 #

Main statements #

TODO #

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] :

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
Instances For
    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

    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.

    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 β„‚.

    @[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

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

    Equations
    Instances For
      @[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.
      Instances For
        @[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 is functorial.

        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, β„‚)