KMS states for a Killing flow in curved spacetime

This file connects the abstract KMS condition (Physicslib4.AQFT.IsKMSState) to the curved-spacetime stabilizer action. A Killing flow fixing a region B is a one-parameter subgroup t ↦ φ_t of the stabilizer Stab(B) = {φ : φ·B = B}. It induces, via the stabilizer automorphism stabAutHom, a one-parameter group of *-automorphisms of the single local algebra 𝔘(B), and one can then ask whether a state on 𝔘(B) is KMS for that flow.

This is the setting of the curved-spacetime thermal states discussed alongside the stabilizer GNS unitary: the Hartle-Hawking state on a Schwarzschild exterior (KMS for the stationary Killing flow at the Hawking temperature) and the Bunch-Davies state restricted to a de Sitter static patch (KMS for the boost Killing flow at the Gibbons-Hawking temperature).

Main definitions / results

• HaagKastlerNet.flowAut: the one-parameter automorphism family of 𝔘(B) induced by a flow into Stab(B).
• HaagKastlerNet.isOneParameterAut_flowAut: if the flow is a one-parameter subgroup, the induced family is a one-parameter automorphism group.
• HaagKastlerNet.IsKMSStateForFlow: a state on 𝔘(B) is a KMS state for the Killing flow.

noncomputable def Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.flowAut {M : LorentzianSpacetime} (N : HaagKastlerNet M) (B : Set M.Carrier) (flow : ℝ → ↥(MulAction.stabilizer M.Isom B)) (t : ℝ) : N.algebra B ≃⋆ₐ[ℂ] N.algebra B

The one-parameter automorphism family of the local algebra 𝔘(B) induced by a flow t ↦ φ_t into the stabilizer Stab(B), via the stabilizer automorphism stabAutHom.

Equations

• N.flowAut B flow t = N.stabAutHom B (flow t)

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isOneParameterAut_flowAut {M : LorentzianSpacetime} (N : HaagKastlerNet M) (B : Set M.Carrier) (flow : ℝ → ↥(MulAction.stabilizer M.Isom B)) (h0 : flow 0 = 1) (hadd : ∀ (s t : ℝ), flow (s + t) = flow s * flow t) : IsOneParameterAut (N.flowAut B flow)

A Killing flow induces a one-parameter automorphism group. If flow is a one-parameter subgroup of Stab(B) (flow 0 = 1, flow (s+t) = flow s * flow t), then the induced automorphisms of 𝔘(B) form a one-parameter group.

def Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsKMSStateForFlow {M : LorentzianSpacetime} (N : HaagKastlerNet M) (B : Set M.Carrier) (flow : ℝ → ↥(MulAction.stabilizer M.Isom B)) (β : ℝ) (ω : GNS.State (N.algebra B)) : Prop

A state ω on the local algebra 𝔘(B) is a KMS state for the Killing flow flow at inverse temperature β if it satisfies the KMS condition for the induced one-parameter automorphism group flowAut.

Equations

• N.IsKMSStateForFlow B flow β ω = Physicslib4.AQFT.IsKMSState (N.flowAut B flow) β ω

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsKMSStateForFlow.exists_gns_unitary_strongContinuous {M : LorentzianSpacetime} (N : HaagKastlerNet M) (B : Set M.Carrier) (flow : ℝ → ↥(MulAction.stabilizer M.Isom B)) (h0 : flow 0 = 1) (hadd : ∀ (s t : ℝ), flow (s + t) = flow s * flow t) {β : ℝ} (hβ : 0 < β) {ω : GNS.State (N.algebra B)} (hkms : N.IsKMSStateForFlow B flow β ω) (hwc : ∀ (a b : N.algebra B), Continuous fun (t : ℝ) => ω (star a * (N.flowAut B flow t) b)) : ∃ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) (U : ℝ → H ≃ₗᵢ[ℂ] H), (∀ (a : N.algebra B), ω a = inner ℂ Ω ((π a) Ω)) ∧ (∀ (t : ℝ) (a : N.algebra B), (U t) ((π a) Ω) = (π ((N.flowAut B flow t) a)) Ω) ∧ (∀ (t : ℝ), (U t) Ω = Ω) ∧ U 0 = LinearIsometryEquiv.refl ℂ H ∧ (∀ (s t : ℝ), U (s + t) = (U t).trans (U s)) ∧ ∀ (ψ : H), Continuous fun (t : ℝ) => (U t) ψ

