Pure states and extreme points of the state space #
A state ω on a unital C*-algebra A is pure (Physicslib4.GNS.IsPure) when
every positive functional ψ dominated by ω is a scalar multiple of ω. The
convex-geometric counterpart is that ω is an extreme point of the (convex)
state space: it is not a nontrivial convex combination of two distinct states.
This file proves the equivalence
IsPure ω ↔ ω.IsExtremePoint,
a classical characterization of purity. The analytic crux is the identity
‖φ‖ = (φ 1).re
for a positive linear functional φ on a unital C*-algebra
(norm_eq_re_apply_one_of_positive), obtained from the Cauchy-Schwarz inequality
for positive functionals together with the C*-norm identity ‖star b * b‖ = ‖b‖².
It is the bridge that lets us normalize positive functionals into states and back.
‖ψ‖ = (ψ 1).rerecovers the normalizationω 1 = 1for states (State.apply_one), pins the convex coefficients in the forward direction, and rescales the two piecesψandω - ψinto states in the backward direction.
Norm of a positive functional. For a positive linear functional φ on a
unital C*-algebra, ‖φ‖ = (φ 1).re. The reverse bound (φ 1).re ≤ ‖φ‖ is
immediate from ‖1‖ = 1; the forward bound uses Cauchy-Schwarz with the first
slot equal to 1, namely ‖φ b‖² ≤ (φ 1).re · (φ (b* b)).re ≤ (φ 1).re · ‖φ‖ · ‖b‖²,
which gives ‖φ‖² ≤ (φ 1).re · ‖φ‖.
A state evaluates to 1 on the unit: ω 1 = 1. The real part is ‖ω‖ = 1
(via norm_eq_re_apply_one_of_positive and normalization), and the imaginary part
vanishes by positivity at 1.
A state ω is an extreme point of the state space if it is not a
nontrivial convex combination of two distinct states: whenever
ω = t·ω₁ + (1-t)·ω₂ with 0 < t < 1 and ω₁, ω₂ states, then ω₁ = ω₂
(and hence both equal ω).
Equations
Instances For
Pure ⟹ extreme point. If ω is pure and decomposes as a convex
combination ω = t·ω₁ + (1-t)·ω₂ of states with 0 < t < 1, then t·ω₁ is a
positive functional dominated by ω, hence (by purity) a scalar multiple of ω;
evaluating at 1 (where all states give 1) pins the scalar to t, forcing
ω₁ = ω, and symmetrically ω₂ = ω.
Extreme point ⟹ pure. If ω is an extreme point and ψ is a positive
functional dominated by ω, set λ = (ψ 1).re ∈ [0,1]. For λ ∈ (0,1) the
rescaled functionals λ⁻¹·ψ and (1-λ)⁻¹·(ω-ψ) are states (normalized via
norm_eq_re_apply_one_of_positive) with ω = λ·(λ⁻¹ψ) + (1-λ)·((1-λ)⁻¹(ω-ψ)), so
extremality identifies them and forces ψ = λ·ω. The boundary cases λ = 0
(ψ = 0) and λ = 1 (ψ = ω) are handled separately.
Purity ⟺ extreme point of the state space.
A *-automorphism of a C*-algebra as a continuous ℂ-linear map; it is
isometric (StarAlgEquiv.isometry), hence bounded with norm ≤ 1.
Equations
Instances For
The pullback of a state along a *-automorphism Φ: a ↦ ω (Φ a). It is
again a state - positivity is the Φ-equivariance of star a * a, and the
normalization ‖ω ∘ Φ‖ = 1 follows since Φ is unital ((ω∘Φ)(1) = ω(1) = 1)
and positive functionals have norm equal to their value at 1.
Equations
- ω.precomp Φ = { toContinuousLinearMap := ω.toContinuousLinearMap ∘SL Physicslib4.GNS.starAlgEquivCLM Φ, isPositive := ⋯, isNormalized := ⋯ }
Instances For
Purity is preserved by pullback along a *-automorphism (one direction).
If ω is pure, so is ω ∘ Φ. A dominated positive functional ψ ≤ ω ∘ Φ becomes
ψ ∘ Φ⁻¹ ≤ ω after transport, which purity sends to a scalar multiple of ω;
transporting back gives ψ proportional to ω ∘ Φ.
The convex combination s·ω₁ + (1-s)·ω₂ of two states (0 ≤ s ≤ 1). It is
again a state: positivity is clear, and normalization ‖·‖ = 1 follows since the
combination is positive and evaluates to s·1 + (1-s)·1 = 1 on the unit.
Equations
- ω₁.convexCombo ω₂ s hs0 hs1 = { toContinuousLinearMap := ↑s • ω₁.toContinuousLinearMap + ↑(1 - s) • ω₂.toContinuousLinearMap, isPositive := ⋯, isNormalized := ⋯ }
Instances For
Purity is invariant under a *-automorphism: ω ∘ Φ is pure iff ω is.
On a Haag-Kastler net with Φ = β_L the covariance automorphism, this says purity
of a state is a covariance-invariant property.
The coercion State A → (A →L[ℂ] ℂ) is injective.
The state space of A realized as a subset of the real topological vector
space A →L[ℂ] ℂ (which carries a real-module structure via
NormedSpace.complexToReal): the image of all states under the coercion.
Instances For
The state space is convex. A real convex combination a·ω₁ + b·ω₂
(a, b ≥ 0, a + b = 1) of two states is again a state, via State.convexCombo.
Bridge to Mathlib's convex-geometry API. A state ω, viewed in the
ambient space A →L[ℂ] ℂ, is an extreme point of the state space (Set.extremePoints)
exactly when it is an extreme point in the sense of State.IsExtremePoint.