WStarAlgebras have Unique Preduals

2. WStarAlgebras and their Topologies🔗

2.1. Basic Definitions and Results🔗

In this section we collect basic definitions and results about C^*-algebras and W^*-algebras.

An associative algebra \mathcal{A} over the complex numbers is called a normed algebra if there is a map assigning to every x \in \mathcal{A} a real number \|x\|, and this map satisfies:

  1. \|x\| \ge 0 and \|x\| = 0 \iff x = 0;

  2. \|x + y\| \le \|x\| + \|y\|;

  3. \|\lambda x\| = |\lambda| \|x\|;

  4. \|xy\| \le \|x\| \|y\|.

If \mathcal{A} is also complete with respect to the norm, it is called a Banach algebra. A mapping {}^* : \mathcal{A} \to \mathcal{A} is called an involution if it satisfies:

  1. (x^*)^* = x;

  2. (x + y)^* = x^* + y^*;

  3. (xy)^* = y^* x^*;

  4. (\lambda x)^* = \overline{\lambda} x^*,

where \lambda above is a complex number.

Definition2.1.1
uses 0
Used by 6
Reverse dependency previews
Preview
Lemma 2.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsmathlib

A Banach algebra \mathcal{A} with an involution is a C^*-algebra if the relation \|x^* x\| = \|x\|^2 holds for every x \in \mathcal{A}. A C^*-algebra is unital if it has a multiplicative identity.

