feat: gamma anticommutator and slash of Lorentz vector

Physlib/Relativity/CliffordAlgebra.lean

@@ -22,9 +22,12 @@ This file defines the Gamma matrices and their relationship to the Clifford alge
   corresponding to the gamma matrices
 - `diracAlgebra`: The algebra generated by the gamma matrices over ℝ
 - `ofCliffordAlgebra`: The algebra homomorphism from the Clifford algebra to `diracAlgebra`
+- `slash`: The Dirac slash operator on Lorentz vectors
+- `slashProd`: The product of a list of Dirac slash operators on Lorentz vectors
 
 ## Main Results
 
+- `gamma_anticomm`: The Clifford anticommutator for gamma matrices
 - `ofCliffordAlgebra_surjective`: The homomorphism `ofCliffordAlgebra` is surjective
 
 ## TODO
@@ -104,6 +107,14 @@ lemma γSet_subset_diracAlgebra : γSet ⊆ diracAlgebra :=
 lemma γ_in_diracAlgebra (μ : Fin 4) : γ μ ∈ diracAlgebra :=
   γSet_subset_diracAlgebra (γ_in_γSet μ)
 
+/-- The Clifford anticommutator identity for gamma matrices. -/
+theorem gamma_anticomm (μ ν : Fin 4) :
+    γ μ * γ ν + γ ν * γ μ =
+      (2 * ((minkowskiMatrix (finSumFinEquiv.symm μ) (finSumFinEquiv.symm ν) : ℝ) : ℂ)) •
+        (1 : Matrix (Fin 4) (Fin 4) ℂ) := by
+  fin_cases μ <;> fin_cases ν <;>
+    simp [γ, γ0, γ1, γ2, γ3, Matrix.one_fin_four]
+
 /-- The quadratic form of the clifford algebra corresponding to the `γ` matrices. -/
 @[simps!]
 def diracForm : QuadraticForm ℝ (Fin 4 → ℝ) :=
@@ -191,6 +202,52 @@ theorem ofCliffordAlgebra_surjective : Function.Surjective ofCliffordAlgebra :=
   rw [← AlgHom.range_eq_top]
   exact ofCliffordAlgebra_range_eq_top
 
+/-! ### Dirac Slash Operators -/
+
+namespace Slash
+
+/-- Components of a Lorentz vector in the `γ0,γ1,γ2,γ3` ordering.
+
+Required cast since Lorentz.Vector is Fin 1 ⊕ Fin d → ℝ, not Fin 4 → ℂ. -/
+def coord (k : Lorentz.Vector 3) : Fin 4 → ℂ :=
+  ![(k (Sum.inl 0) : ℂ), (k (Sum.inr 0) : ℂ), (k (Sum.inr 1) : ℂ), (k (Sum.inr 2) : ℂ)]
+
+/-- The Dirac slash of a Lorentz vector. -/
+def slash (k : Lorentz.Vector 3) : Matrix (Fin 4) (Fin 4) ℂ :=
+  ∑ μ, coord k μ • γ μ
+
+@[simp]
+lemma slash_zero : slash (0 : Lorentz.Vector 3) = 0 := by
+  ext i j
+  fin_cases i <;> fin_cases j <;> simp [slash, coord, Fin.sum_univ_four]
+
+@[simp]
+lemma slash_add (k l : Lorentz.Vector 3) : slash (k + l) = slash k + slash l := by
+  ext i j
+  fin_cases i <;> fin_cases j
+  · simp [slash, coord, Fin.sum_univ_four]
+    ring_nf
+
+@[simp]
+lemma slash_smul (c : ℝ) (k : Lorentz.Vector 3) : slash (c • k) = c • slash k := by
+  ext i j
+  fin_cases i <;> fin_cases j
+  · simp [slash, coord, Fin.sum_univ_four, mul_assoc]
+    ring_nf
+
+/-- Product of list of slash factors, in left-to-right order. -/
+def slashProd (ks : List (Lorentz.Vector 3)) : Matrix (Fin 4) (Fin 4) ℂ :=
+  (ks.map slash).prod
+
+@[simp]
+lemma slashProd_nil : slashProd [] = 1 := rfl
+
+@[simp]
+lemma slashProd_cons (k : Lorentz.Vector 3) (ks : List (Lorentz.Vector 3)) :
+    slashProd (k :: ks) = slash k * slashProd ks := rfl
+
+end Slash
+
 end γ
 
 end diracRepresentation