Physicslib4.AQFT.HaagKastler.QuasilocalKMS

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

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

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

The automorphisms t ↦ β_(L_t) of the quasilocal algebra along a curve t ↦ L_t of Poincaré transformations.

Here β_L is the action HaagKastlerNet.action of L on 𝔘. When t ↦ L_t is a one-parameter subgroup, for instance the time translations, this is a one-parameter group of automorphisms, the dynamics of the theory (isOneParameterAut_flowAut).

Blueprint: def:flow-aut-covariance

Equations

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

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isOneParameterAut_flowAut (N : HaagKastlerNet) (flow : ℝ → InhomogeneousLorentzGroup) (h0 : flow 0 = 1) (hadd : ∀ (s t : ℝ), flow (s + t) = flow s * flow t) : IsOneParameterAut (N.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.HaagKastlerNet.IsKMSStateForFlow (N : HaagKastlerNet) (flow : ℝ → InhomogeneousLorentzGroup) (β : ℝ) (ω : GNS.State N.quasilocal.carrier) : Prop

A state ω on the quasilocal algebra is a KMS state at inverse temperature β for a flow t ↦ L_t.

As you will recall, the Kubo–Martin–Schwinger condition characterises thermal equilibrium: for all a, b the correlation function t ↦ ω(a τ_t(b)) extends to a bounded continuous function on the strip 0 ≤ Im z ≤ β, holomorphic inside, whose values on Im z = β are ω(τ_t(b) a). This definition is the general KMS condition AQFT.IsKMSState for the automorphisms τ_t = β_(L_t) of 𝔘 (flowAut). In Minkowski spacetime every Poincaré transformation acts on the single algebra 𝔘, so any one-parameter subgroup may serve as the dynamics.

Blueprint: def:kms-state-for-flow-covariance

Equations

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

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsKMSStateForFlow.convexCombo (N : HaagKastlerNet) (flow : ℝ → InhomogeneousLorentzGroup) {β : ℝ} {ω₁ ω₂ : GNS.State N.quasilocal.carrier} (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (h₁ : N.IsKMSStateForFlow flow β ω₁) (h₂ : N.IsKMSStateForFlow flow β ω₂) : N.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.HaagKastlerNet.IsGroundStateForFlow (N : HaagKastlerNet) (flow : ℝ → InhomogeneousLorentzGroup) (ω : GNS.State N.quasilocal.carrier) : Prop

A ground state for a flow t ↦ L_t: a flow-invariant state in which the flow has a positive generator.

A state ω on the quasilocal algebra is a ground state for t ↦ L_t when

1. ω(β_(L_t) a) = ω(a) for all t and a; and
2. there is a representation (K, π, Ω) reproducing ω, with unitaries U(t) that fix Ω and implement the flow, U(t)π(a)Ω = π(β_(L_t) a)Ω, such that t ↦ U(t) has positive energy (AQFT.IsPositiveEnergy): it is strongly continuous with positive generator.

For a timelike translation the generator is the Hamiltonian. The ground state is the zero-temperature counterpart of the KMS states of IsKMSStateForFlow.

Blueprint: def:ground-state-for-flow-covariance

Equations

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

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsGroundStateForFlow.invariant (N : HaagKastlerNet) (flow : ℝ → InhomogeneousLorentzGroup) {ω : GNS.State N.quasilocal.carrier} (h : N.IsGroundStateForFlow flow ω) (t : ℝ) (a : N.quasilocal.carrier) : ω ((N.flowAut flow t) a) = ω a

A covariance-flow ground state is invariant under the flow (the first conjunct); the spectrum condition is not used.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsGroundStateForFlow.exists_strongContinuous_unitary (N : HaagKastlerNet) (flow : ℝ → InhomogeneousLorentzGroup) {ω : GNS.State N.quasilocal.carrier} (h : N.IsGroundStateForFlow flow ω) : ∃ (K : Type u) (x : NormedAddCommGroup K) (x_1 : InnerProductSpace ℂ K) (x_2 : CompleteSpace K) (π : N.quasilocal.carrier →⋆ₐ[ℂ] K →L[ℂ] K) (Ω : K) (U : ℝ → K ≃ₗᵢ[ℂ] K), (∀ (a : N.quasilocal.carrier), ω a = inner ℂ Ω ((π a) Ω)) ∧ (∀ (t : ℝ) (a : N.quasilocal.carrier), (U t) ((π a) Ω) = (π ((N.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: strong continuity is a field of the positive-energy hypothesis (AQFT.IsPositiveEnergy.strongContinuous).