Lean code for Definition2.1.1●2 definitions
  • class(extends 53, 61 methods)defined in Mathlib/Analysis/CStarAlgebra/Classes.lean
    complete
    class CStarAlgebra.{u_1} (A : Type u_1) : Type u_1
    class CStarAlgebra.{u_1} (A : Type u_1) :
  Type u_1
    The class of unital (complex) C⋆-algebras.

    Extends

    • NormedRing A
    • StarRing A
    • CompleteSpace A
    • CStarRing A
    • NormedAlgebra ℂ A
    • StarModule ℂ A

    Methods

    norm : A → ℝ
    Inherited from
    1. NormedRing
    2. Norm
    zero : A
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. AddCommMonoid
    5. AddMonoid
    6. Zero
    add : A → A → A
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. AddCommMonoid
    5. AddMonoid
    6. Add
    add_assoc : ∀ (a b c : A), a + b + c = a + (b + c)
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. AddCommMonoid
    5. AddMonoid
    zero_add : ∀ (a : A), 0 + a = a
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. AddCommMonoid
    5. AddMonoid
    add_zero : ∀ (a : A), a + 0 = a
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. AddCommMonoid
    5. AddMonoid
    nsmul : ℕ → A → A
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. AddCommMonoid
    5. AddMonoid
    6. NSMul
    nsmul_zero : ∀ (x : A), 0 • x = 0
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. AddCommMonoid
    5. AddMonoid
    nsmul_succ : ∀ (n : ℕ) (x : A), (n + 1) • x = n • x + x
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. AddCommMonoid
    5. AddMonoid
    add_comm : ∀ (a b : A), a + b = b + a
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. AddCommMonoid
    one : A
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. Monoid
    5. One
    mul : A → A → A
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. Monoid
    5. Mul
    mul_assoc : ∀ (a b c : A), a * b * c = a * (b * c)
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. Monoid
    one_mul : ∀ (a : A), 1 * a = a
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. Monoid
    mul_one : ∀ (a : A), a * 1 = a
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. Monoid
    npow : ℕ → A → A
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. Monoid
    5. NPow
    npow_zero : ∀ (x : A), x ^ 0 = 1
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. Monoid
    npow_succ : ∀ (n : ℕ) (x : A), x ^ (n + 1) = x ^ n * x
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. Monoid
    zero_mul : ∀ (a : A), 0 * a = 0
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    mul_zero : ∀ (a : A), a * 0 = 0
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    left_distrib : ∀ (a b c : A), a * (b + c) = a * b + a * c
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    right_distrib : ∀ (a b c : A), (a + b) * c = a * c + b * c
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    natCast : ℕ → A
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    4. NatCast
    natCast_zero : ↑0 = 0
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    natCast_succ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
    Inherited from
    1. NormedRing
    2. Ring
    3. Semiring
    neg : A → A
    Inherited from
    1. NormedRing
    2. Ring
    3. Neg
    sub : A → A → A
    Inherited from
    1. NormedRing
    2. Ring
    3. Sub
    zsmul : ℤ → A → A
    Inherited from
    1. NormedRing
    2. Ring
    3. ZSMul
    sub_eq_add_neg : ∀ (a b : A), a - b = a + -b
    Inherited from
    1. NormedRing
    2. Ring
    zsmul_zero' : ∀ (a : A), 0 • a = 0
    Inherited from
    1. NormedRing
    2. Ring
    zsmul_succ' : ∀ (n : ℕ) (a : A), ↑n.succ • a = ↑n • a + a
    Inherited from
    1. NormedRing
    2. Ring
    zsmul_neg' : ∀ (n : ℕ) (a : A), Int.negSucc n • a = -(↑n.succ • a)
    Inherited from
    1. NormedRing
    2. Ring
    neg_add_cancel : ∀ (a : A), -a + a = 0
    Inherited from
    1. NormedRing
    2. Ring
    intCast : ℤ → A
    Inherited from
    1. NormedRing
    2. Ring
    3. IntCast
    intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
    Inherited from
    1. NormedRing
    2. Ring
    intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
    Inherited from
    1. NormedRing
    2. Ring
    dist : A → A → ℝ
    Inherited from
    1. NormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    4. Dist
    dist_self : ∀ (x : A), dist x x = 0
    Inherited from
    1. NormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    dist_comm : ∀ (x y : A), dist x y = dist y x
    Inherited from
    1. NormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    dist_triangle : ∀ (x y z : A), dist x z ≤ dist x y + dist y z
    Inherited from
    1. NormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    edist : A → A → ENNReal
    Inherited from
    1. NormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    edist_dist : ∀ (x y : A), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
    Inherited from
    1. NormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    toUniformSpace : UniformSpace A
    Inherited from
    1. NormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    uniformity_dist : uniformity A = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε}
    Inherited from
    1. NormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    toBornology : Bornology A
    Inherited from
    1. NormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    cobounded_sets : (Bornology.cobounded A).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
    Inherited from
    1. NormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    eq_of_dist_eq_zero : ∀ {x y : A}, dist x y = 0 → x = y
    Inherited from
    1. NormedRing
    2. MetricSpace
    dist_eq : ∀ (x y : A), dist x y = ‖-x + y‖
    Inherited from
    1. NormedRing
    norm_mul_le : ∀ (a b : A), ‖a * b‖ ≤ ‖a‖ * ‖b‖
    Inherited from
    1. NormedRing
    star : A → A
    Inherited from
    1. StarRing
    2. StarMul
    3. InvolutiveStar
    4. Star
    star_involutive : Function.Involutive star
    Inherited from
    1. StarRing
    2. StarMul
    3. InvolutiveStar
    star_mul : ∀ (r s : A), star (r * s) = star s * star r
    Inherited from
    1. StarRing
    2. StarMul
    star_add : ∀ (r s : A), star (r + s) = star r + star s
    Inherited from
    1. StarRing
    complete : ∀ {f : Filter A}, Cauchy f → ∃ x, f ≤ nhds x
    Inherited from
    1. CompleteSpace
    norm_mul_self_le : ∀ (x : A), ‖x‖ * ‖x‖ ≤ ‖star x * x‖
    Inherited from
    1. CStarRing
    smul : ℂ → A → A
    Inherited from
    1. NormedAlgebra
    2. Algebra
    3. SMul
    algebraMap : ℂ →+* A
    Inherited from
    1. NormedAlgebra
    2. Algebra
    commutes' : ∀ (r : ℂ) (x : A), (algebraMap ℂ A) r * x = x * (algebraMap ℂ A) r
    Inherited from
    1. NormedAlgebra
    2. Algebra
    smul_def' : ∀ (r : ℂ) (x : A), r • x = (algebraMap ℂ A) r * x
    Inherited from
    1. NormedAlgebra
    2. Algebra
    norm_smul_le : ∀ (r : ℂ) (x : A), ‖r • x‖ ≤ ‖r‖ * ‖x‖
    Inherited from
    1. NormedAlgebra
    star_smul : ∀ (r : ℂ) (a : A), star (r • a) = star r • star a
    Inherited from
    1. StarModule
  • class(extends 45, 54 methods)defined in Mathlib/Analysis/CStarAlgebra/Classes.lean
    complete
    class NonUnitalCStarAlgebra.{u_1} (A : Type u_1) : Type u_1
    class NonUnitalCStarAlgebra.{u_1}
  (A : Type u_1) : Type u_1
    The class of non-unital (complex) C⋆-algebras.

    Extends

    • NonUnitalNormedRing A
    • StarRing A
    • CompleteSpace A
    • CStarRing A
    • NormedSpace ℂ A
    • IsScalarTower ℂ A A
    • SMulCommClass ℂ A A
    • StarModule ℂ A

    Methods

    norm : A → ℝ
    Inherited from
    1. NonUnitalNormedRing
    2. Norm
    zero : A
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    7. AddMonoid
    8. Zero
    add : A → A → A
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    7. AddMonoid
    8. Add
    add_assoc : ∀ (a b c : A), a + b + c = a + (b + c)
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    7. AddMonoid
    zero_add : ∀ (a : A), 0 + a = a
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    7. AddMonoid
    add_zero : ∀ (a : A), a + 0 = a
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    7. AddMonoid
    nsmul : ℕ → A → A
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    7. AddMonoid
    8. NSMul
    nsmul_zero : ∀ (x : A), 0 • x = 0
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    7. AddMonoid
    nsmul_succ : ∀ (n : ℕ) (x : A), (n + 1) • x = n • x + x
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    7. AddMonoid
    neg : A → A
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    7. Neg
    sub : A → A → A
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    7. Sub
    zsmul : ℤ → A → A
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    7. ZSMul
    sub_eq_add_neg : ∀ (a b : A), a - b = a + -b
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    zsmul_zero' : ∀ (a : A), 0 • a = 0
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    zsmul_succ' : ∀ (n : ℕ) (a : A), ↑n.succ • a = ↑n • a + a
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    zsmul_neg' : ∀ (n : ℕ) (a : A), Int.negSucc n • a = -(↑n.succ • a)
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    6. SubNegMonoid
    neg_add_cancel : ∀ (a : A), -a + a = 0
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    5. AddGroup
    add_comm : ∀ (a b : A), a + b = b + a
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. AddCommGroup
    mul : A → A → A
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    4. Mul
    left_distrib : ∀ (a b c : A), a * (b + c) = a * b + a * c
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    right_distrib : ∀ (a b c : A), (a + b) * c = a * c + b * c
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    zero_mul : ∀ (a : A), 0 * a = 0
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    mul_zero : ∀ (a : A), a * 0 = 0
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    3. NonUnitalNonAssocRing
    mul_assoc : ∀ (a b c : A), a * b * c = a * (b * c)
    Inherited from
    1. NonUnitalNormedRing
    2. NonUnitalRing
    dist : A → A → ℝ
    Inherited from
    1. NonUnitalNormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    4. Dist
    dist_self : ∀ (x : A), dist x x = 0
    Inherited from
    1. NonUnitalNormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    dist_comm : ∀ (x y : A), dist x y = dist y x
    Inherited from
    1. NonUnitalNormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    dist_triangle : ∀ (x y z : A), dist x z ≤ dist x y + dist y z
    Inherited from
    1. NonUnitalNormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    edist : A → A → ENNReal
    Inherited from
    1. NonUnitalNormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    edist_dist : ∀ (x y : A), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
    Inherited from
    1. NonUnitalNormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    toUniformSpace : UniformSpace A
    Inherited from
    1. NonUnitalNormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    uniformity_dist : uniformity A = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε}
    Inherited from
    1. NonUnitalNormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    toBornology : Bornology A
    Inherited from
    1. NonUnitalNormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    cobounded_sets : (Bornology.cobounded A).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
    Inherited from
    1. NonUnitalNormedRing
    2. MetricSpace
    3. PseudoMetricSpace
    eq_of_dist_eq_zero : ∀ {x y : A}, dist x y = 0 → x = y
    Inherited from
    1. NonUnitalNormedRing
    2. MetricSpace
    dist_eq : ∀ (x y : A), dist x y = ‖-x + y‖
    Inherited from
    1. NonUnitalNormedRing
    norm_mul_le : ∀ (a b : A), ‖a * b‖ ≤ ‖a‖ * ‖b‖
    Inherited from
    1. NonUnitalNormedRing
    star : A → A
    Inherited from
    1. StarRing
    2. StarMul
    3. InvolutiveStar
    4. Star
    star_involutive : Function.Involutive star
    Inherited from
    1. StarRing
    2. StarMul
    3. InvolutiveStar
    star_mul : ∀ (r s : A), star (r * s) = star s * star r
    Inherited from
    1. StarRing
    2. StarMul
    star_add : ∀ (r s : A), star (r + s) = star r + star s
    Inherited from
    1. StarRing
    complete : ∀ {f : Filter A}, Cauchy f → ∃ x, f ≤ nhds x
    Inherited from
    1. CompleteSpace
    norm_mul_self_le : ∀ (x : A), ‖x‖ * ‖x‖ ≤ ‖star x * x‖
    Inherited from
    1. CStarRing
    smul : ℂ → A → A
    Inherited from
    1. NormedSpace
    2. Module
    3. DistribMulAction
    4. MulAction
    5. SemigroupAction
    6. SMul
    mul_smul : ∀ (x y : ℂ) (b : A), (x * y) • b = x • y • b
    Inherited from
    1. NormedSpace
    2. Module
    3. DistribMulAction
    4. MulAction
    5. SemigroupAction
    one_smul : ∀ (b : A), 1 • b = b
    Inherited from
    1. NormedSpace
    2. Module
    3. DistribMulAction
    4. MulAction
    smul_zero : ∀ (a : ℂ), a • 0 = 0
    Inherited from
    1. NormedSpace
    2. Module
    3. DistribMulAction
    smul_add : ∀ (a : ℂ) (x y : A), a • (x + y) = a • x + a • y
    Inherited from
    1. NormedSpace
    2. Module
    3. DistribMulAction
    add_smul : ∀ (r s : ℂ) (x : A), (r + s) • x = r • x + s • x
    Inherited from
    1. NormedSpace
    2. Module
    zero_smul : ∀ (x : A), 0 • x = 0
    Inherited from
    1. NormedSpace
    2. Module
    norm_smul_le : ∀ (a : ℂ) (b : A), ‖a • b‖ ≤ ‖a‖ * ‖b‖
    Inherited from
    1. NormedSpace
    smul_assoc : ∀ (x : ℂ) (y z : A), (x • y) • z = x • y • z
    Inherited from
    1. IsScalarTower
    smul_comm : ∀ (m : ℂ) (n a : A), m • n • a = n • m • a
    Inherited from
    1. SMulCommClass
    star_smul : ∀ (r : ℂ) (a : A), star (r • a) = star r • star a
    Inherited from
    1. StarModule
