Axiom 5 (Isometric Covariance), curved spacetime

This file formalises the blueprint declaration def:isometric-covariance-in-curved-spacetime (Axiom 5 of the Haag-Kastler axioms on a Lorentzian spacetime, Chapter 10 (sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime) of the AQFT-in-Lean blueprint):

A member φ of the group of isometries of M connected to the identity acts on 𝔘(𝐁) via a unital *-isomorphism α_φ : 𝔘(𝐁) → 𝔘(φ(𝐁)), where φ(𝐁) is the image of the basis set. The action satisfies (1) α_𝟙 = id, (2) α_{φ'·φ} = α_{φ'} ∘ α_φ, and (3) it commutes with the isotony monomorphism i (Axiom 2).

Main definitions

• Physicslib4.AQFT.HaagKastlerCurved.IsometricCovariance: a Prop-valued predicate on a LocalNet M asserting Axiom 5.

Modelling notes

• The Minkowski analogue (LorentzCovariance) uses the identity component of the inhomogeneous Lorentz group. Here the analogous role is played by the abstract group M.Isom of isometries connected to the identity, acting on M.Carrier; the induced pointwise action on Set M.Carrier (φ • B = φ(B)) supplies the blueprint's φ(𝐁).

• Conditions (1) and (2) carry cross-fiber identifications U.algebra (1 • B) = U.algebra B and U.algebra ((φ'·φ) • B) = U.algebra (φ' • (φ • B)) coming from one_smul/mul_smul, implemented as Eq.mpr/congrArg. This matches the Minkowski LorentzCovariance encoding verbatim.

def Physicslib4.AQFT.HaagKastlerCurved.IsometricCovariance {M : LorentzianSpacetime} (U : LocalNet M) : Prop

Axiom 5 (Isometric Covariance), curved spacetime. A local net U on a Lorentzian spacetime M is isometrically covariant if the group M.Isom of identity-component isometries acts on the assignment B ↦ U.algebra B and the action

(1) sends the identity isometry to the identity automorphism, (2) is multiplicative in the group element, α (φ' · φ) = α φ' ∘ α φ, and (3) commutes with isotony.

Concretely, there exist:

• for every isometry φ : M.Isom and every Alexandrov-basis set B, a *-algebra equivalence α φ B : U.algebra B ≃⋆ₐ[ℂ] U.algebra (φ • B);
• for every inclusion B₁ ⊆ B₂ of basis sets, a choice of isotony *-monomorphism ι B₁ B₂ : U.algebra B₁ →⋆ₐ[ℂ] U.algebra B₂;

such that (1) α 1 B a = a, (2) α (φ' * φ) B a = α φ' (φ • B) (α φ B a), and (3) for every φ and inclusion B₁ ⊆ B₂, the action commutes with the isotony inclusion.

Blueprint reference: def:isometric-covariance-in-curved-spacetime.

Equations

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