Axiom 5: Lorentz Covariance, the predicate #
This file states Axiom 5 (def:lorentz-covariance) for a local net and its Axiom 2
isotony family. The inhomogeneous Lorentz group and its action are in
Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean. The predicate sits after
Physicslib4/Spacetime/LorentzCausality.lean so that condition (3) can use
isAlexandrovBasisSet_smul: Lorentz transformations carry Alexandrov basis sets to basis
sets, so the isotony embedding between the images needs no extra hypothesis.
Axiom 5 (Lorentz covariance): the Poincaré group acts on the net, compatibly with isotony.
The axiom asks for a unital *-isomorphism α_L : 𝔘(B) → 𝔘(LB) for every element L of the identity
component of the Poincaré group (InhomogeneousLorentzGroup) and every region B, where LB is the
image of B under L, such that
- α_1 is the identity;
- α_(L'L) = α_L' ∘ α_L; and
- α_L commutes with isotony: α_L ∘ i(B₁, B₂) = i(LB₁, LB₂) ∘ α_L for diamonds B₁ ⊆ B₂, where i is the isotony family of Axiom 2.
In condition 3, LB₁ and LB₂ are diamonds with LB₁ ⊆ LB₂ because L preserves chronological
precedence (isAlexandrovBasisSet_smul, Set.smul_set_mono), so no further hypothesis is
needed. The predicate takes the isotony family as a parameter, so the action respects the net's own
embeddings.
HaagKastlerNet.covEquiv chooses the maps α_L, and HaagKastlerNet.action extends them to
automorphisms of the quasilocal algebra.
Implementation note: 𝔘(1B) and 𝔘(B), and 𝔘((L'L)B) and 𝔘(L'(LB)), are different types that are
equal only propositionally, so conditions 1 and 2 transport along those equalities (one_smul,
mul_smul) with Eq.mp.
Blueprint: def:lorentz-covariance
Equations
- One or more equations did not get rendered due to their size.