Lemma2.1.2
uses 1used by 1✓L∃∀N
Tagsmathlib

(Sakai 1.1.6) The involution on a C^*-algebra preserves the norm.

Lean code for Lemma2.1.2●1 theorem
  • theoremdefined in Mathlib/Analysis/CStarAlgebra/Basic.lean
    complete
    theorem CStarRing.to_normedStarGroup.{u_2} {E : Type u_2}
  [NonUnitalNormedRing E] [StarRing E] [CStarRing E] : NormedStarGroup E
    theorem CStarRing.to_normedStarGroup.{u_2}
  {E : Type u_2} [NonUnitalNormedRing E]
  [StarRing E] [CStarRing E] :
  NormedStarGroup E
    In a C⋆-ring, star preserves the norm.
Proof for Lemma 2.1.2
uses 0

Note \|x\|^2 = \|x^* x\| \le \|x^*\| \|x\|, and \|x^*\|^2 \le \|x x^*\| \le \|x\| \|x^*\|.

Theorem2.1.3
uses 1
Used by 4
Reverse dependency previews
Preview
Corollary 2.1.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsmathlib

(Sakai 1.2.1) Every commutative, unital C^*-algebra \mathcal{A} is *-isomorphic to C(K), the algebra of complex-valued continuous functions on K, where K is the compact Hausdorff space of maximal ideals of \mathcal{A}. (Note C(K) is itself a C^*-algebra with pointwise complex conjugation as * and the uniform norm.)

