Generators of the Lorentz Algebra

This file defines the 6 standard generators of the Lorentz algebra so(1,3) :

• Boost generators K₀, K₁, K₂: Generate Lorentz transformations (velocity changes)
• Rotation generators J₀, J₁, J₂: Generate spatial rotations

These generators form a basis for the 6-dimensional Lie algebra so(1,3), though the full basis structure (linear independence and spanning) is not yet proven here.

Physical Interpretation

• boostGenerator i: Infinitesimal boost in the i-th spatial direction. Exponentiating this generator produces finite Lorentz boosts.
• rotationGenerator i: Infinitesimal rotation about the i-th axis following the right-hand rule. Exponentiating this generator produces spatial rotations.

Mathematical Structure

Each generator satisfies the Lorentz algebra condition: Aᵀ η = -η A, where η is the Minkowski metric with signature (+,-,-,-).

The boost generators are symmetric matrices with non-zero entries only in the time-space block, while rotation generators are antisymmetric matrices acting only on spatial indices.

References

• Weinberg, The Quantum Theory of Fields, Vol 1, Section 2.7
• Peskin & Schroeder, An Introduction to QFT, Appendix A

Future Work

TODO "6VZKA" can be completed by proving linear independence and spanning of these 6 generators, then constructing a formal Basis (Fin 2 × Fin 3) ℝ lorentzAlgebra.

def lorentzAlgebra.boostGenerator (i : Fin 3) : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ

The boost generator K_i in the Lorentz algebra so(1,3).

This matrix generates infinitesimal Lorentz boosts in the i-th spatial direction. The matrix has non-zero entries only at positions (0, i+1) and (i+1, 0) with value 1, where we use the index convention 0 = time, 1,2,3 = space.

Properties

• Symmetric: K_iᵀ = K_i
• Traceless: tr(K_i) = 0
• Satisfies Lorentz algebra condition: K_iᵀ η = -η K_i

Physical Meaning

Exponentiating β·K_i produces a finite Lorentz boost with rapidity β in direction i.

Equations

• lorentzAlgebra.boostGenerator i μ ν = if μ = Sum.inl 0 ∧ ν = Sum.inr i ∨ μ = Sum.inr i ∧ ν = Sum.inl 0 then 1 else 0

def lorentzAlgebra.rotationGenerator (i : Fin 3) : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ

The rotation generator J_i in the Lorentz algebra so(1,3).

This matrix generates infinitesimal rotations about the i-th axis following the right-hand rule. The matrix acts only on spatial indices in the antisymmetric pattern characteristic of angular momentum generators.

Properties

• Antisymmetric: J_iᵀ = -J_i
• Traceless: tr(J_i) = 0
• Satisfies Lorentz algebra condition: J_iᵀ η = -η J_i

Structure

• J_0 (rotation about x-axis) : Acts on (y,z) components
• J_1 (rotation about y-axis) : Acts on (z,x) components
• J_2 (rotation about z-axis) : Acts on (x,y) components

Physical Meaning

Exponentiating θ·J_i produces a finite rotation by angle θ about axis i.

Equations

• lorentzAlgebra.rotationGenerator 0 μ ν = if μ = Sum.inr 1 ∧ ν = Sum.inr 2 then -1 else if μ = Sum.inr 2 ∧ ν = Sum.inr 1 then 1 else 0
• lorentzAlgebra.rotationGenerator 1 μ ν = if μ = Sum.inr 0 ∧ ν = Sum.inr 2 then 1 else if μ = Sum.inr 2 ∧ ν = Sum.inr 0 then -1 else 0
• lorentzAlgebra.rotationGenerator 2 μ ν = if μ = Sum.inr 0 ∧ ν = Sum.inr 1 then -1 else if μ = Sum.inr 1 ∧ ν = Sum.inr 0 then 1 else 0

theorem lorentzAlgebra.boostGenerator_mem (i : Fin 3) : boostGenerator i ∈ lorentzAlgebra

The boost generator K_i is in the Lorentz algebra.

theorem lorentzAlgebra.rotationGenerator_mem (i : Fin 3) : rotationGenerator i ∈ lorentzAlgebra

The rotation generator J_i is in the Lorentz algebra.

TODO: Properties of Generators

The following properties are documented in the docstrings but not yet formally proven. These should be established in future PRs to complete the characterization of the generators.