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.lean because they require heavier imports.

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

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

• norm : A → ℝ
• add : A → A → A
• add_assoc (a b c : A) : a + b + c = a + (b + c)
• zero : A
• zero_add (a : A) : 0 + a = a
• add_zero (a : A) : a + 0 = a
• nsmul : ℕ → A → A
• nsmul_zero (x : A) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : A) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : A → A
• sub : A → A → A
• sub_eq_add_neg (a b : A) : a - b = a + -b
• zsmul : ℤ → A → A
• zsmul_zero' (a : A) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : A) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : A) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : A) : -a + a = 0
• add_comm (a b : A) : a + b = b + a
• mul : A → A → A
• left_distrib (a b c : A) : a * (b + c) = a * b + a * c
• right_distrib (a b c : A) : (a + b) * c = a * c + b * c
• zero_mul (a : A) : 0 * a = 0
• mul_zero (a : A) : a * 0 = 0
• mul_assoc (a b c : A) : a * b * c = a * (b * c)
• dist : A → A → ℝ
• dist_self (x : A) : dist x x = 0
• dist_comm (x y : A) : dist x y = dist y x
• dist_triangle (x y z : A) : dist x z ≤ dist x y + dist y z
• edist : A → A → ENNReal
• edist_dist (x y : A) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace A
• uniformity_dist : uniformity A = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : A × A | dist p.1 p.2 < ε}
• toBornology : Bornology A
• cobounded_sets : (Bornology.cobounded A).sets = {s : Set A | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : A} : dist x y = 0 → x = y
• dist_eq (x y : A) : dist x y = ‖x - y‖
• norm_mul_le (a b : A) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• star : A → A
• star_involutive : Function.Involutive star
• star_mul (r s : A) : star (r * s) = star s * star r
• star_add (r s : A) : star (r + s) = star r + star s
• complete {f : Filter A} : Cauchy f → ∃ (x : A), f ≤ nhds x
• norm_mul_self_le (x : A) : ‖x‖ * ‖x‖ ≤ ‖star x * x‖
• smul : ℂ → A → A
• mul_smul (x y : ℂ) (b : A) : (x * y) • b = x • y • b
• one_smul (b : A) : 1 • b = b
• smul_zero (a : ℂ) : a • 0 = 0
• smul_add (a : ℂ) (x y : A) : a • (x + y) = a • x + a • y
• add_smul (r s : ℂ) (x : A) : (r + s) • x = r • x + s • x
• zero_smul (x : A) : 0 • x = 0
• norm_smul_le (a : ℂ) (b : A) : ‖a • b‖ ≤ ‖a‖ * ‖b‖
• smul_assoc (x : ℂ) (y z : A) : (x • y) • z = x • y • z
• smul_comm (m : ℂ) (n a : A) : m • n • a = n • m • a
• star_smul (r : ℂ) (a : A) : star (r • a) = star r • star a

class NonUnitalCommCStarAlgebra (A : Type u_1) extends NonUnitalNormedCommRing A, NonUnitalCStarAlgebra A : Type u_1

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

• norm : A → ℝ
• add : A → A → A
• add_assoc (a b c : A) : a + b + c = a + (b + c)
• zero : A
• zero_add (a : A) : 0 + a = a
• add_zero (a : A) : a + 0 = a
• nsmul : ℕ → A → A
• nsmul_zero (x : A) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : A) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : A → A
• sub : A → A → A
• sub_eq_add_neg (a b : A) : a - b = a + -b
• zsmul : ℤ → A → A
• zsmul_zero' (a : A) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : A) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : A) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : A) : -a + a = 0
• add_comm (a b : A) : a + b = b + a
• mul : A → A → A
• left_distrib (a b c : A) : a * (b + c) = a * b + a * c
• right_distrib (a b c : A) : (a + b) * c = a * c + b * c
• zero_mul (a : A) : 0 * a = 0
• mul_zero (a : A) : a * 0 = 0
• mul_assoc (a b c : A) : a * b * c = a * (b * c)
• dist : A → A → ℝ
• dist_self (x : A) : dist x x = 0
• dist_comm (x y : A) : dist x y = dist y x
• dist_triangle (x y z : A) : dist x z ≤ dist x y + dist y z
• edist : A → A → ENNReal
• edist_dist (x y : A) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace A
• uniformity_dist : uniformity A = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : A × A | dist p.1 p.2 < ε}
• toBornology : Bornology A
• cobounded_sets : (Bornology.cobounded A).sets = {s : Set A | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : A} : dist x y = 0 → x = y
• dist_eq (x y : A) : dist x y = ‖x - y‖
• norm_mul_le (a b : A) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm (a b : A) : a * b = b * a
• star : A → A
• star_involutive : Function.Involutive star
• star_mul (r s : A) : star (r * s) = star s * star r
• star_add (r s : A) : star (r + s) = star r + star s
• complete {f : Filter A} : Cauchy f → ∃ (x : A), f ≤ nhds x
• norm_mul_self_le (x : A) : ‖x‖ * ‖x‖ ≤ ‖star x * x‖
• smul : ℂ → A → A
• mul_smul (x y : ℂ) (b : A) : (x * y) • b = x • y • b
• one_smul (b : A) : 1 • b = b
• smul_zero (a : ℂ) : a • 0 = 0
• smul_add (a : ℂ) (x y : A) : a • (x + y) = a • x + a • y
• add_smul (r s : ℂ) (x : A) : (r + s) • x = r • x + s • x
• zero_smul (x : A) : 0 • x = 0
• norm_smul_le (a : ℂ) (b : A) : ‖a • b‖ ≤ ‖a‖ * ‖b‖
• smul_assoc (x : ℂ) (y z : A) : (x • y) • z = x • y • z
• smul_comm (m : ℂ) (n a : A) : m • n • a = n • m • a
• star_smul (r : ℂ) (a : A) : star (r • a) = star r • star a

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

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

