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