Purity of states on the quasilocal algebra

The canonical quasilocal algebra 𝔘 of a Minkowski Haag-Kastler net is a unital C*-algebra, so the abstract characterizations of purity apply to it. This file registers them for 𝔘:

• a state on 𝔘 is pure iff it is an extreme point of the state space;
• a state on 𝔘 is pure iff its GNS representation is irreducible.

Unlike the curved setting, Minkowski spacetime has a single global quasilocal algebra 𝔘, so these are statements about its global state space - the natural home for the vacuum and other distinguished states.

Main results

• Physicslib4.AQFT.HaagKastler.HaagKastlerNet.pure_iff_extreme
• Physicslib4.AQFT.HaagKastler.HaagKastlerNet.exists_gns_pure_iff_irreducible

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.pure_iff_extreme (N : HaagKastlerNet) (ω : GNS.State N.quasilocal.carrier) : GNS.IsPure ω ↔ ω.IsExtremePoint

Pure ⟺ extreme point for the quasilocal algebra. A state ω on the canonical quasilocal algebra 𝔘 of a Minkowski Haag-Kastler net is pure if and only if it is an extreme point of the state space of 𝔘. This is the abstract equivalence isPure_iff_isExtremePoint applied to the C*-algebra 𝔘.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.exists_gns_pure_iff_irreducible (N : HaagKastlerNet) (ω : GNS.State N.quasilocal.carrier) : ∃ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H), GNS.IsCyclicVector π Ω ∧ (∀ (a : N.quasilocal.carrier), ω a = inner ℂ Ω ((π a) Ω)) ∧ (GNS.IsPure ω ↔ GNS.IsIrreducible π)

Pure ⟺ irreducible GNS representation for the quasilocal algebra. For a state ω on the quasilocal algebra 𝔘, there is a GNS triple (H, π, Ω) reproducing ω in which ω is pure if and only if the representation π is irreducible (its commutant is trivial). This combines the GNS construction with the abstract isPure_iff_isIrreducible.