• norm : A → ℝ
• add : A → A → A
• add_assoc (a b c : A) : a + b + c = a + (b + c)
• zero : A
• zero_add (a : A) : 0 + a = a
• add_zero (a : A) : a + 0 = a
• nsmul : ℕ → A → A
• nsmul_zero (x : A) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : A) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : A) : a + b = b + a
• mul : A → A → A
• left_distrib (a b c : A) : a * (b + c) = a * b + a * c
• right_distrib (a b c : A) : (a + b) * c = a * c + b * c
• zero_mul (a : A) : 0 * a = 0
• mul_zero (a : A) : a * 0 = 0
• mul_assoc (a b c : A) : a * b * c = a * (b * c)
• one : A
• one_mul (a : A) : 1 * a = a
• mul_one (a : A) : a * 1 = a
• natCast : ℕ → A
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → A → A
• npow_zero (x : A) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : A) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : A → A
• sub : A → A → A
• sub_eq_add_neg (a b : A) : a - b = a + -b
• zsmul : ℤ → A → A
• zsmul_zero' (a : A) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : A) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : A) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : A) : -a + a = 0
• intCast : ℤ → A
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• dist : A → A → ℝ
• dist_self (x : A) : dist x x = 0
• dist_comm (x y : A) : dist x y = dist y x
• dist_triangle (x y z : A) : dist x z ≤ dist x y + dist y z
• edist : A → A → ENNReal
• edist_dist (x y : A) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace A
• uniformity_dist : uniformity A = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : A × A | dist p.1 p.2 < ε}
• toBornology : Bornology A
• cobounded_sets : (Bornology.cobounded A).sets = {s : Set A | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : A} : dist x y = 0 → x = y
• dist_eq (x y : A) : dist x y = ‖x - y‖
• norm_mul_le (a b : A) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• star : A → A
• star_involutive : Function.Involutive star
• star_mul (r s : A) : star (r * s) = star s * star r
• star_add (r s : A) : star (r + s) = star r + star s
• complete {f : Filter A} : Cauchy f → ∃ (x : A), f ≤ nhds x
• norm_mul_self_le (x : A) : ‖x‖ * ‖x‖ ≤ ‖star x * x‖
• smul : ℂ → A → A
• algebraMap : ℂ →+* A
• commutes' (r : ℂ) (x : A) : Algebra.algebraMap r * x = x * Algebra.algebraMap r
• smul_def' (r : ℂ) (x : A) : r • x = Algebra.algebraMap r * x
• norm_smul_le (r : ℂ) (x : A) : ‖r • x‖ ≤ ‖r‖ * ‖x‖
• star_smul (r : ℂ) (a : A) : star (r • a) = star r • star a

class CommCStarAlgebra (A : Type u_1) extends NormedCommRing A, CStarAlgebra A : Type u_1

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

