Weak-* compactness of the state space

The state space of a unital C*-algebra, viewed inside the weak-* dual WeakDual ℂ A, is weak- compact* (Banach-Alaoglu): it is a weak-* closed subset of the unit ball, being the intersection of the (weak-* closed) positivity conditions 0 ≤ φ (star a * a) and the normalization φ 1 = 1. This is the first step toward the existence of pure states via Krein-Milman.

Main results

• Physicslib4.GNS.weakStateSet — the state space realized in WeakDual ℂ A.
• Physicslib4.GNS.isClosed_weakStateSet — it is weak-* closed.
• Physicslib4.GNS.isCompact_weakStateSet — it is weak-* compact.

Note on pure-state existence

Concluding the existence of a pure state by Krein-Milman needs LocallyConvexSpace ℝ (WeakDual ℂ A), which in turn requires the scalar-tower instance IsScalarTower ℝ ℂ (A →L[ℂ] ℂ); the latter does not resolve in the current Mathlib due to a real/complex module diamond on the dual space. The extreme-point-to-state transfer also needs weak-* coercion-algebra lemmas ((t • φ + (1-t) • ψ) a = t • φ a + (1-t) • ψ a) which Mathlib does not provide for WeakDual. Both are recorded as follow-ups; the compactness result below is the reusable substance.

def Physicslib4.GNS.weakStateSet {A : Type u_1} [CStarAlgebra A] : Set (WeakDual ℂ A)

The state space realized inside the weak-* dual WeakDual ℂ A: the positive, normalized (φ 1 = 1) continuous functionals. For a positive functional, φ 1 = 1 is equivalent to ‖φ‖ = 1, so this is exactly the set of states.

Equations

• Physicslib4.GNS.weakStateSet = {φ : WeakDual ℂ A | (∀ (a : A), 0 ≤ φ (star a * a)) ∧ φ 1 = 1}

noncomputable def Physicslib4.GNS.State.toWeakDual {A : Type u_1} [CStarAlgebra A] (ω : State A) : WeakDual ℂ A

A state, viewed as an element of the weak-* dual.

Equations

• ω.toWeakDual = StrongDual.toWeakDual ω.toContinuousLinearMap

@[simp]

theorem Physicslib4.GNS.State.toWeakDual_apply {A : Type u_1} [CStarAlgebra A] (ω : State A) (a : A) : ω.toWeakDual a = ω a

theorem Physicslib4.GNS.State.toWeakDual_mem_weakStateSet {A : Type u_1} [CStarAlgebra A] (ω : State A) : ω.toWeakDual ∈ weakStateSet

theorem Physicslib4.GNS.isClosed_complex_nonneg : IsClosed {z : ℂ | 0 ≤ z}

The nonnegative reals inside ℂ form a closed set.

theorem Physicslib4.GNS.isClosed_weakStateSet {A : Type u_1} [CStarAlgebra A] : IsClosed weakStateSet

theorem Physicslib4.GNS.isCompact_weakStateSet {A : Type u_1} [CStarAlgebra A] [Nontrivial A] : IsCompact weakStateSet