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.
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
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
class
CStarAlgebra
(A : Type u_1)
extends
NormedRing
,
StarRing
,
CompleteSpace
,
CStarRing
,
NormedAlgebra
,
StarModule
:
Type u_1
The class of unital (complex) C⋆-algebras.
Instances
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
@[instance 100]
Equations
- CStarAlgebra.toNonUnitalCStarAlgebra A = NonUnitalCStarAlgebra.mk
@[instance 100]
Equations
- CommCStarAlgebra.toNonUnitalCommCStarAlgebra A = NonUnitalCommCStarAlgebra.mk
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
- StarSubalgebra.cstarAlgebra s = CStarAlgebra.mk
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]
:
Equations
- StarSubalgebra.commCStarAlgebra s = CommCStarAlgebra.mk
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]
:
Equations
- NonUnitalStarSubalgebra.nonUnitalCStarAlgebra s = NonUnitalCStarAlgebra.mk
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]
:
Equations
- NonUnitalStarSubalgebra.nonUnitalCommCStarAlgebra s = NonUnitalCommCStarAlgebra.mk
Equations
- instCommCStarAlgebraComplex = CommCStarAlgebra.mk
instance
instNonUnitalCStarAlgebraForall
{ι : Type u_1}
{A : ι → Type u_2}
[Fintype ι]
[(i : ι) → NonUnitalCStarAlgebra (A i)]
:
NonUnitalCStarAlgebra ((i : ι) → A i)
Equations
- instNonUnitalCStarAlgebraForall = NonUnitalCStarAlgebra.mk
instance
instNonUnitalCommCStarAlgebraForall
{ι : Type u_1}
{A : ι → Type u_2}
[Fintype ι]
[(i : ι) → NonUnitalCommCStarAlgebra (A i)]
:
NonUnitalCommCStarAlgebra ((i : ι) → A i)
Equations
- instNonUnitalCommCStarAlgebraForall = NonUnitalCommCStarAlgebra.mk
noncomputable instance
instCStarAlgebraForall
{ι : Type u_1}
{A : ι → Type u_2}
[Fintype ι]
[(i : ι) → CStarAlgebra (A i)]
:
CStarAlgebra ((i : ι) → A i)
Equations
- instCStarAlgebraForall = CStarAlgebra.mk
noncomputable instance
instCommCStarAlgebraForall
{ι : Type u_1}
{A : ι → Type u_2}
[Fintype ι]
[(i : ι) → CommCStarAlgebra (A i)]
:
CommCStarAlgebra ((i : ι) → A i)
Equations
- instCommCStarAlgebraForall = CommCStarAlgebra.mk
instance
instNonUnitalCStarAlgebraProd
{A : Type u_1}
{B : Type u_2}
[NonUnitalCStarAlgebra A]
[NonUnitalCStarAlgebra B]
:
NonUnitalCStarAlgebra (A × B)
Equations
- instNonUnitalCStarAlgebraProd = NonUnitalCStarAlgebra.mk
instance
instNonUnitalCommCStarAlgebraProd
{A : Type u_1}
{B : Type u_2}
[NonUnitalCommCStarAlgebra A]
[NonUnitalCommCStarAlgebra B]
:
NonUnitalCommCStarAlgebra (A × B)
Equations
- instNonUnitalCommCStarAlgebraProd = NonUnitalCommCStarAlgebra.mk
noncomputable instance
instCStarAlgebraProd
{A : Type u_1}
{B : Type u_2}
[CStarAlgebra A]
[CStarAlgebra B]
:
CStarAlgebra (A × B)
Equations
- instCStarAlgebraProd = CStarAlgebra.mk
noncomputable instance
instCommCStarAlgebraProd
{A : Type u_1}
{B : Type u_2}
[CommCStarAlgebra A]
[CommCStarAlgebra B]
:
CommCStarAlgebra (A × B)
Equations
- instCommCStarAlgebraProd = CommCStarAlgebra.mk