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 u) (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.

GNS covariance for the local algebras

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.unitaryEquiv_gns_covEquiv (N : HaagKastlerNet) (L : InhomogeneousLorentzGroup) (B : Set StandardMinkowskiSpacetime.Carrier) (ω : GNS.State (N.algebra (L • B))) {H₁ : Type u_1} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] (π₁ : N.algebra B →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁) {H₂ : Type u_2} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : N.algebra (L • B) →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₁ : GNS.IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : N.algebra B), (ω.comp (N.covEquiv L B).toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) (hcyc₂ : GNS.IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (b : N.algebra (L • B)), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) : GNS.UnitaryEquiv π₁ (π₂.comp (N.covEquiv L B).toStarAlgHom)

GNS covariance for local algebras. The Axiom 5 covariance equivalence α_L : 𝔘(B) ≃⋆ₐ[ℂ] 𝔘(L·B) is a *-isomorphism of local algebras, so a cyclic representation of 𝔘(B) reproducing the pullback state ω ∘ α_L is unitarily equivalent to π_ω ∘ α_L.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isIrreducible_iff_gns_covEquiv (N : HaagKastlerNet) (L : InhomogeneousLorentzGroup) (B : Set StandardMinkowskiSpacetime.Carrier) (ω : GNS.State (N.algebra (L • B))) {H₁ : Type u_1} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] (π₁ : N.algebra B →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁) {H₂ : Type u_2} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : N.algebra (L • B) →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₁ : GNS.IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : N.algebra B), (ω.comp (N.covEquiv L B).toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) (hcyc₂ : GNS.IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (b : N.algebra (L • B)), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) : GNS.IsIrreducible π₁ ↔ GNS.IsIrreducible π₂

Irreducibility is constant along the Lorentz orbit of a region. With the GNS data above, π₁ is irreducible exactly when π₂ is.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isFactor_iff_gns_covEquiv (N : HaagKastlerNet) (L : InhomogeneousLorentzGroup) (B : Set StandardMinkowskiSpacetime.Carrier) (ω : GNS.State (N.algebra (L • B))) {H₁ : Type u_1} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] (π₁ : N.algebra B →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁) {H₂ : Type u_2} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : N.algebra (L • B) →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₁ : GNS.IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : N.algebra B), (ω.comp (N.covEquiv L B).toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) (hcyc₂ : GNS.IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (b : N.algebra (L • B)), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) : IsFactor (GNS.gnsVonNeumann π₁) ↔ IsFactor (GNS.gnsVonNeumann π₂)

Factoriality is constant along the Lorentz orbit of a region. With the GNS data above, π₁(𝔘(B))'' is a factor exactly when π₂(𝔘(L·B))'' is. So the superselection type of a local state is a Lorentz-orbit invariant.