Physicslib4.AQFT.HaagKastler.LorentzCovariance

Axiom 5: Lorentz Covariance

This file formalises the blueprint declaration def:lorentz-covariance (Axiom 5 of the "sharpened" Haag-Kastler axioms, section 10.6 of the AQFT-in-Lean blueprint):

The inhomogeneous Lorentz group 𝓛 (more precisely, its identity component; see section 7.1 of the blueprint) acts on the assignment B ↦ 𝔘(B). For every L ∈ 𝓛, there is a *-isomorphism αL B : 𝔘(B) ≃⋆ₐ[ℂ] 𝔘(L·B) such that the action commutes with isotony, in the sense that for every inclusion B₁ ⊆ B₂ of basis sets the obvious diagram of inclusion arrows and αL-arrows commutes.

Main definitions

• Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup: the identity component of the inhomogeneous Lorentz group acting on Minkowski spacetime, modelled as the set of pairs (L, t) where L : V ≃ₗ[ℝ] V is a linear automorphism of the spacetime carrier V lying in SO(1,3)↑ (preserves the Minkowski form, has determinant 1, and preserves the future time direction) and t : V is a translation. The group operation is composition of the affine maps x ↦ L x + t.

• The Axiom 5 predicate Physicslib4.AQFT.HaagKastler.LorentzCovariance itself is in Physicslib4/AQFT/HaagKastler/LorentzCovarianceAxiom.lean, after Physicslib4/Spacetime/LorentzCausality.lean, which proves that the action preserves Alexandrov basis sets (isAlexandrovBasisSet_smul).

Supporting lemmas

• InhomogeneousLorentzGroup.timelike_separated_smul_iff, InhomogeneousLorentzGroup.spacelike_separated_smul_iff, InhomogeneousLorentzGroup.null_separated_smul_iff: Lorentz invariance of the sign of the Minkowski interval, one lemma per causal class.

Modelling notes

• The Lorentz-action data is given as: a group InhomogeneousLorentzGroup, a MulAction of that group on StandardMinkowskiSpacetime.Carrier, and, for each pair (L, B), a *-algebra equivalence αL B : U.algebra B ≃⋆ₐ[ℂ] U.algebra (L • B).

• "Commutes with isotony" is encoded by the commutativity of, for every B₁ ⊆ B₂ (basis sets) and every L, the square formed by the isotony arrow 𝔘(B₁) ↪ 𝔘(B₂) and the action arrows 𝔘(B₁) ≃ 𝔘(L·B₁) and 𝔘(B₂) ≃ 𝔘(L·B₂). The isotony arrows are those of Axiom 2: the predicate takes the Isotony family as a parameter, so the action is required to be equivariant for the net's own embeddings, not for a separately chosen family.

• The "linear" component is restricted to the orthochronous proper Lorentz subgroup SO(1,3)↑ of ℝ-linear automorphisms of StandardMinkowskiSpacetime.Carrier: those preserving the Minkowski form, with determinant +1, and preserving the future time direction. Closure of the orthochronous condition under composition and inversion is provided by Physicslib4.isOrthochronous_trans and Physicslib4.isOrthochronous_symm in Spacetime/Minkowski.lean, proved via the reverse Cauchy-Schwarz inequality on the Minkowski form.

structure Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup : Type

The identity component of the Poincaré group, the symmetry group of Axiom 5.

An element is a pair (Λ, a) of a proper orthochronous Lorentz transformation Λ ∈ SO(1,3)↑ and a translation a, acting on Minkowski spacetime by x ↦ Λx + a. The product is the composition of these affine maps, (Λ₁, a₁)(Λ₂, a₂) = (Λ₁Λ₂, a₁ + Λ₁a₂). Haag and Kastler call the Poincaré group the inhomogeneous Lorentz group. Space and time reflections are not included: a theory need not be invariant under them (the weak interaction violates parity), and time reversal would act antilinearly.

The group carries the topology induced by its embedding g ↦ (Λ, Λ⁻¹, a) into a space of bounded operators and vectors, and is a topological group.

Blueprint: def:inhomogeneous-lorentz-group

• linear : StandardMinkowskiSpacetime.Carrier ≃ₗ[ℝ] StandardMinkowskiSpacetime.Carrier

  The Lorentz transformation Λ, a real-linear automorphism of spacetime.

• translation : StandardMinkowskiSpacetime.Carrier

  The translation a.

• isLorentz : IsLorentz self.linear

  Λ preserves the Minkowski form.

• isProper : IsProper self.linear

  Λ is proper: its determinant is 1.

• isOrthochronous : IsOrthochronous self.linear

  Λ is orthochronous: it preserves the direction of time, (Λe₀)⁰ > 0 for the unit time vector e₀.

theorem Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.ext {a b : InhomogeneousLorentzGroup} (hL : a.linear = b.linear) (ht : a.translation = b.translation) : a = b

theorem Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.ext_iff {a b : InhomogeneousLorentzGroup} : a = b ↔ a.linear = b.linear ∧ a.translation = b.translation

@[instance_reducible]

noncomputable instance Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.instGroup : Group InhomogeneousLorentzGroup

Group structure on the inhomogeneous Lorentz group: the product (L₁, t₁) * (L₂, t₂) = (L₁ ∘ L₂, t₁ + L₁ t₂) is the composition of the affine maps x ↦ Lᵢ x + tᵢ.

