Physicslib4.AQFT.HaagKastler.CovariantState

Covariant families of local states

This file defines covariant families of local states on a Haag-Kastler net over Minkowski spacetime. The Lorentz action on the net is implemented fiberwise by the covariance equivalences α_L : 𝔘(B) ≃⋆ₐ[ℂ] 𝔘(L·B) (HaagKastlerNet.covEquiv, from Axiom 5). A covariant family of local states is a choice of state ω B on each local algebra 𝔘(B) that is intertwined by these equivalences.

Main definitions

• Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsCovariantFamily: a family ω : ∀ B, State 𝔘(B) is covariant if ω B a = ω (L·B) (α_L a) for every Lorentz transformation L, region B, and a ∈ 𝔘(B).

Main results

• IsCovariantFamily.one: at the identity, covariance reduces to the canonical identification 𝔘(B) = 𝔘(1·B) (via covEquiv_one).
• IsCovariantFamily.comp: covariance composes - chaining through L then L' expresses ω B via the state on L'·(L·B).

Notes

This is the local, fiberwise form of covariance. Lifting the fiberwise action to an automorphism group of the quasilocal algebra 𝔘 is carried out in QuasilocalIntertwiner.lean (QuasilocalLift, HaagKastlerNet.action), which gives Lorentz-invariant states a single invariant state on 𝔘. A genuine vacuum state requires, beyond invariance, the spectrum condition (energy positivity); it is formalised in VacuumState.lean through AQFT.IsPositiveEnergy.

def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsCovariantFamily (N : HaagKastlerNet) (ω : (B : Set StandardMinkowskiSpacetime.Carrier) → GNS.State (N.algebra B)) : Prop

A covariant family of local states assigns to every region B a state ω B on the local algebra 𝔘(B) such that the state on B is the pullback of the state on the Lorentz translate L·B along the covariance equivalence: ω B a = ω (L·B) (α_L a) for all L, B, and a ∈ 𝔘(B).

Equations

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

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsCovariantFamily.one (N : HaagKastlerNet) {ω : (B : Set StandardMinkowskiSpacetime.Carrier) → GNS.State (N.algebra B)} (hω : N.IsCovariantFamily ω) (B : Set StandardMinkowskiSpacetime.Carrier) (a : N.algebra B) : (ω B) a = (ω (1 • B)) (⋯.mp a)

Covariance at the identity. For a covariant family, the state on B agrees with the state on 1·B transported along the canonical identification 𝔘(B) = 𝔘(1·B) (from one_smul).

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsCovariantFamily.comp (N : HaagKastlerNet) {ω : (B : Set StandardMinkowskiSpacetime.Carrier) → GNS.State (N.algebra B)} (hω : N.IsCovariantFamily ω) (L L' : InhomogeneousLorentzGroup) (B : Set StandardMinkowskiSpacetime.Carrier) (a : N.algebra B) : (ω B) a = (ω (L' • L • B)) ((N.covEquiv L' (L • B)) ((N.covEquiv L B) a))

Covariance composes. Chaining covariance through L and then L' expresses the state on B via the state on L'·(L·B) and the composed equivalences.