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.
An extreme point of the state space: ω is not a mixture t ω₁ + (1 − t) ω₂ of two distinct states.
The states of A form a convex set: a mixture of states with weights t and 1 − t is a state
(State.convexCombo). ω is extreme when ω = t ω₁ + (1 − t) ω₂ with 0 < t < 1 forces ω₁ = ω₂,
and then both equal ω. Physically, an extreme state carries no classical uncertainty about which
state the system is in. Extremality is equivalent to purity (isPure_iff_isExtremePoint) and to
membership in Mathlib's extremePoints of the state space
(mem_extremePoints_iff_isExtremePoint).
Implementation note: the decomposition is stated pointwise, ω(a) = t ω₁(a) + (1 − t) ω₂(a) for all a ∈ A, with real t.
Blueprint: def:extreme-state
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 Φ of A: the state a ↦ ω(Φ(a)).
If Φ is a symmetry of the observables, for instance the automorphism β_L of the quasilocal
algebra induced by a Poincaré transformation L, then ω ∘ Φ is the transformed state. It is a
state: positivity follows from Φ(a* a) = Φ(a)* Φ(a), and normalisation from Φ(1) = 1. Purity is
preserved (isPure_precomp_iff). State.comp is the general pullback along a unital
*-homomorphism between two algebras.
Implementation note: Φ enters as a continuous linear map through starAlgEquivCLM; a
-automorphism of a C-algebra is isometric.
Blueprint: the pullback of thrm:purity-covariance-invariant
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 mixture s ω₁ + (1 − s) ω₂ of two states, for 0 ≤ s ≤ 1, as a state.
Physically this is the state of a system prepared in ω₁ with probability s and in ω₂ with
probability 1 − s. Positivity is clear, and the mixture takes the value s + (1 − s) = 1 on the
unit; a positive functional has norm equal to its value at 1, so it is normalised. This shows
that the state space is convex (convex_stateSpace).
Blueprint: the convex combination of thrm:state-space-convex-bridge
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: the set of all states, as a subset of the continuous linear functionals.
The states of A form a convex set (convex_stateSpace), whose extreme points are the pure
states (mem_extremePoints_iff_isExtremePoint, isPure_iff_isExtremePoint), so Mathlib's
Convex and extremePoints apply to it.
Implementation note: the set is the image of State A in A →L[ℂ] ℂ, regarded as a real vector
space through NormedSpace.complexToReal, with the norm topology. The weak-* compact version is
weakStateSet; mathematically the Krein–Milman theorem applies to it, and the library proves the
compactness, not the application.
Blueprint: the state space of thrm:state-space-convex-bridge
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.
A unital *-homomorphism of C*-algebras as a continuous ℂ-linear map; it is
contractive (‖π a‖ ≤ ‖a‖, NonUnitalStarAlgHom.norm_apply_le), hence bounded with
norm ≤ 1.
Equations
- Physicslib4.GNS.starAlgHomCLM π = (↑π).toLinearMap.mkContinuous 1 ⋯
Instances For
The pullback ω ∘ π of a state ω on B along a unital *-homomorphism π : A → B: a ↦ ω(π(a)).
Positivity follows from π(a* a) = π(a)* π(a), and normalisation from π(1) = 1, since a positive
functional has norm equal to its value at 1. The pullback is contravariantly functorial
(State.comp_id, State.comp_comp): a *-homomorphism A → B gives a map from the states of B to
the states of A. Along a *-isomorphism Φ, purity is preserved in both directions
(isPure_comp_iff), and the GNS representation of ω ∘ Φ is that of ω composed with Φ, up to
unitary equivalence (unitaryEquiv_comp_of_gns). An example is the restriction of a global
state to a local algebra along the inclusion ι_B.
Implementation note: π enters as a continuous linear map through starAlgHomCLM, since a
-homomorphism of C-algebras is contractive. The automorphism case is also available as
State.precomp.
Blueprint: def:state-pullback
Equations
- ω.comp π = { toContinuousLinearMap := ω.toContinuousLinearMap ∘SL Physicslib4.GNS.starAlgHomCLM π, isPositive := ⋯, isNormalized := ⋯ }
Instances For
Functoriality (identity). Pulling a state back along the identity
*-homomorphism leaves it unchanged.
Functoriality (composition). The pullback is contravariant: for
π₁ : A →⋆ₐ[ℂ] B and π₂ : B →⋆ₐ[ℂ] C, pulling ω : State C back along the
composite π₂ ∘ π₁ equals pulling back first along π₂, then along π₁.
Purity is preserved by pullback along a *-isomorphism (one direction).
If ω is a pure state on B and Φ : A ≃⋆ₐ[ℂ] B, then the pullback ω ∘ Φ is a
pure state on A. A dominated positive functional ψ ≤ ω ∘ Φ on A transports to
ψ ∘ Φ⁻¹ ≤ ω on B, which purity of ω sends to a scalar multiple of ω;
transporting back gives ψ proportional to ω ∘ Φ.
Pulling a state back along Φ and then along Φ⁻¹ recovers the original state.
Purity is invariant under a *-isomorphism: for Φ : A ≃⋆ₐ[ℂ] B and a state
ω on B, the pullback ω ∘ Φ is pure iff ω is. This is the cross-algebra
generalization of isPure_precomp_iff (the *-automorphism case).