The Killing-flow KMS thermal representation. A KMS state ω on 𝔘(B) for a one-parameter Killing flow t ↦ φ_t into Stab(B), at positive inverse temperature β, yields a GNS triple (H, π, Ω) reproducing ω together with a strongly continuous one-parameter unitary group U : ℝ → (H ≃ₗᵢ[ℂ] H) implementing the flow: U t (π a Ω) = π (α_t a) Ω, U t Ω = Ω, U 0 = id, U (s+t) = U s ∘ U t, and t ↦ U t ψ is continuous for every ψ.

This is the curved-spacetime equilibrium (thermal) representation - the role played by the vacuum representation in Minkowski spacetime - for states such as the Hartle-Hawking and Gibbons-Hawking states. The hypotheses are: flow is a one-parameter subgroup of Stab(B), 0 < β, the KMS condition, and weak continuity of the matrix coefficients t ↦ ω(a⋆ · α_t b). KMS at β > 0 gives α-invariance (IsKMSState.invariant_of_pos), which feeds the abstract strongly-continuous GNS unitary construction.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsKMSStateForFlow.convexCombo {M : LorentzianSpacetime} (N : HaagKastlerNet M) (B : Set M.Carrier) (flow : ℝ → ↥(MulAction.stabilizer M.Isom B)) {β : ℝ} {ω₁ ω₂ : GNS.State (N.algebra B)} (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (h₁ : N.IsKMSStateForFlow B flow β ω₁) (h₂ : N.IsKMSStateForFlow B flow β ω₂) : N.IsKMSStateForFlow B flow β (ω₁.convexCombo ω₂ s hs0 hs1)

The Killing-flow KMS state set is convex. A convex combination s·ω₁ + (1-s)·ω₂ (0 ≤ s ≤ 1) of two KMS states on 𝔘(B) for the same Killing flow at the same inverse temperature β is again a KMS state for that flow. This specializes the abstract KMS convexity (AQFT.IsKMSState.convexCombo) to the induced one-parameter group flowAut. Physically the curved-spacetime thermal equilibrium states for a stationary Killing flow form a convex set.

def Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsGroundStateForFlow {M : LorentzianSpacetime} (N : HaagKastlerNet M) (B : Set M.Carrier) (flow : ℝ → ↥(MulAction.stabilizer M.Isom B)) (ω : GNS.State (N.algebra B)) : Prop

Ground state for a Killing flow (bounded-generator scaffold). A state ω on 𝔘(B) is a ground state for a one-parameter Killing flow t ↦ φ_t into Stab(B) when it is invariant under the flow and, in a GNS representation (K, π, Ω) reproducing ω and implementing the flow by unitaries U (fixing Ω), the one-parameter unitary group t ↦ U t has positive energy (AQFT.IsPositiveEnergy). This is the ground-state (β → ∞, spectrum-condition) counterpart of IsKMSStateForFlow: it selects the stationary state whose Killing-flow generator (the local "Hamiltonian") is positive. The positive-energy condition is the bounded-generator scaffold; the faithful unbounded form is Stone-gated.

Equations

• One or more equations did not get rendered due to their size.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsGroundStateForFlow.invariant {M : LorentzianSpacetime} (N : HaagKastlerNet M) (B : Set M.Carrier) (flow : ℝ → ↥(MulAction.stabilizer M.Isom B)) {ω : GNS.State (N.algebra B)} (h : N.IsGroundStateForFlow B flow ω) (t : ℝ) (a : N.algebra B) : ω ((N.flowAut B flow t) a) = ω a

A Killing-flow ground state is invariant under the flow (the first conjunct); no spectrum condition or Stone's theorem is needed.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsGroundStateForFlow.exists_strongContinuous_unitary {M : LorentzianSpacetime} (N : HaagKastlerNet M) (B : Set M.Carrier) (flow : ℝ → ↥(MulAction.stabilizer M.Isom B)) {ω : GNS.State (N.algebra B)} (h : N.IsGroundStateForFlow B flow ω) : ∃ (K : Type) (x : NormedAddCommGroup K) (x_1 : InnerProductSpace ℂ K) (x_2 : CompleteSpace K) (π : N.algebra B →⋆ₐ[ℂ] K →L[ℂ] K) (Ω : K) (U : ℝ → K ≃ₗᵢ[ℂ] K), (∀ (a : N.algebra B), ω a = inner ℂ Ω ((π a) Ω)) ∧ (∀ (t : ℝ) (a : N.algebra B), (U t) ((π a) Ω) = (π ((N.flowAut B flow t) a)) Ω) ∧ (∀ (t : ℝ), (U t) Ω = Ω) ∧ ∀ (ψ : K), Continuous fun (t : ℝ) => (U t) ψ

The implementing unitary group of a Killing-flow ground state is strongly continuous, since it has positive energy (AQFT.IsPositiveEnergy.strongContinuous). This needs no spectrum condition.