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

source
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
    Instances For
      source
      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
      source
      theorem WeakDual.CharacterSpace.exists_apply_eq_zero {A : Type u_1} [NormedCommRing A] [NormedAlgebra β„‚ A] [CompleteSpace A] {a : A} (ha : Β¬IsUnit a) :
      βˆƒ (f : ↑(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.

      source
      theorem WeakDual.CharacterSpace.mem_spectrum_iff_exists {A : Type u_1} [NormedCommRing A] [NormedAlgebra β„‚ A] [CompleteSpace A] {a : A} {z : β„‚} :
      z ∈ spectrum β„‚ a ↔ βˆƒ (f : ↑(characterSpace β„‚ A)), f a = z
      source
      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.

      source
      instance instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial {A : Type u_1} [NormedCommRing A] [NormedAlgebra β„‚ A] [CompleteSpace A] [Nontrivial A] :
      Nonempty ↑(WeakDual.characterSpace β„‚ A)
      source
      theorem gelfandTransform_map_star {A : Type u_1} [CommCStarAlgebra A] (a : A) :
      (WeakDual.gelfandTransform β„‚ A) (star a) = star ((WeakDual.gelfandTransform β„‚ A) a)
      source
      theorem gelfandTransform_isometry (A : Type u_1) [CommCStarAlgebra A] :
      Isometry ⇑(WeakDual.gelfandTransform β„‚ A)

      The Gelfand transform is an isometry when the algebra is a C⋆-algebra over β„‚.

      source
      theorem gelfandTransform_bijective (A : Type u_1) [CommCStarAlgebra A] :
      Function.Bijective ⇑(WeakDual.gelfandTransform β„‚ A)

      The Gelfand transform is bijective when the algebra is a C⋆-algebra over β„‚.

      source
      noncomputable def gelfandStarTransform (A : Type u_1) [CommCStarAlgebra 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
        Instances For
          source
          @[simp]
          theorem gelfandStarTransform_apply_apply (A : Type u_1) [CommCStarAlgebra A] (a : A) (Ο† : ↑(WeakDual.characterSpace β„‚ A)) :
          ((gelfandStarTransform A) a) Ο† = Ο† a
          source
          @[simp]
          theorem gelfandStarTransform_symm_apply (A : Type u_1) [CommCStarAlgebra A] (a✝ : C(↑(WeakDual.characterSpace β„‚ A), β„‚)) :
          (gelfandStarTransform A).symm a✝ = (↑(RingEquiv.ofBijective { toAlgHom := WeakDual.gelfandTransform β„‚ A, map_star' := β‹― } β‹―)).symm a✝
          source
          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(↑(characterSpace π•œ B), ↑(characterSpace π•œ A))

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

          Equations
            Instances For
              source
              @[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) (Ο† : ↑(characterSpace π•œ B)) :
              (compContinuousMap ψ) Ο† = equivAlgHom.symm ((equivAlgHom Ο†).comp ψ.toAlgHom)
              source
              @[simp]
              theorem WeakDual.CharacterSpace.compContinuousMap_id (A : Type u_1) {π•œ : Type u_4} [NontriviallyNormedField π•œ] [NormedRing A] [NormedAlgebra π•œ A] [CompleteSpace A] [StarRing A] :
              compContinuousMap (StarAlgHom.id π•œ A) = ContinuousMap.id ↑(characterSpace π•œ A)

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

              source
              @[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) :
              compContinuousMap (Οˆβ‚‚.comp Οˆβ‚) = (compContinuousMap Οˆβ‚).comp (compContinuousMap Οˆβ‚‚)

              WeakDual.CharacterSpace.compContinuousMap is functorial.

              source
              theorem gelfandStarTransform_naturality {A : Type u_1} {B : Type u_2} [CommCStarAlgebra A] [CommCStarAlgebra 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, β„‚)
              source
              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)) :
              (↑(homeoEval Y π•œ)).comp f = (compContinuousMap (ContinuousMap.compStarAlgHom' π•œ π•œ f)).comp ↑(homeoEval X π•œ)

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