Lean code for Theorem2.1.3●1 definition
  • defdefined in Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
    complete
    def gelfandStarTransform.{u_1} (A : Type u_1) [CommCStarAlgebra A] :
  A ≃⋆ₐ[ℂ] C(↑(WeakDual.characterSpace ℂ A), ℂ)
    def gelfandStarTransform.{u_1} (A : Type u_1)
  [CommCStarAlgebra A] :
  A ≃⋆ₐ[ℂ]
    C(↑(WeakDual.characterSpace ℂ A), ℂ)
    The Gelfand transform as a `StarAlgEquiv` between a commutative unital C⋆-algebra over `ℂ`
and the continuous functions on its `characterSpace`.
Proof for Theorem 2.1.3
uses 0

By Banach algebra theory, the Gelfand transform provides a homomorphism of \mathcal{A} into C(K). A standard calculation using the C^*-identity shows that it is isometric. Mapping a self-adjoint element h to the unit circle (complex exponentiation) one can show that the spectrum lands on the unit circle and so the spectrum of h is in the reals. The spectrum of an element in C(K) is its range, from which *-preservation follows.

Corollary2.1.4
uses 1used by 1XL∃∀N

(Sakai 1.2.2) Let \mathcal{A} be a commutative C^*-algebra without identity. Then \mathcal{A} is *-isomorphic to the algebra C_0(\Omega) of continuous functions vanishing at infinity on a locally compact Hausdorff space \Omega. The space \Omega is called the spectrum space of \mathcal{A}.

Corollary2.1.5
Statement uses 2
Statement dependency previews
Preview
Theorem 2.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagsmathlib

(Non-unital continuous functional calculus) Let a be a self-adjoint element of a C^*-algebra \mathcal{A}. Then the C^*-subalgebra of \mathcal{A} generated by a is isometrically *-isomorphic to C_0(\sigma(a) \cup \{0\}), the algebra of complex-valued continuous functions on \sigma(a) \cup \{0\} that vanish at 0, via an isomorphism sending a to the identity function.

Lean code for Corollary2.1.5●2 declarations
  • defdefined in Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
    complete
    def cfcₙ.{u_3, u_4} {R : Type u_3} {A : Type u_4} {p : A → Prop}
  [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R]
  [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A]
  [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A]
  [SMulCommClass R A A]
  [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R)
  (a : A) : A
    def cfcₙ.{u_3, u_4} {R : Type u_3}
  {A : Type u_4} {p : A → Prop}
  [CommSemiring R] [Nontrivial R]
  [StarRing R] [MetricSpace R]
  [IsTopologicalSemiring R]
  [ContinuousStar R] [NonUnitalRing A]
  [StarRing A] [TopologicalSpace A]
  [Module R A] [IsScalarTower R A A]
  [SMulCommClass R A A]
  [instCFCₙ :
    NonUnitalContinuousFunctionalCalculus
      R A p]
  (f : R → R) (a : A) : A
    This is the *continuous functional calculus* of an element `a : A` in a non-unital algebra
applied to bare functions.  When either `a` does not satisfy the predicate `p` (i.e., `a` is not
`IsStarNormal`, `IsSelfAdjoint`, or `0 ≤ a` when `R` is `ℂ`, `ℝ`, or `ℝ≥0`, respectively), or when
`f : R → R` is not continuous on the quasispectrum of `a` or `f 0 ≠ 0`, then `cfcₙ f a` returns the
junk value `0`.

This is the primary declaration intended for widespread use of the continuous functional calculus
for non-unital algebras, and all the API applies to this declaration. For more information, see the
module documentation for `Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital`.
  • theoremdefined in Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
    complete
    theorem IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus.{u_1}
  {A : Type u_1} [NonUnitalCStarAlgebra A] :
  NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
    theorem IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus.{u_1}
  {A : Type u_1}
  [NonUnitalCStarAlgebra A] :
  NonUnitalIsometricContinuousFunctionalCalculus
    ℝ A IsSelfAdjoint
Proof for Corollary 2.1.5
uses 0

