Purity of states on curved local algebras

The local algebra 𝔘(B) of a Haag-Kastler net in curved spacetime is a unital C*-algebra, so the abstract characterizations of purity of a state apply to it verbatim. This file registers them for 𝔘(B):

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

There is no quasilocal algebra in curved spacetime, so these statements are phrased per region, on each local algebra 𝔘(B) separately - which is exactly the right generality, since each 𝔘(B) is itself a C*-algebra with its own state space and GNS representations.

Main results

• Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.pure_iff_extreme
• Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_pure_iff_irreducible

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.pure_iff_extreme {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} (ω : GNS.State (N.algebra B)) : GNS.IsPure ω ↔ ω.IsExtremePoint

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

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_pure_iff_irreducible {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} (ω : GNS.State (N.algebra B)) : ∃ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H), GNS.IsCyclicVector π Ω ∧ (∀ (a : N.algebra B), ω a = inner ℂ Ω ((π a) Ω)) ∧ (GNS.IsPure ω ↔ GNS.IsIrreducible π)

Pure ⟺ irreducible GNS representation for a curved local algebra. For a state ω on the local algebra 𝔘(B), 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.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_factor_of_isPure {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} {ω : GNS.State (N.algebra B)} (hpure : GNS.IsPure ω) : ∃ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H), GNS.IsCyclicVector π Ω ∧ (∀ (a : N.algebra B), ω a = inner ℂ Ω ((π a) Ω)) ∧ GNS.gnsVonNeumann π ∩ (GNS.gnsVonNeumann π).centralizer = {T : H →L[ℂ] H | ∃ (c : ℂ), T = c • 1}

The GNS representation of a pure state on a curved local algebra is a factor. For a pure state ω on 𝔘(B) there is a cyclic GNS triple reproducing ω whose generated von Neumann algebra π(𝔘(B))'' has trivial center (its center equals the scalars). The abstract GNS.exists_gns_factor_of_isPure at the C*-algebra 𝔘(B).

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_generates_all_of_isPure {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} {ω : GNS.State (N.algebra B)} (hpure : GNS.IsPure ω) : ∃ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H), GNS.IsCyclicVector π Ω ∧ (∀ (a : N.algebra B), ω a = inner ℂ Ω ((π a) Ω)) ∧ GNS.gnsVonNeumann π = Set.univ

The GNS representation of a pure state on a curved local algebra generates 𝓑(H). For a pure state ω on 𝔘(B) there is a cyclic GNS triple reproducing ω whose generated von Neumann algebra is all of 𝓑(H): π(𝔘(B))'' = 𝓑(H). The abstract GNS.exists_gns_generates_all_of_isPure at the C*-algebra 𝔘(B).

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.areDisjoint_or_unitaryEquiv_of_isIrreducible {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} {H₁ : Type u_1} {H₂ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : N.algebra B →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : N.algebra B →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} (h1 : GNS.IsIrreducible π₁) (h2 : GNS.IsIrreducible π₂) : GNS.AreDisjoint π₁ π₂ ∨ GNS.UnitaryEquiv π₁ π₂

The irreducible dichotomy for curved local algebras. Two irreducible representations of a curved local algebra 𝔘(B) are either disjoint or unitarily equivalent. The abstract GNS.areDisjoint_or_unitaryEquiv_of_isIrreducible at the C*-algebra 𝔘(B).

GNS covariance for the local algebras

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.unitaryEquiv_gns_covEquiv {M : LorentzianSpacetime} (N : HaagKastlerNet M) (φ : M.Isom) (B : Set M.Carrier) (ω : GNS.State (N.algebra (φ • 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 (φ • B) →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₁ : GNS.IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : N.algebra B), (ω.comp (N.covEquiv φ B).toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) (hcyc₂ : GNS.IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (b : N.algebra (φ • B)), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) : GNS.UnitaryEquiv π₁ (π₂.comp (N.covEquiv φ B).toStarAlgHom)

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

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isIrreducible_iff_gns_covEquiv {M : LorentzianSpacetime} (N : HaagKastlerNet M) (φ : M.Isom) (B : Set M.Carrier) (ω : GNS.State (N.algebra (φ • 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 (φ • B) →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₁ : GNS.IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : N.algebra B), (ω.comp (N.covEquiv φ B).toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) (hcyc₂ : GNS.IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (b : N.algebra (φ • B)), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) : GNS.IsIrreducible π₁ ↔ GNS.IsIrreducible π₂

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

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isFactor_iff_gns_covEquiv {M : LorentzianSpacetime} (N : HaagKastlerNet M) (φ : M.Isom) (B : Set M.Carrier) (ω : GNS.State (N.algebra (φ • 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 (φ • B) →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₁ : GNS.IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : N.algebra B), (ω.comp (N.covEquiv φ B).toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) (hcyc₂ : GNS.IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (b : N.algebra (φ • B)), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) : IsFactor (GNS.gnsVonNeumann π₁) ↔ IsFactor (GNS.gnsVonNeumann π₂)

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