Equations

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

Topological group structure

The inhomogeneous Lorentz group is topologized as a subspace of the operator-norm space (Carrier →L Carrier)² × Carrier, recording each element as its linear part, the inverse of its linear part, and its translation. Carrying the inverse linear part as a separate coordinate makes group inversion a continuous coordinate operation (a swap plus an application), so no continuity of operator inversion is needed.

noncomputable def Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.toProd (g : InhomogeneousLorentzGroup) : (StandardMinkowskiSpacetime.Carrier →L[ℝ] StandardMinkowskiSpacetime.Carrier) × (StandardMinkowskiSpacetime.Carrier →L[ℝ] StandardMinkowskiSpacetime.Carrier) × StandardMinkowskiSpacetime.Carrier

The faithful coordinate embedding used to topologize the inhomogeneous Lorentz group: g ↦ (g.linear, g.linear⁻¹, g.translation) inside the operator-norm space.

Equations

• g.toProd = (LinearMap.toContinuousLinearMap ↑g.linear, LinearMap.toContinuousLinearMap ↑g.linear.symm, g.translation)

@[instance_reducible]

noncomputable instance Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.instTopologicalSpace : TopologicalSpace InhomogeneousLorentzGroup

The topology on the inhomogeneous Lorentz group, induced by the coordinate embedding toProd into the operator-norm space.

Equations

• Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.instTopologicalSpace = TopologicalSpace.induced Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.toProd inferInstance

theorem Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.continuous_toProd : Continuous toProd

theorem Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.toProd_mul (a b : InhomogeneousLorentzGroup) : (a * b).toProd = (a.toProd.1 ∘SL b.toProd.1, b.toProd.2.1 ∘SL a.toProd.2.1, a.toProd.2.2 + a.toProd.1 b.toProd.2.2)

The embedding decomposes multiplication: the linear part composes, the inverse linear part composes in reverse, and the translation is the affine combination.

theorem Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.toProd_inv (a : InhomogeneousLorentzGroup) : a⁻¹.toProd = (a.toProd.2.1, a.toProd.1, -a.toProd.2.1 a.toProd.2.2)

The embedding decomposes inversion: swap the two linear coordinates and negate the back-transported translation.

instance Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.instContinuousMul : ContinuousMul InhomogeneousLorentzGroup

instance Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.instContinuousInv : ContinuousInv InhomogeneousLorentzGroup

instance Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.instIsTopologicalGroup : IsTopologicalGroup InhomogeneousLorentzGroup

@[instance_reducible]

noncomputable instance Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.instMulActionCarrierStandardMinkowskiSpacetime : MulAction InhomogeneousLorentzGroup StandardMinkowskiSpacetime.Carrier

The MulAction of the inhomogeneous Lorentz group on the Minkowski spacetime carrier: (L, t) • x = L x + t.

Equations

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

theorem Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.smul_sub_smul (g : InhomogeneousLorentzGroup) (x y : StandardMinkowskiSpacetime.Carrier) : g • x - g • y = g.linear (x - y)

The translation part of the action cancels on differences: the displacement between two points is transformed by the linear part alone.

theorem Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.minkowskiForm_smul_sub_smul (g : InhomogeneousLorentzGroup) (x y z w : StandardMinkowskiSpacetime.Carrier) : (minkowskiForm (g • x - g • y)) (g • z - g • w) = (minkowskiForm (x - y)) (z - w)

The inhomogeneous Lorentz group acts by isometries of the Minkowski form. Since the translation part cancels on differences and the linear part is Lorentz, the Minkowski inner product of displacements is preserved.

theorem Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.minkowskiForm_smul_sub_self (g : InhomogeneousLorentzGroup) (x y : StandardMinkowskiSpacetime.Carrier) : (minkowskiForm (g • x - g • y)) (g • x - g • y) = (minkowskiForm (x - y)) (x - y)

The Minkowski interval between two events is invariant under the inhomogeneous Lorentz group: ‖g • x - g • y‖²_M = ‖x - y‖²_M. This is the diagonal case of minkowskiForm_smul_sub_smul.

theorem Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.timelike_separated_smul_iff (g : InhomogeneousLorentzGroup) (x y : StandardMinkowskiSpacetime.Carrier) : (minkowskiForm (g • x - g • y)) (g • x - g • y) < 0 ↔ (minkowskiForm (x - y)) (x - y) < 0

The action preserves timelike separation: g • x and g • y are timelike-separated (negative Minkowski interval) iff x and y are.

theorem Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.spacelike_separated_smul_iff (g : InhomogeneousLorentzGroup) (x y : StandardMinkowskiSpacetime.Carrier) : 0 < (minkowskiForm (g • x - g • y)) (g • x - g • y) ↔ 0 < (minkowskiForm (x - y)) (x - y)

The action preserves spacelike separation: g • x and g • y are spacelike-separated (positive Minkowski interval) iff x and y are.

theorem Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup.null_separated_smul_iff (g : InhomogeneousLorentzGroup) (x y : StandardMinkowskiSpacetime.Carrier) : (minkowskiForm (g • x - g • y)) (g • x - g • y) = 0 ↔ (minkowskiForm (x - y)) (x - y) = 0

The action preserves null separation: g • x and g • y are null-separated (zero Minkowski interval) iff x and y are.