Pass to the unitization \tilde{\mathcal{A}} of \mathcal{A}, in which the spectrum of a is \sigma(a) \cup \{0\}. The unital C^*-subalgebra of \tilde{\mathcal{A}} generated by a is commutative, so by Theorem 2.1.3 it is C(K) for its maximal ideal space K. The Gelfand transform of a is a continuous map K \to \sigma(a) \cup \{0\}, which is bijective since a generates the algebra, and hence a homeomorphism by Lemma 7.1.1. This identifies the unital C^*-algebra generated by a with C(\sigma(a) \cup \{0\}), sending a to the identity function, and the (non-unital) C^*-algebra generated by a corresponds to the functions vanishing at 0.

Definition2.1.6
uses 1
Used by 3
Reverse dependency previews
Preview
Lemma 2.1.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A C^*-algebra M is called a W^*-algebra if it is a dual Banach space, i.e. if there exists a Banach space M_* so that (M_*)^* is isometrically isomorphic to M. We call M_* a predual of M.

Lean code for Definition2.1.6●2 definitions
  • class(1 method)defined in Mathlib/Analysis/VonNeumannAlgebra/Basic.lean
    complete
    class WStarAlgebra.{u} (M : Type u) [CStarAlgebra M] : Prop
    class WStarAlgebra.{u} (M : Type u)
  [CStarAlgebra M] : Prop
    Sakai's definition of a von Neumann algebra as a C⋆ algebra with a Banach space predual.

So that we can unambiguously talk about these "abstract" von Neumann algebras
in parallel with the "concrete" ones (weakly closed \*-subalgebras of B(H)),
we name this definition `WStarAlgebra`.

