Covariant families of local states, curved spacetime

This file mirrors Physicslib4.AQFT.HaagKastler.CovariantState for a Haag-Kastler net over an abstract Lorentzian spacetime M. The identity-component isometry action on the net is implemented fiberwise by the covariance equivalences α_φ : 𝔘(B) ≃⋆ₐ[ℂ] 𝔘(φ·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.HaagKastlerCurved.HaagKastlerNet.IsCovariantFamily: a family ω : ∀ B, State 𝔘(B) is covariant if ω B a = ω (φ·B) (α_φ a) for every isometry φ, 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 φ then φ' expresses ω B via the state on φ'·(φ·B).

Notes

As in the Minkowski case, this is the local, fiberwise form of covariance. Lifting the fiberwise action to an automorphism group is realized per region by the stabilizer action stabAut (StabilizerAction.lean): for g fixing B, α_g is an automorphism of the single algebra 𝔘(B). Since curved spacetime has no quasilocal algebra, there is no global isometry-invariant vacuum; equilibrium is instead captured by KMS states for Killing flows (StabilizerKMS.lean).

def Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsCovariantFamily {M : LorentzianSpacetime} (N : HaagKastlerNet M) (ω : (B : Set M.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 isometric image φ·B along the covariance equivalence: ω B a = ω (φ·B) (α_φ a) for all φ, B, and a ∈ 𝔘(B).

Equations

• N.IsCovariantFamily ω = ∀ (φ : M.Isom) (B : Set M.Carrier) (a : N.algebra B), (ω B) a = (ω (φ • B)) ((N.covEquiv φ B) a)

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsCovariantFamily.one {M : LorentzianSpacetime} (N : HaagKastlerNet M) {ω : (B : Set M.Carrier) → GNS.State (N.algebra B)} (hω : N.IsCovariantFamily ω) (B : Set M.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.HaagKastlerCurved.HaagKastlerNet.IsCovariantFamily.comp {M : LorentzianSpacetime} (N : HaagKastlerNet M) {ω : (B : Set M.Carrier) → GNS.State (N.algebra B)} (hω : N.IsCovariantFamily ω) (φ φ' : M.Isom) (B : Set M.Carrier) (a : N.algebra B) : (ω B) a = (ω (φ' • φ • B)) ((N.covEquiv φ' (φ • B)) ((N.covEquiv φ B) a))

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

def Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsWeaklyContinuousAction {M : LorentzianSpacetime} (N : HaagKastlerNet M) [TopologicalSpace M.Isom] (O B : Set M.Carrier) (ω : GNS.State (N.algebra B)) (incl : (φ : M.Isom) → M.IsBasisSet (φ • O) → φ • O ⊆ B → N.algebra (φ • O) →⋆ₐ[ℂ] N.algebra B) : Prop

Fiberwise weak continuity of the covariance action (state-relative), curved spacetime. Mirror of Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsWeaklyContinuousAction.

Continuity is measured relative to a state ω on the algebra of a containing region B. A fixed observable a ∈ 𝔘(B) is compared against the isometry-transported observable α_φ b of a b ∈ 𝔘(O) from a sub-region O. Since α_φ b lives in the different algebra 𝔘(φ·O), it is embedded back into 𝔘(B) along a supplied isotony inclusion incl (explicit data, not the existential isotony witness). The family is weakly continuous if for all a, b the matrix coefficient φ ↦ ω(a⋆ · ι_{φ·O ⊆ B}(α_φ b)) is continuous on the subspace of isometries keeping φ·O a basis set inside B.

Because the abstract LorentzianSpacetime interface equips M.Isom with only a group and an action - no topology - the topology required to state continuity enters as an explicit [TopologicalSpace M.Isom] instance argument rather than as a field on the interface. The definition is otherwise identical to the Minkowski one and uses no quasilocal algebra, confirming that the fiberwise form ports cleanly to curved spacetime.

Equations

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