Axiom 5: Lorentz Covariance

This file formalises the blueprint declaration def:lorentz-covariance (Axiom 5 of the "sharpened" Haag-Kastler axioms, section 10.3 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.

• Physicslib4.AQFT.HaagKastler.LorentzCovariance: a Prop-valued predicate on a LocalNet asserting Axiom 5.

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₂). Because the isotony arrows are existentially quantified (see Isotony), we quantify over them: the predicate asks that some choice of isotony arrows makes the action equivariant.

• 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 inhomogeneous Lorentz group acting on Minkowski spacetime, as the set of pairs (L, t) where L is an ℝ-linear automorphism of the spacetime carrier lying in SO(1,3)↑ (Lorentz, proper, orthochronous) and t is a translation vector. The group law is composition of the affine maps x ↦ L x + t.

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

  The "Lorentz part": an ℝ-linear automorphism of the Minkowski spacetime carrier.

• translation : StandardMinkowskiSpacetime.Carrier

  The translation part: a vector in the spacetime carrier.

• isLorentz : IsLorentz self.linear

  The linear part preserves the Minkowski form.

• isProper : IsProper self.linear

  The linear part is proper (determinant 1).

• isOrthochronous : IsOrthochronous self.linear

  The linear part is orthochronous (preserves the direction of time).

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

@[implicit_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)

@[implicit_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

@[implicit_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.

def Physicslib4.AQFT.HaagKastler.LorentzCovariance (U : LocalNet) : Prop

Axiom 5 (Lorentz Covariance). A local net U is Lorentz covariant if the inhomogeneous Lorentz group acts on the assignment B ↦ U.algebra B and the action

(1) sends the identity element of the Lorentz group to the identity automorphism, (2) is multiplicative in the group element, i.e. α (L' · L) = α L' ∘ α L, and (3) commutes with isotony.

Concretely, there exist:

• for every group element L : InhomogeneousLorentzGroup and every Alexandrov-basis set B, a *-algebra equivalence α L B : U.algebra B ≃⋆ₐ[ℂ] U.algebra (L • B);
• for every inclusion B₁ ⊆ B₂ of basis sets, a choice of isotony-witness unital *-monomorphism ι B₁ B₂ : U.algebra B₁ →⋆ₐ[ℂ] U.algebra B₂;

such that

(1) [identity] for every basis set B and every a : U.algebra B, α 1 B a = a (modulo the canonical identification U.algebra (1 • B) = U.algebra B coming from one_smul);

(2) [composition] for every pair L, L' : InhomogeneousLorentzGroup, every basis set B and every a : U.algebra B, α (L' * L) B a = α L' (L • B) (α L B a) (modulo the canonical identification U.algebra ((L' * L) • B) = U.algebra (L' • (L • B)) coming from mul_smul); and

(3) [isotony] for every L, every inclusion B₁ ⊆ B₂, and every element a : U.algebra B₁, the action of L commutes with the isotony inclusion: α L B₂ (ι B₁ B₂ a) = ι' (L • B₁) (L • B₂) (α L B₁ a), where ι' is the isotony-witness arrow for L • B₁ ⊆ L • B₂ (which holds because L • _ preserves set inclusions).

The cross-fiber identifications in conditions (1) and (2) are implemented as Eq.mpr of the obvious congruence U.algebra _ = U.algebra _ produced from one_smul/mul_smul.

Blueprint reference: def:lorentz-covariance.

Equations

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