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 , Norm , NonUnitalRing , MetricSpace , NonUnitalNonAssocRing , NonUnitalSemiring , AddCommGroup , NonUnitalNonAssocSemiring , AddGroup , SemigroupWithZero , AddCommMonoid , SubNegMonoid , Distrib , Semigroup , MulZeroClass , AddMonoid , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Mul , Zero , AddCommMagma , Add , PseudoMetricSpace , Dist , StarMul , InvolutiveStar , Star , Module , DistribMulAction , MulAction , SMul :
Type u_1

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

    Instances
      source
      class NonUnitalCommCStarAlgebra (A : Type u_1) extends NonUnitalNormedCommRing , NonUnitalCStarAlgebra , NonUnitalNormedRing , StarRing , CompleteSpace , CStarRing , NormedSpace , IsScalarTower , SMulCommClass , StarModule , Norm , NonUnitalRing , MetricSpace , NonUnitalNonAssocRing , NonUnitalSemiring , AddCommGroup , NonUnitalNonAssocSemiring , AddGroup , SemigroupWithZero , AddCommMonoid , SubNegMonoid , Distrib , Semigroup , MulZeroClass , AddMonoid , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Mul , Zero , AddCommMagma , Add , PseudoMetricSpace , Dist , StarMul , InvolutiveStar , Star , Module , DistribMulAction , MulAction , SMul :
      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 , Norm , Ring , MetricSpace , Semiring , AddCommGroup , AddGroupWithOne , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , MulOneClass , IntCast , AddMonoidWithOne , AddGroup , AddCommMonoid , Distrib , Semigroup , MulZeroClass , NatCast , SubNegMonoid , AddMonoid , One , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Mul , Zero , AddCommMagma , Add , PseudoMetricSpace , Dist , StarMul , InvolutiveStar , Star , Algebra , SMul , RingHom , MonoidHom , OneHom , AddMonoidHom , NonUnitalRingHom , MonoidWithZeroHom , MulHom , ZeroHom , AddHom :
          Type u_1

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

            Instances
              source
              class CommCStarAlgebra (A : Type u_1) extends NormedCommRing , CStarAlgebra , NormedRing , StarRing , CompleteSpace , CStarRing , NormedAlgebra , StarModule , Norm , Ring , MetricSpace , Semiring , AddCommGroup , AddGroupWithOne , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , MulOneClass , IntCast , AddMonoidWithOne , AddGroup , AddCommMonoid , Distrib , Semigroup , MulZeroClass , NatCast , SubNegMonoid , AddMonoid , One , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Mul , Zero , AddCommMagma , Add , PseudoMetricSpace , Dist , StarMul , InvolutiveStar , Star , Algebra , SMul , RingHom , MonoidHom , OneHom , AddMonoidHom , NonUnitalRingHom , MonoidWithZeroHom , MulHom , ZeroHom , AddHom :
              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