Einstein causality in curved spacetime

This is the curved-spacetime counterpart of Minkowski Einstein causality. There is no quasilocal algebra in curved spacetime, so local commutativity is phrased inside a common containing basis algebra 𝔘(B): if B₁, B₂ are completely spacelike and both contained in B, then the images of 𝔘(B₁) and 𝔘(B₂) in 𝔘(B) commute. This file pushes that into Hilbert space: under any *-representation π of the containing algebra 𝔘(B) - in particular the GNS representation of any state on 𝔘(B) - the spacelike-separated local observables commute as bounded operators.

Main results

• Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.einstein_causality: causality in any representation of the containing algebra.
• Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_einstein_causality: the GNS specialization.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.einstein_causality {M : LorentzianSpacetime} (N : HaagKastlerNet M) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {B : Set M.Carrier} (hB : M.IsBasisSet B) (π : N.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set M.Carrier⦄ (hB₁ : M.IsBasisSet B₁) (hB₂ : M.IsBasisSet B₂) (hs : M.IsCompletelySpacelike B₁ B₂) (h₁ : B₁ ⊆ B) (h₂ : B₂ ⊆ B) (a : N.algebra B₁) (b : N.algebra B₂) : Commute (π ((N.commIsotony hB₁ hB h₁) a)) (π ((N.commIsotony hB₂ hB h₂) b))

Einstein causality in a representation (curved spacetime). For any *-representation π of a containing basis algebra 𝔘(B), the images of the local observables of two completely spacelike-separated subregions B₁, B₂ ⊆ B commute as bounded operators. This is Commute.map applied to the curved local commutativity commute_of_spacelike.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_einstein_causality {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} (hB : M.IsBasisSet B) (ω : 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) Ω)) ∧ ∀ ⦃B₁ B₂ : Set M.Carrier⦄ (hB₁ : M.IsBasisSet B₁) (hB₂ : M.IsBasisSet B₂), M.IsCompletelySpacelike B₁ B₂ → ∀ (h₁ : B₁ ⊆ B) (h₂ : B₂ ⊆ B) (a : N.algebra B₁) (b : N.algebra B₂), Commute (π ((N.commIsotony hB₁ hB h₁) a)) (π ((N.commIsotony hB₂ hB h₂) b))

Einstein causality on a GNS Hilbert space (curved spacetime). For any state ω on a containing basis algebra 𝔘(B) there is a GNS triple (H, π, Ω) reproducing ω in which the local observables of completely spacelike-separated subregions commute as operators on H.