• norm : A → ℝ
• add : A → A → A
• add_assoc (a b c : A) : a + b + c = a + (b + c)
• zero : A
• zero_add (a : A) : 0 + a = a
• add_zero (a : A) : a + 0 = a
• nsmul : ℕ → A → A
• nsmul_zero (x : A) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : A) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : A) : a + b = b + a
• mul : A → A → A
• left_distrib (a b c : A) : a * (b + c) = a * b + a * c
• right_distrib (a b c : A) : (a + b) * c = a * c + b * c
• zero_mul (a : A) : 0 * a = 0
• mul_zero (a : A) : a * 0 = 0
• mul_assoc (a b c : A) : a * b * c = a * (b * c)
• one : A
• one_mul (a : A) : 1 * a = a
• mul_one (a : A) : a * 1 = a
• natCast : ℕ → A
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → A → A
• npow_zero (x : A) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : A) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : A → A
• sub : A → A → A
• sub_eq_add_neg (a b : A) : a - b = a + -b
• zsmul : ℤ → A → A
• zsmul_zero' (a : A) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : A) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : A) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : A) : -a + a = 0
• intCast : ℤ → A
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• dist : A → A → ℝ
• dist_self (x : A) : dist x x = 0
• dist_comm (x y : A) : dist x y = dist y x
• dist_triangle (x y z : A) : dist x z ≤ dist x y + dist y z
• edist : A → A → ENNReal
• edist_dist (x y : A) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace A
• uniformity_dist : uniformity A = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : A × A | dist p.1 p.2 < ε}
• toBornology : Bornology A
• cobounded_sets : (Bornology.cobounded A).sets = {s : Set A | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : A} : dist x y = 0 → x = y
• dist_eq (x y : A) : dist x y = ‖x - y‖
• norm_mul_le (a b : A) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm (a b : A) : a * b = b * a
• star : A → A
• star_involutive : Function.Involutive star
• star_mul (r s : A) : star (r * s) = star s * star r
• star_add (r s : A) : star (r + s) = star r + star s
• complete {f : Filter A} : Cauchy f → ∃ (x : A), f ≤ nhds x
• norm_mul_self_le (x : A) : ‖x‖ * ‖x‖ ≤ ‖star x * x‖
• smul : ℂ → A → A
• algebraMap : ℂ →+* A
• commutes' (r : ℂ) (x : A) : Algebra.algebraMap r * x = x * Algebra.algebraMap r
• smul_def' (r : ℂ) (x : A) : r • x = Algebra.algebraMap r * x
• norm_smul_le (r : ℂ) (x : A) : ‖r • x‖ ≤ ‖r‖ * ‖x‖
• star_smul (r : ℂ) (a : A) : star (r • a) = star r • star a

@[instance 100]

instance CStarAlgebra.toNonUnitalCStarAlgebra (A : Type u_1) [CStarAlgebra A] : NonUnitalCStarAlgebra A

@[instance 100]

instance CommCStarAlgebra.toNonUnitalCommCStarAlgebra (A : Type u_1) [CommCStarAlgebra A] : NonUnitalCommCStarAlgebra A

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

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

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

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

noncomputable instance instCommCStarAlgebraComplex : CommCStarAlgebra ℂ

noncomputable instance instCStarAlgebraSubtypeMemStarSubalgebraComplexElemental {A : Type u_1} [CStarAlgebra A] (x : A) : CStarAlgebra ↥(StarAlgebra.elemental ℂ x)

noncomputable instance instNonUnitalCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElemental {A : Type u_1} [NonUnitalCStarAlgebra A] (x : A) : NonUnitalCStarAlgebra ↥(NonUnitalStarAlgebra.elemental ℂ x)

noncomputable instance instCommCStarAlgebraSubtypeMemStarSubalgebraComplexElementalOfIsStarNormal {A : Type u_1} [CStarAlgebra A] (x : A) [IsStarNormal x] : CommCStarAlgebra ↥(StarAlgebra.elemental ℂ x)

noncomputable instance instNonUnitalCommCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElementalOfIsStarNormal {A : Type u_1} [NonUnitalCStarAlgebra A] (x : A) [IsStarNormal x] : NonUnitalCommCStarAlgebra ↥(NonUnitalStarAlgebra.elemental ℂ x)

instance instNonUnitalCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → NonUnitalCStarAlgebra (A i)] : NonUnitalCStarAlgebra ((i : ι) → A i)

instance instNonUnitalCommCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → NonUnitalCommCStarAlgebra (A i)] : NonUnitalCommCStarAlgebra ((i : ι) → A i)

instance instCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → CStarAlgebra (A i)] : CStarAlgebra ((i : ι) → A i)

instance instCommCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → CommCStarAlgebra (A i)] : CommCStarAlgebra ((i : ι) → A i)

instance instNonUnitalCStarAlgebraProd {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] : NonUnitalCStarAlgebra (A × B)

instance instNonUnitalCommCStarAlgebraProd {A : Type u_1} {B : Type u_2} [NonUnitalCommCStarAlgebra A] [NonUnitalCommCStarAlgebra B] : NonUnitalCommCStarAlgebra (A × B)

instance instCStarAlgebraProd {A : Type u_1} {B : Type u_2} [CStarAlgebra A] [CStarAlgebra B] : CStarAlgebra (A × B)

instance instCommCStarAlgebraProd {A : Type u_1} {B : Type u_2} [CommCStarAlgebra A] [CommCStarAlgebra B] : CommCStarAlgebra (A × B)

instance MulOpposite.instNonUnitalCStarAlgebra {A : Type u_1} [NonUnitalCStarAlgebra A] : NonUnitalCStarAlgebra Aᵐᵒᵖ

instance MulOpposite.instNonUnitalCommCStarAlgebra {A : Type u_1} [NonUnitalCommCStarAlgebra A] : NonUnitalCommCStarAlgebra Aᵐᵒᵖ

instance MulOpposite.instCStarAlgebra {A : Type u_1} [CStarAlgebra A] : CStarAlgebra Aᵐᵒᵖ

instance MulOpposite.instCommCStarAlgebra {A : Type u_1} [CommCStarAlgebra A] : CommCStarAlgebra Aᵐᵒᵖ