Documentation

Mathlib.Analysis.CStarAlgebra.Classes

Classes of C⋆-algebras #

This file defines classes for complex C⋆-algebras. These are (unital or non-unital, commutative or noncommutative) Banach algebra over ℂ with an antimultiplicative conjugate-linear involution (star) satisfying the C⋆-identity ∥star x * x∥ = ∥x∥ ^ 2.

Notes #

These classes are not defined in Mathlib.Analysis.CStarAlgebra.Basic because they require heavier imports.

source
class NonUnitalCStarAlgebra (A : Type u_1) extends NonUnitalNormedRing , StarRing , CompleteSpace , CStarRing , NormedSpace , IsScalarTower , SMulCommClass , StarModule :
Type u_1

The class of non-unital (complex) C⋆-algebras.

    Instances
      source
      class NonUnitalCommCStarAlgebra (A : Type u_1) extends NonUnitalNormedCommRing , StarRing , CompleteSpace , CStarRing , NormedSpace , IsScalarTower , SMulCommClass , StarModule :
      Type u_1

      The class of non-unital commutative (complex) C⋆-algebras.

        Instances
          source
          class CStarAlgebra (A : Type u_1) extends NormedRing , StarRing , CompleteSpace , CStarRing , NormedAlgebra , StarModule :
          Type u_1

          The class of unital (complex) C⋆-algebras.

            Instances
              source
              class CommCStarAlgebra (A : Type u_1) extends NormedCommRing , StarRing , CompleteSpace , CStarRing , NormedAlgebra , StarModule :
              Type u_1

              The class of unital commutative (complex) C⋆-algebras.

                Instances
                  source
                  @[instance 100]
                  instance CStarAlgebra.toNonUnitalCStarAlgebra (A : Type u_1) [CStarAlgebra A] :
                  NonUnitalCStarAlgebra A
                  Equations
                  source
                  @[instance 100]
                  instance CommCStarAlgebra.toNonUnitalCommCStarAlgebra (A : Type u_1) [CommCStarAlgebra A] :
                  NonUnitalCommCStarAlgebra A
                  Equations
                  source
                  noncomputable instance StarSubalgebra.cstarAlgebra {S : Type u_1} {A : Type u_2} [CStarAlgebra A] [SetLike S A] [SubringClass S A] [SMulMemClass S ℂ A] [StarMemClass S A] (s : S) [h_closed : IsClosed ↑s] :
                  CStarAlgebra ↥s
                  Equations
                  source
                  noncomputable instance StarSubalgebra.commCStarAlgebra {S : Type u_1} {A : Type u_2} [CommCStarAlgebra A] [SetLike S A] [SubringClass S A] [SMulMemClass S ℂ A] [StarMemClass S A] (s : S) [h_closed : IsClosed ↑s] :
                  CommCStarAlgebra ↥s
                  Equations
                  source
                  noncomputable instance NonUnitalStarSubalgebra.nonUnitalCStarAlgebra {S : Type u_1} {A : Type u_2} [NonUnitalCStarAlgebra A] [SetLike S A] [NonUnitalSubringClass S A] [SMulMemClass S ℂ A] [StarMemClass S A] (s : S) [h_closed : IsClosed ↑s] :
                  NonUnitalCStarAlgebra ↥s
                  Equations
                  source
                  noncomputable instance NonUnitalStarSubalgebra.nonUnitalCommCStarAlgebra {S : Type u_1} {A : Type u_2} [NonUnitalCommCStarAlgebra A] [SetLike S A] [NonUnitalSubringClass S A] [SMulMemClass S ℂ A] [StarMemClass S A] (s : S) [h_closed : IsClosed ↑s] :
                  NonUnitalCommCStarAlgebra ↥s
                  Equations
                  source
                  noncomputable instance instCommCStarAlgebraComplex :
                  CommCStarAlgebra ℂ
                  Equations
                  source
                  instance instNonUnitalCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → NonUnitalCStarAlgebra (A i)] :
                  NonUnitalCStarAlgebra ((i : ι) → A i)
                  Equations
                  • instNonUnitalCStarAlgebraForall = NonUnitalCStarAlgebra.mk
                  source
                  instance instNonUnitalCommCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → NonUnitalCommCStarAlgebra (A i)] :
                  NonUnitalCommCStarAlgebra ((i : ι) → A i)
                  Equations
                  • instNonUnitalCommCStarAlgebraForall = NonUnitalCommCStarAlgebra.mk
                  source
                  noncomputable instance instCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → CStarAlgebra (A i)] :
                  CStarAlgebra ((i : ι) → A i)
                  Equations
                  • instCStarAlgebraForall = CStarAlgebra.mk
                  source
                  noncomputable instance instCommCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → CommCStarAlgebra (A i)] :
                  CommCStarAlgebra ((i : ι) → A i)
                  Equations
                  • instCommCStarAlgebraForall = CommCStarAlgebra.mk
                  source
                  instance instNonUnitalCStarAlgebraProd {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] :
                  NonUnitalCStarAlgebra (A × B)
                  Equations
                  • instNonUnitalCStarAlgebraProd = NonUnitalCStarAlgebra.mk
                  source
                  instance instNonUnitalCommCStarAlgebraProd {A : Type u_1} {B : Type u_2} [NonUnitalCommCStarAlgebra A] [NonUnitalCommCStarAlgebra B] :
                  NonUnitalCommCStarAlgebra (A × B)
                  Equations
                  • instNonUnitalCommCStarAlgebraProd = NonUnitalCommCStarAlgebra.mk
                  source
                  noncomputable instance instCStarAlgebraProd {A : Type u_1} {B : Type u_2} [CStarAlgebra A] [CStarAlgebra B] :
                  CStarAlgebra (A × B)
                  Equations
                  • instCStarAlgebraProd = CStarAlgebra.mk
                  source
                  noncomputable instance instCommCStarAlgebraProd {A : Type u_1} {B : Type u_2} [CommCStarAlgebra A] [CommCStarAlgebra B] :
                  CommCStarAlgebra (A × B)
                  Equations
                  • instCommCStarAlgebraProd = CommCStarAlgebra.mk