KMS states for the covariance action in Minkowski spacetime

This file connects the abstract KMS condition (Physicslib4.AQFT.IsKMSState) to the Minkowski covariance action on the quasilocal algebra. A one-parameter subgroup t ↦ L_t of the inhomogeneous Lorentz group - for instance the time-translation subgroup whose modular/Hamiltonian flow defines time evolution - induces, via the quasilocal lift β_L, a one-parameter group of *-automorphisms of the global quasilocal algebra 𝔘. One can then ask whether a state on 𝔘 is KMS for that flow.

Unlike the curved-spacetime case, where the absence of a global quasilocal algebra forces a restriction to the stabilizer subgroup Stab(B), here the lift β_L is a genuine automorphism of the single global algebra 𝔘 for every L, so no stabilizer restriction is needed.

Main definitions / results

• CovariantQuasilocalAlgebra.flowAut: the one-parameter automorphism family of 𝔘 induced by a one-parameter subgroup of the inhomogeneous Lorentz group.
• CovariantQuasilocalAlgebra.isOneParameterAut_flowAut: a one-parameter subgroup induces a one-parameter automorphism group.
• CovariantQuasilocalAlgebra.IsKMSStateForFlow: a state on 𝔘 is a KMS state for the covariance flow.
• CovariantQuasilocalAlgebra.IsKMSStateForFlow.convexCombo: the KMS state set for the covariance flow is convex.

noncomputable def Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.flowAut (C : CovariantQuasilocalAlgebra) (flow : ℝ → InhomogeneousLorentzGroup) (t : ℝ) : C.quasilocal.carrier ≃⋆ₐ[ℂ] C.quasilocal.carrier

The one-parameter automorphism family of the quasilocal algebra 𝔘 induced by a one-parameter subgroup t ↦ L_t of the inhomogeneous Lorentz group, via the covariance action β_L.

Equations

• C.flowAut flow t = C.action (flow t)

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.isOneParameterAut_flowAut (C : CovariantQuasilocalAlgebra) (flow : ℝ → InhomogeneousLorentzGroup) (h0 : flow 0 = 1) (hadd : ∀ (s t : ℝ), flow (s + t) = flow s * flow t) : IsOneParameterAut (C.flowAut flow)

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

def Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.IsKMSStateForFlow (C : CovariantQuasilocalAlgebra) (flow : ℝ → InhomogeneousLorentzGroup) (β : ℝ) (ω : GNS.State C.quasilocal.carrier) : Prop

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

Equations

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

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.IsKMSStateForFlow.convexCombo (C : CovariantQuasilocalAlgebra) (flow : ℝ → InhomogeneousLorentzGroup) {β : ℝ} {ω₁ ω₂ : GNS.State C.quasilocal.carrier} (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (h₁ : C.IsKMSStateForFlow flow β ω₁) (h₂ : C.IsKMSStateForFlow flow β ω₂) : C.IsKMSStateForFlow flow β (ω₁.convexCombo ω₂ s hs0 hs1)

The covariance-flow KMS state set is convex. A convex combination s·ω₁ + (1-s)·ω₂ (0 ≤ s ≤ 1) of two KMS states on 𝔘 for the same covariance 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 equilibrium states for a one-parameter symmetry flow form a convex set.

def Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.IsGroundStateForFlow (C : CovariantQuasilocalAlgebra) (flow : ℝ → InhomogeneousLorentzGroup) (ω : GNS.State C.quasilocal.carrier) : Prop

Ground state for a covariance flow (bounded-generator scaffold). A state ω on the quasilocal algebra 𝔘 is a ground state for a one-parameter subgroup t ↦ L_t of the inhomogeneous Lorentz group (e.g. a translation or boost flow) 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: the stationary state whose flow generator (the Hamiltonian, for a timelike flow) 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.HaagKastler.CovariantQuasilocalAlgebra.IsGroundStateForFlow.invariant (C : CovariantQuasilocalAlgebra) (flow : ℝ → InhomogeneousLorentzGroup) {ω : GNS.State C.quasilocal.carrier} (h : C.IsGroundStateForFlow flow ω) (t : ℝ) (a : C.quasilocal.carrier) : ω ((C.flowAut flow t) a) = ω a

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

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.IsGroundStateForFlow.exists_strongContinuous_unitary (C : CovariantQuasilocalAlgebra) (flow : ℝ → InhomogeneousLorentzGroup) {ω : GNS.State C.quasilocal.carrier} (h : C.IsGroundStateForFlow flow ω) : ∃ (K : Type) (x : NormedAddCommGroup K) (x_1 : InnerProductSpace ℂ K) (x_2 : CompleteSpace K) (π : C.quasilocal.carrier →⋆ₐ[ℂ] K →L[ℂ] K) (Ω : K) (U : ℝ → K ≃ₗᵢ[ℂ] K), (∀ (a : C.quasilocal.carrier), ω a = inner ℂ Ω ((π a) Ω)) ∧ (∀ (t : ℝ) (a : C.quasilocal.carrier), (U t) ((π a) Ω) = (π ((C.flowAut flow t) a)) Ω) ∧ (∀ (t : ℝ), (U t) Ω = Ω) ∧ ∀ (ψ : K), Continuous fun (t : ℝ) => (U t) ψ

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