Documentation

Mathlib.Topology.Algebra.Module.CharacterSpace

Character space of a topological algebra #

The character space of a topological algebra is the subset of elements of the weak dual that are also algebra homomorphisms. This space is used in the Gelfand transform, which gives an isomorphism between a commutative Cā‹†-algebra and continuous functions on the character space of the algebra. This, in turn, is used to construct the continuous functional calculus on Cā‹†-algebras.

Implementation notes #

We define WeakDual.characterSpace š•œ A as a subset of the weak dual, which automatically puts the correct topology on the space. We then define WeakDual.CharacterSpace.toAlgHom which provides the algebra homomorphism corresponding to any element. We also provide WeakDual.CharacterSpace.toClm which provides the element as a continuous linear map. (Even though WeakDual š•œ A is a type copy of A ā†’L[š•œ] š•œ, this is often more convenient.)

Tags #

character space, Gelfand transform, functional calculus

def WeakDual.characterSpace (š•œ : Type u_1) (A : Type u_2) [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] :
Set (WeakDual š•œ A)

The character space of a topological algebra is the subset of elements of the weak dual that are also algebra homomorphisms.

Instances For
    instance WeakDual.CharacterSpace.instContinuousLinearMapClass {š•œ : Type u_1} {A : Type u_2} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] :
    ContinuousLinearMapClass (ā†‘(WeakDual.characterSpace š•œ A)) š•œ A š•œ

    Elements of the character space are continuous linear maps.

    @[simp]
    theorem WeakDual.CharacterSpace.coe_coe {š•œ : Type u_1} {A : Type u_2} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] (Ļ† : ā†‘(WeakDual.characterSpace š•œ A)) :
    ā†‘ā†‘Ļ† = ā†‘Ļ†
    theorem WeakDual.CharacterSpace.ext {š•œ : Type u_1} {A : Type u_2} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] {Ļ† : ā†‘(WeakDual.characterSpace š•œ A)} {Ļˆ : ā†‘(WeakDual.characterSpace š•œ A)} (h : āˆ€ (x : A), ā†‘Ļ† x = ā†‘Ļˆ x) :
    Ļ† = Ļˆ
    def WeakDual.CharacterSpace.toClm {š•œ : Type u_1} {A : Type u_2} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] (Ļ† : ā†‘(WeakDual.characterSpace š•œ A)) :
    A ā†’L[š•œ] š•œ

    An element of the character space, as a continuous linear map.

    Instances For
      @[simp]
      theorem WeakDual.CharacterSpace.coe_toClm {š•œ : Type u_1} {A : Type u_2} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] (Ļ† : ā†‘(WeakDual.characterSpace š•œ A)) :
      ā†‘(WeakDual.CharacterSpace.toClm Ļ†) = ā†‘Ļ†
      instance WeakDual.CharacterSpace.instNonUnitalAlgHomClass {š•œ : Type u_1} {A : Type u_2} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] :
      NonUnitalAlgHomClass (ā†‘(WeakDual.characterSpace š•œ A)) š•œ A š•œ

      Elements of the character space are non-unital algebra homomorphisms.

      def WeakDual.CharacterSpace.toNonUnitalAlgHom {š•œ : Type u_1} {A : Type u_2} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] (Ļ† : ā†‘(WeakDual.characterSpace š•œ A)) :
      A ā†’ā‚™ā‚[š•œ] š•œ

      An element of the character space, as a non-unital algebra homomorphism.

      Instances For
        @[simp]
        theorem WeakDual.CharacterSpace.coe_toNonUnitalAlgHom {š•œ : Type u_1} {A : Type u_2} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] (Ļ† : ā†‘(WeakDual.characterSpace š•œ A)) :
        instance WeakDual.CharacterSpace.instIsEmpty {š•œ : Type u_1} {A : Type u_2} [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] [Subsingleton A] :
        IsEmpty ā†‘(WeakDual.characterSpace š•œ A)
        theorem WeakDual.CharacterSpace.union_zero (š•œ : Type u_1) (A : Type u_2) [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] :
        WeakDual.characterSpace š•œ A āˆŖ {0} = {Ļ† | āˆ€ (x y : A), ā†‘Ļ† (x * y) = ā†‘Ļ† x * ā†‘Ļ† y}
        theorem WeakDual.CharacterSpace.union_zero_isClosed (š•œ : Type u_1) (A : Type u_2) [CommSemiring š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module š•œ A] [T2Space š•œ] [ContinuousMul š•œ] :

        The characterSpace š•œ A along with 0 is always a closed set in WeakDual š•œ A.

        instance WeakDual.CharacterSpace.instAlgHomClass {š•œ : Type u_1} {A : Type u_2} [CommRing š•œ] [NoZeroDivisors š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [TopologicalSpace A] [Semiring A] [Algebra š•œ A] :
        AlgHomClass (ā†‘(WeakDual.characterSpace š•œ A)) š•œ A š•œ

        In a unital algebra, elements of the character space are algebra homomorphisms.

        @[simp]
        theorem WeakDual.CharacterSpace.toAlgHom_apply {š•œ : Type u_1} {A : Type u_2} [CommRing š•œ] [NoZeroDivisors š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [TopologicalSpace A] [Semiring A] [Algebra š•œ A] (Ļ† : ā†‘(WeakDual.characterSpace š•œ A)) :
        āˆ€ (a : A), ā†‘(WeakDual.CharacterSpace.toAlgHom Ļ†) a = MulActionHom.toFun (WeakDual.CharacterSpace.toNonUnitalAlgHom Ļ†).toDistribMulActionHom.toMulActionHom a
        def WeakDual.CharacterSpace.toAlgHom {š•œ : Type u_1} {A : Type u_2} [CommRing š•œ] [NoZeroDivisors š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [TopologicalSpace A] [Semiring A] [Algebra š•œ A] (Ļ† : ā†‘(WeakDual.characterSpace š•œ A)) :
        A ā†’ā‚[š•œ] š•œ

        An element of the character space of a unital algebra, as an algebra homomorphism.

        Instances For
          theorem WeakDual.CharacterSpace.eq_set_map_one_map_mul {š•œ : Type u_1} {A : Type u_2} [CommRing š•œ] [NoZeroDivisors š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [TopologicalSpace A] [Semiring A] [Algebra š•œ A] [Nontrivial š•œ] :
          WeakDual.characterSpace š•œ A = {Ļ† | ā†‘Ļ† 1 = 1 āˆ§ āˆ€ (x y : A), ā†‘Ļ† (x * y) = ā†‘Ļ† x * ā†‘Ļ† y}
          theorem WeakDual.CharacterSpace.isClosed {š•œ : Type u_1} {A : Type u_2} [CommRing š•œ] [NoZeroDivisors š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [TopologicalSpace A] [Semiring A] [Algebra š•œ A] [Nontrivial š•œ] [T2Space š•œ] [ContinuousMul š•œ] :

          under suitable mild assumptions on š•œ, the character space is a closed set in WeakDual š•œ A.

          theorem WeakDual.CharacterSpace.apply_mem_spectrum {š•œ : Type u_1} {A : Type u_2} [CommRing š•œ] [NoZeroDivisors š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [TopologicalSpace A] [Ring A] [Algebra š•œ A] [Nontrivial š•œ] (Ļ† : ā†‘(WeakDual.characterSpace š•œ A)) (a : A) :
          ā†‘Ļ† a āˆˆ spectrum š•œ a
          theorem WeakDual.CharacterSpace.ext_ker {š•œ : Type u_1} {A : Type u_2} [CommRing š•œ] [NoZeroDivisors š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [TopologicalSpace A] [Ring A] [Algebra š•œ A] {Ļ† : ā†‘(WeakDual.characterSpace š•œ A)} {Ļˆ : ā†‘(WeakDual.characterSpace š•œ A)} (h : RingHom.ker Ļ† = RingHom.ker Ļˆ) :
          Ļ† = Ļˆ
          instance WeakDual.ker_isMaximal {š•œ : Type u_1} {A : Type u_2} [Field š•œ] [TopologicalSpace š•œ] [ContinuousAdd š•œ] [ContinuousConstSMul š•œ š•œ] [Ring A] [TopologicalSpace A] [Algebra š•œ A] (Ļ† : ā†‘(WeakDual.characterSpace š•œ A)) :

          The RingHom.ker of Ļ† : characterSpace š•œ A is maximal.

          @[simp]
          theorem WeakDual.gelfandTransform_apply_apply (š•œ : Type u_1) (A : Type u_2) [CommRing š•œ] [NoZeroDivisors š•œ] [TopologicalSpace š•œ] [TopologicalRing š•œ] [TopologicalSpace A] [Semiring A] [Algebra š•œ A] (a : A) (Ļ† : ā†‘(WeakDual.characterSpace š•œ A)) :
          ā†‘(ā†‘(WeakDual.gelfandTransform š•œ A) a) Ļ† = ā†‘Ļ† a
          def WeakDual.gelfandTransform (š•œ : Type u_1) (A : Type u_2) [CommRing š•œ] [NoZeroDivisors š•œ] [TopologicalSpace š•œ] [TopologicalRing š•œ] [TopologicalSpace A] [Semiring A] [Algebra š•œ A] :
          A ā†’ā‚[š•œ] C(ā†‘(WeakDual.characterSpace š•œ A), š•œ)

          The Gelfand transform is an algebra homomorphism (over š•œ) from a topological š•œ-algebra A into the š•œ-algebra of continuous š•œ-valued functions on the characterSpace š•œ A. The character space itself consists of all algebra homomorphisms from A to š•œ.

          Instances For