Note that for now we only assert the mere existence of predual, rather than picking one.
This may later prove problematic, and need to be revisited.
Picking one may cause problems with definitional unification of different instances.
One the other hand, not picking one means that the weak-\* topology
(which depends on a choice of predual) must be defined using the choice,
and we may be unhappy with the resulting opaqueness of the definition.

    Methods

    exists_predual : ∃ X x x_1, ∃ (_ : CompleteSpace X), Nonempty (StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    There is a Banach space `X` whose dual is isometrically (conjugate-linearly) isomorphic
to the `WStarAlgebra`.
  • class(1 method)defined in LeanOA/Ultraweak/Basic.lean
    complete
    class Predual.{u_1, u_2, u_3} (𝕜 : Type u_1) (M : Type u_2) (P : Type u_3)
  [RCLike 𝕜] [NormedAddCommGroup M] [NormedAddCommGroup P]
  [NormedSpace 𝕜 M] [NormedSpace 𝕜 P] : Type (max (max u_1 u_2) u_3)
    class Predual.{u_1, u_2, u_3} (𝕜 : Type u_1)
  (M : Type u_2) (P : Type u_3) [RCLike 𝕜]
  [NormedAddCommGroup M]
  [NormedAddCommGroup P] [NormedSpace 𝕜 M]
  [NormedSpace 𝕜 P] :
  Type (max (max u_1 u_2) u_3)
    A class which encodes a specified isometric linear isomorpism between `M`
and the strong dual of `P`, so that we may treat `P` as a predual of `M`.

    Methods

    equivDual : M ≃ₗᵢ[𝕜] StrongDual 𝕜 P
    A linear isometric equivalence between `M` and the dual of its predual `P`.

It is premature to fix a notation like M_* in the above, but the aim of this project is to prove that any two preduals of M are isomorphic as Banach spaces, so we take the liberty with Sakai of fixing a reference predual at the outset. The formalization also takes M to be unital from the start; this loses no generality, by Lemma 8.1.8.

Lemma2.1.7
Statement uses 3
Statement dependency previews
Preview
Corollary 1.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

(Sakai 1.1.4) A self-adjoint, \sigma-closed *-subalgebra N of a W^*-algebra M is also a W^*-algebra, since (M_* / N^0)^* = N, where N^0 is the polar (annihilator) of N in M_*, i.e. the set of \varphi \in M_* such that \varphi(x) = 0 for all x \in N.

Lean code for Lemma2.1.7●2 definitions
  • abbrevdefined in LeanOA/Ultraweak/ClosedSubspace.lean
    complete
    abbrev Ultraweak.predualOfIsClosed.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {M : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup M]
  [NormedSpace 𝕜 M] [NormedAddCommGroup P] [NormedSpace 𝕜 P]
  [Predual 𝕜 M P] (N : Submodule 𝕜 M)
  (hN : IsClosed (ofUltraweak ⁻¹' ↑N)) :
  Predual 𝕜 (↥N) (Ultraweak.Subpredual P N)
    abbrev Ultraweak.predualOfIsClosed.{u_1, u_2,
    u_3}
  {𝕜 : Type u_1} {M : Type u_2}
  {P : Type u_3} [RCLike 𝕜]
  [NormedAddCommGroup M] [NormedSpace 𝕜 M]
  [NormedAddCommGroup P] [NormedSpace 𝕜 P]
  [Predual 𝕜 M P] (N : Submodule 𝕜 M)
  (hN : IsClosed (ofUltraweak ⁻¹' ↑N)) :
  Predual 𝕜 (↥N)
    (Ultraweak.Subpredual P N)
    **Sakai 1.1.4**: an ultraweakly closed subspace `N` of `M` is the dual of `P ⧸ N_⊥`.
  • defdefined in LeanOA/Mathlib/Analysis/Normed/Module/DualQuotient.lean
    complete
    def Submodule.equivDualQuotientPolarSubmodule.{u_1, u_2} {𝕜 : Type u_1}
  {X : Type u_2} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
  (N : Submodule 𝕜 (StrongDual 𝕜 X))
  (hN : IsClosed (⇑WeakDual.toStrongDual ⁻¹' ↑N)) :
  ↥N ≃ₗᵢ[𝕜] StrongDual 𝕜 (X ⧸ (topDualPairing 𝕜 X).polarSubmodule N)
    def Submodule.equivDualQuotientPolarSubmodule.{u_1,
    u_2}
  {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup X] [NormedSpace 𝕜 X]
  (N : Submodule 𝕜 (StrongDual 𝕜 X))
  (hN :
    IsClosed
      (⇑WeakDual.toStrongDual ⁻¹' ↑N)) :
  ↥N ≃ₗᵢ[𝕜]
    StrongDual 𝕜
      (X ⧸
        (topDualPairing 𝕜
              X).polarSubmodule
          N)
    If `N` is a weak⋆ closed subspace of the dual of `X`, then `N` is isometrically isomorphic to
the dual of `X ⧸ (topDualPairing 𝕜 X).polarSubmodule N`.
Proof for Lemma 2.1.7
uses 0

Restriction to N identifies the dual of M_* / N^0 isometrically with the subspace of M = (M_*)^* annihilating N^0, and by Corollary 1.6 this is the \sigma-closure of N, which is N itself.

2.2. The Ultraweak (Sigma) Topology🔗

Definition2.2.1
Statement uses 2
Statement dependency previews
Preview
Definition 1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 17
Reverse dependency previews
Preview
Lemma 2.1.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The weak-* topology \sigma(M, M_*) on a W^*-algebra M, that is, the weak topology of the pairing M \times M_* \to \mathbb{C} (Definition 1.1), is called the \sigma-topology, or ultraweak topology.

Lean code for Definition2.2.1●1 definition
  • abbrevdefined in LeanOA/Ultraweak/Basic.lean
    complete
    abbrev Ultraweak.{u_1, u_2, u_3} (𝕜 : Type u_1) (M : Type u_2) (P : Type u_3)
  [RCLike 𝕜] [NormedAddCommGroup M] [NormedAddCommGroup P]
  [NormedSpace 𝕜 M] [NormedSpace 𝕜 P] [Predual 𝕜 M P] : Type u_2
    abbrev Ultraweak.{u_1, u_2, u_3} (𝕜 : Type u_1)
  (M : Type u_2) (P : Type u_3) [RCLike 𝕜]
  [NormedAddCommGroup M]
  [NormedAddCommGroup P] [NormedSpace 𝕜 M]
  [NormedSpace 𝕜 P] [Predual 𝕜 M P] :
  Type u_2
    A type synonym of `M` equipped with the *ultraweak topology* (also known as the
*σ-weak topology*) relative to a given predual `P`. This is the weak-* topology on
`M` induced by the isometric isomorphism with the dual of `P`. `Ultraweak 𝕜 P M` is
equipped with the scoped notation `σ(M, P)_𝕜`.

The topology is only defined in the presence of a `Predual 𝕜 P M` instance.
Proposition2.2.2
Statement uses 3
Statement dependency previews
Preview
Definition 1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 5
Reverse dependency previews
Preview
Lemma 2.2.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The set of \sigma(M, M_*)-continuous linear functionals is precisely M_*.

Lean code for Proposition2.2.2●2 theorems
  • theoremdefined in LeanOA/Ultraweak/Dual.lean
    complete
    theorem Ultraweak.continuous_iff_exists_eq.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {M : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup M]
  [NormedSpace 𝕜 M] [NormedAddCommGroup P] [NormedSpace 𝕜 P]
  [Predual 𝕜 M P] (f : M →ₗ[𝕜] 𝕜) :
  (Continuous fun x ↦ f (ofUltraweak x)) ↔
    ∃ p, ∀ (m : M), f m = (Predual.equivDual m) p
    theorem Ultraweak.continuous_iff_exists_eq.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {M : Type u_2}
  {P : Type u_3} [RCLike 𝕜]
  [NormedAddCommGroup M] [NormedSpace 𝕜 M]
  [NormedAddCommGroup P] [NormedSpace 𝕜 P]
  [Predual 𝕜 M P] (f : M →ₗ[𝕜] 𝕜) :
  (Continuous fun x ↦ f (ofUltraweak x)) ↔
    ∃ p,
      ∀ (m : M),
        f m = (Predual.equivDual m) p
    A linear functional on `M` is ultraweakly continuous if and only if it is evaluation at some
element of the predual.
  • theoremdefined in LeanOA/Ultraweak/Dual.lean
    complete
    theorem Ultraweak.continuous_iff_mem_range.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {M : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup M]
  [NormedSpace 𝕜 M] [NormedAddCommGroup P] [NormedSpace 𝕜 P]
  [Predual 𝕜 M P] (f : StrongDual 𝕜 M) :
  (Continuous fun x ↦ f (ofUltraweak x)) ↔
    f ∈ Set.range ⇑(Predual.toDual 𝕜 M P)
    theorem Ultraweak.continuous_iff_mem_range.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {M : Type u_2}
  {P : Type u_3} [RCLike 𝕜]
  [NormedAddCommGroup M] [NormedSpace 𝕜 M]
  [NormedAddCommGroup P] [NormedSpace 𝕜 P]
  [Predual 𝕜 M P] (f : StrongDual 𝕜 M) :
  (Continuous fun x ↦ f (ofUltraweak x)) ↔
    f ∈ Set.range ⇑(Predual.toDual 𝕜 M P)
    A norm continuous linear functional on `M` is ultraweakly continuous if and only if it lies in
the range of the canonical embedding of the predual.
Proof for Proposition 2.2.2
uses 0

This is Lemma 1.3 for the pairing of M with M_*, which separates the points of M_*. Equivalently, \sigma(M, M_*) is compatible with this pairing (Definition 1.2).

Lemma2.2.3
Statement uses 3
Statement dependency previews
Preview
Theorem 1.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 2.2.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

(Sakai 1.7.6) Let p be any projection in M. Then the subspace pMp is \sigma-closed.

Lean code for Lemma2.2.3●1 theorem
  • theoremdefined in LeanOA/Ultraweak/Corner.lean
    complete
    theorem IsStarProjection.isClosed_cornerSubmodule_of_ultraweak.{u_1, u_2}
  {M : Type u_1} {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℂ P]
  [CompleteSpace P] [CStarAlgebra M] [PartialOrder M]
  [StarOrderedRing M] [Predual ℂ M P] {e : Ultraweak ℂ M P}
  (he : IsStarProjection e) :
  IsClosed ↑(IsStarProjection.cornerSubmodule ℂ he)
    theorem IsStarProjection.isClosed_cornerSubmodule_of_ultraweak.{u_1,
    u_2}
  {M : Type u_1} {P : Type u_2}
  [NormedAddCommGroup P] [NormedSpace ℂ P]
  [CompleteSpace P] [CStarAlgebra M]
  [PartialOrder M] [StarOrderedRing M]
  [Predual ℂ M P] {e : Ultraweak ℂ M P}
  (he : IsStarProjection e) :
  IsClosed
    ↑(IsStarProjection.cornerSubmodule ℂ
        he)
Proof for Lemma 2.2.3
uses 0

By Theorem 1.7 it suffices to show that pMp \cap S is \sigma-closed, where S is the closed unit ball, and since x \mapsto x^* is \sigma-continuous (Lemma 5.2) it suffices to treat the self-adjoint part. If P denotes the positive elements, then pM^sp \cap S = (pPp \cap S) - (pPp \cap S) = ([0, p] \cap S) - ([0, p] \cap S). The order interval [0, p] is \sigma-closed by Lemma 5.2, and S is \sigma-compact, so this is the continuous image of a compact set, hence closed.

That x \mapsto pxp is \sigma-continuous, which Sakai also includes in 1.7.6, follows from Lemma 2.2.6.

Lemma2.2.4
Statement uses 3
Statement dependency previews
Preview
Lemma 2.1.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

If p \in M is a projection, then pMp is also a W^*-algebra with identity p.

Lean code for Lemma2.2.4●2 definitions
  • defdefined in LeanOA/CStarAlgebra/Corner/Basic.lean
    complete
    def IsStarProjection.Corner.instCStarAlgebra.{u_2} {A : Type u_2}
  [NonUnitalCStarAlgebra A] (p : A) {hp : IsStarProjection p} :
  CStarAlgebra hp.Corner
    def IsStarProjection.Corner.instCStarAlgebra.{u_2}
  {A : Type u_2} [NonUnitalCStarAlgebra A]
  (p : A) {hp : IsStarProjection p} :
  CStarAlgebra hp.Corner
    The corner `p * A * p` of a non-unital C⋆-algebra is a C⋆-algebra with unit `p`.
  • defdefined in LeanOA/Ultraweak/ClosedSubspace.lean
    complete
    def IsStarProjection.Corner.instPredual.{u_1, u_2} {M : Type u_1}
  {P : Type u_2} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M]
  [NormedAddCommGroup P] [NormedSpace ℂ P] [CompleteSpace P]
  [Predual ℂ M P] {p : M} {hp : IsStarProjection p} :
  Predual ℂ hp.Corner
    (Ultraweak.Subpredual P (IsStarProjection.cornerSubmodule ℂ hp))
    def IsStarProjection.Corner.instPredual.{u_1,
    u_2}
  {M : Type u_1} {P : Type u_2}
  [CStarAlgebra M] [PartialOrder M]
  [StarOrderedRing M]
  [NormedAddCommGroup P] [NormedSpace ℂ P]
  [CompleteSpace P] [Predual ℂ M P]
  {p : M} {hp : IsStarProjection p} :
  Predual ℂ hp.Corner
    (Ultraweak.Subpredual P
      (IsStarProjection.cornerSubmodule ℂ
        hp))
    The predual of the corner `hp.Corner` of a W⋆-algebra `M` with predual `P`. Together with
`IsStarProjection.Corner.instCStarAlgebra`, this makes `hp.Corner` into a W⋆-algebra with
unit `p`.
Proof for Lemma 2.2.4
uses 0

It is clear that eMe is an algebra, since any sum or product of elements preserves the pre- and post-multiplication by e. It is also clear that e is the multiplicative identity of this algebra. The product-reversing property of * and the fact that e is a self-adjoint projection imply that eMe is a *-algebra. By Lemma 2.1.7, if this *-subalgebra is \sigma-closed, then it is a W^*-subalgebra of M. But this is the result of Lemma 2.2.3.

Lemma2.2.5
Statement uses 3
Statement dependency previews
Preview
Theorem 1.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 2.2.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

(Sakai 1.7.7) If p is any projection of M, then the mappings x \mapsto px and x \mapsto xp are \sigma-continuous.

Lean code for Lemma2.2.5●1 theorem
  • theoremdefined in LeanOA/Ultraweak/Multiplication.lean
    complete
    theorem Ultraweak.continuous_mul_left_of_isStarProjection.{u_1, u_2}
  {M : Type u_1} {P : Type u_2} [CStarAlgebra M] [PartialOrder M]
  [StarOrderedRing M] [NormedAddCommGroup P] [NormedSpace ℂ P]
  [CompleteSpace P] [Predual ℂ M P] {p : Ultraweak ℂ M P}
  (hp : IsStarProjection p) : Continuous fun x ↦ p * x
    theorem Ultraweak.continuous_mul_left_of_isStarProjection.{u_1,
    u_2}
  {M : Type u_1} {P : Type u_2}
  [CStarAlgebra M] [PartialOrder M]
  [StarOrderedRing M]
  [NormedAddCommGroup P] [NormedSpace ℂ P]
  [CompleteSpace P] [Predual ℂ M P]
  {p : Ultraweak ℂ M P}
  (hp : IsStarProjection p) :
  Continuous fun x ↦ p * x
    Left multiplication by a projection is ultraweakly continuous.
Proof for Lemma 2.2.5
uses 0

We follow arXiv:2009.05825, §5.3. Let q = 1 - p and let S be the closed unit ball. For y \in S, \lambda \in \mathbb{C} and b \in qMp, the C^*-identity gives \|pyq + \lambda p\| \le (1 + |\lambda|^2)^{1/2} and \|pyq + b\| \le \max(1, \|b\|). Since closed balls are \sigma-closed, these estimates pass to \sigma-limits x of nets (p y_\alpha q), and force pxp = qxq = qxp = 0, so that x \in pSq. Thus pSq is \sigma-compact. Since also pSp is \sigma-compact (Lemma 2.2.3), so is pS = (pSp + pSq) \cap S, and by Theorem 1.7 pM is \sigma-closed; likewise qM. Hence x \mapsto px is a bounded idempotent map whose range pM and kernel qM are \sigma-closed, and such a map is \sigma-continuous (by compactness of the unit ball and Theorem 1.7). The claim for x \mapsto xp follows by taking adjoints.

Lemma2.2.6
Statement uses 4
Statement dependency previews
Preview
Definition 2.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 5
Reverse dependency previews
Preview
Lemma 4.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

(Sakai 1.7.8) The mappings x \mapsto x^*, x \mapsto ax, and x \mapsto xa are \sigma-continuous for x, a \in M.

Lean code for Lemma2.2.6●2 theorems
  • theoremdefined in LeanOA/Ultraweak/Multiplication.lean
    complete
    theorem Ultraweak.instSeparatelyContinuousMul.{u_1, u_2} {M : Type u_1}
  {P : Type u_2} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M]
  [NormedAddCommGroup P] [NormedSpace ℂ P] [CompleteSpace P]
  [Predual ℂ M P] : SeparatelyContinuousMul (Ultraweak ℂ M P)
    theorem Ultraweak.instSeparatelyContinuousMul.{u_1,
    u_2}
  {M : Type u_1} {P : Type u_2}
  [CStarAlgebra M] [PartialOrder M]
  [StarOrderedRing M]
  [NormedAddCommGroup P] [NormedSpace ℂ P]
  [CompleteSpace P] [Predual ℂ M P] :
  SeparatelyContinuousMul
    (Ultraweak ℂ M P)
    **Sakai 1.7.8**: multiplication on `σ(M, P)` is separately ultraweakly continuous.
  • theoremdefined in LeanOA/Ultraweak/Multiplication.lean
    complete
    theorem Ultraweak.instIsSemitopologicalRing.{u_1, u_2} {M : Type u_1}
  {P : Type u_2} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M]
  [NormedAddCommGroup P] [NormedSpace ℂ P] [CompleteSpace P]
  [Predual ℂ M P] : IsSemitopologicalRing (Ultraweak ℂ M P)
    theorem Ultraweak.instIsSemitopologicalRing.{u_1,
    u_2}
  {M : Type u_1} {P : Type u_2}
  [CStarAlgebra M] [PartialOrder M]
  [StarOrderedRing M]
  [NormedAddCommGroup P] [NormedSpace ℂ P]
  [CompleteSpace P] [Predual ℂ M P] :
  IsSemitopologicalRing (Ultraweak ℂ M P)
    `σ(M, P)` is a semitopological ring.
Proof for Lemma 2.2.6
uses 0

The set of a for which x \mapsto ax is \sigma-continuous is a linear subspace containing the projections (Lemma 2.2.5). It is norm closed, because the \sigma-continuous functionals form a norm closed subspace of M^* (Proposition 2.2.2). Since the span of the projections is norm dense (Lemma 6.5), it is all of M. The claim for x \mapsto xa follows by taking adjoints.