feat: gamma anticommutator and slash of Lorentz vector

Physlib/Relativity/CliffordAlgebra.lean

@@ -9,6 +9,8 @@ public import Mathlib.Analysis.Complex.Basic
 public import Mathlib.Data.Matrix.Reflection
 public import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
 public import Physlib.Meta.TODO.Basic
+public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic
+public import Physlib.Relativity.MinkowskiMatrix
 /-!
 # The Clifford Algebra
 
@@ -17,14 +19,18 @@ This file defines the Gamma matrices and their relationship to the Clifford alge
 ## Main Definitions
 
 - `γ0, γ1, γ2, γ3`: The four gamma matrices in the Dirac representation (4×4 complex matrices)
+- `γ`: The gamma matrices indexed by `Fin 1 ⊕ Fin 3`, matching the Minkowski index type
 - `γSet`: The set of gamma matrices
 - `diracForm`: The quadratic form with Minkowski signature (+,-,-,-)
   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
@@ -78,21 +84,24 @@ def γ5 : Matrix (Fin 4) (Fin 4) ℂ := I • (γ0 * γ1 * γ2 * γ3)
 
 /-- The γ gamma matrices in the Dirac representation. -/
 @[simp]
-def γ : Fin 4 → Matrix (Fin 4) (Fin 4) ℂ := ![γ0, γ1, γ2, γ3]
+def γ : Fin 1 ⊕ Fin 3 → Matrix (Fin 4) (Fin 4) ℂ
+  | Sum.inl _ => γ0
+  | Sum.inr 0 => γ1
+  | Sum.inr 1 => γ2
+  | Sum.inr 2 => γ3
 
 namespace γ
 
 open spaceTime
 
-variable (μ ν : Fin 4)
+variable (μ ν : Fin 1 ⊕ Fin 3)
 
 /-- The subset of `Matrix (Fin 4) (Fin 4) ℂ` formed by the gamma matrices in the Dirac
 representation. -/
 @[simp]
-def γSet : Set (Matrix (Fin 4) (Fin 4) ℂ) := {γ i | i : Fin 4}
+def γSet : Set (Matrix (Fin 4) (Fin 4) ℂ) := {γ i | i : Fin 1 ⊕ Fin 3}
 
-lemma γ_in_γSet (μ : Fin 4) : γ μ ∈ γSet := by
-  simp [γSet]
+lemma γ_in_γSet (μ : Fin 1 ⊕ Fin 3) : γ μ ∈ γSet := ⟨μ, rfl⟩
 
 /-- The algebra generated by the gamma matrices in the Dirac representation. -/
 def diracAlgebra : Subalgebra ℝ (Matrix (Fin 4) (Fin 4) ℂ) :=
@@ -101,9 +110,35 @@ def diracAlgebra : Subalgebra ℝ (Matrix (Fin 4) (Fin 4) ℂ) :=
 lemma γSet_subset_diracAlgebra : γSet ⊆ diracAlgebra :=
   Algebra.subset_adjoin
 
-lemma γ_in_diracAlgebra (μ : Fin 4) : γ μ ∈ diracAlgebra :=
+lemma γ_in_diracAlgebra (μ : Fin 1 ⊕ Fin 3) : γ μ ∈ diracAlgebra :=
   γSet_subset_diracAlgebra (γ_in_γSet μ)
 
+/-- The Clifford anticommutator identity for gamma matrices. -/
+theorem gamma_anticomm (μ ν : Fin 1 ⊕ Fin 3) :
+    γ μ * γ ν + γ ν * γ μ =
+      (2 * ((minkowskiMatrix μ ν : ℝ) : ℂ)) • (1 : Matrix (Fin 4) (Fin 4) ℂ) := by
+  cases μ with
+  | inl μ =>
+    fin_cases μ
+    cases ν with
+    | inl ν =>
+      fin_cases ν
+      simp [γ0_mul_γ0, minkowskiMatrix.inl_0_inl_0, two_smul]
+    | inr ν =>
+      fin_cases ν <;>
+        simp [γ1_mul_γ0, γ2_mul_γ0, γ3_mul_γ0, minkowskiMatrix.off_diag_zero]
+  | inr μ =>
+    cases ν with
+    | inl ν =>
+      fin_cases μ <;> fin_cases ν <;>
+        simp [γ1_mul_γ0, γ2_mul_γ0, γ3_mul_γ0, minkowskiMatrix.off_diag_zero]
+    | inr ν =>
+      fin_cases μ <;> fin_cases ν <;>
+        simp [γ1_mul_γ1, γ2_mul_γ2, γ3_mul_γ3,
+              γ2_mul_γ1, γ3_mul_γ1, γ3_mul_γ2,
+              minkowskiMatrix.inr_i_inr_i, minkowskiMatrix.off_diag_zero,
+              two_smul, neg_smul, neg_add_rev]
+
 /-- The quadratic form of the clifford algebra corresponding to the `γ` matrices. -/
 @[simps!]
 def diracForm : QuadraticForm ℝ (Fin 4 → ℝ) :=
@@ -116,44 +151,50 @@ def diracForm : QuadraticForm ℝ (Fin 4 → ℝ) :=
 `γ` matrices. -/
 def ofCliffordAlgebra : CliffordAlgebra diracForm →ₐ[ℝ] diracAlgebra :=
   CliffordAlgebra.lift _
-    ⟨∑ i, (LinearMap.proj i).smulRight ⟨γ i, γ_in_diracAlgebra _⟩, fun v => by
+    ⟨∑ i : Fin 4, (LinearMap.proj i).smulRight ⟨γ (finSumFinEquiv.symm i), γ_in_diracAlgebra _⟩,
+     fun v => by
       ext : 1
-      simp only [γ, Fin.sum_univ_four, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
-        Matrix.cons_val, LinearMap.add_apply, LinearMap.coe_smulRight, LinearMap.coe_proj,
+      have h0 : (finSumFinEquiv.symm (0 : Fin 4) : Fin 1 ⊕ Fin 3) = Sum.inl 0 := rfl
+      have h1 : (finSumFinEquiv.symm (1 : Fin 4) : Fin 1 ⊕ Fin 3) = Sum.inr 0 := rfl
+      have h2 : (finSumFinEquiv.symm (2 : Fin 4) : Fin 1 ⊕ Fin 3) = Sum.inr 1 := rfl
+      have h3 : (finSumFinEquiv.symm (3 : Fin 4) : Fin 1 ⊕ Fin 3) = Sum.inr 2 := rfl
+      simp only [Fin.sum_univ_four, Fin.isValue, h0, h1, h2, h3, γ,
+        LinearMap.add_apply, LinearMap.coe_smulRight, LinearMap.coe_proj,
         Function.eval, SetLike.mk_smul_mk, AddMemClass.mk_add_mk, MulMemClass.mk_mul_mk, mul_add,
         Algebra.mul_smul_comm, add_mul, Algebra.smul_mul_assoc, γ0_mul_γ0, γ1_mul_γ0, smul_neg,
         γ2_mul_γ0, γ3_mul_γ0, smul_add, γ1_mul_γ1, γ2_mul_γ1, γ3_mul_γ1, γ2_mul_γ2, γ3_mul_γ2,
         γ3_mul_γ3, diracForm_apply, Algebra.algebraMap_eq_smul_one, SetLike.val_smul,
         OneMemClass.coe_one]
       module⟩
 
-/-- The generators of the clifford algebra correspond to the elements `γ`. -/
+/-- The generator of the Clifford algebra corresponding to `γ i`. -/
 @[simp]
-lemma ofCliffordAlgebra_ι_single (i : Fin 4) (r : ℝ) :
-    ofCliffordAlgebra (CliffordAlgebra.ι _ (Pi.single i r)) = r • ⟨γ i, γ_in_diracAlgebra _⟩ :=
+lemma ofCliffordAlgebra_ι_single (i : Fin 1 ⊕ Fin 3) (r : ℝ) :
+    ofCliffordAlgebra (CliffordAlgebra.ι _ (Pi.single (finSumFinEquiv i) r)) =
+      r • ⟨γ i, γ_in_diracAlgebra _⟩ :=
   CliffordAlgebra.lift_ι_apply _ _ _ |>.trans <| Subtype.ext <| by
-    simp only [γ, LinearMap.coe_sum, LinearMap.coe_smulRight, LinearMap.coe_proj, Function.eval,
+    simp only [LinearMap.coe_sum, LinearMap.coe_smulRight, LinearMap.coe_proj, Function.eval,
       SetLike.mk_smul_mk, Finset.sum_apply, AddSubmonoidClass.coe_finsetSum]
-    rw [Finset.sum_eq_single i]
-    · simp
+    rw [Finset.sum_eq_single (finSumFinEquiv i)]
+    · simp [Equiv.symm_apply_apply]
     · intro b _ hb
       simp [Pi.single_eq_of_ne hb]
     · simp
 
 /-! ### Surjectivity of ofCliffordAlgebra -/
 
 /-- Each gamma matrix (as an element of diracAlgebra) is in the range of ofCliffordAlgebra. -/
-lemma γ_subtype_in_range (i : Fin 4) :
+lemma γ_subtype_in_range (i : Fin 1 ⊕ Fin 3) :
     ⟨γ i, γ_in_diracAlgebra i⟩ ∈ ofCliffordAlgebra.range := by
-  use CliffordAlgebra.ι diracForm (Pi.single i 1)
+  use CliffordAlgebra.ι diracForm (Pi.single (finSumFinEquiv i) 1)
   simp [ofCliffordAlgebra_ι_single]
 
 /-- Helper lemma: If a matrix is in Algebra.adjoin ℝ γSet, then its subtype is in the range. -/
 private lemma mem_adjoin_imp_subtype_in_range (m : Matrix (Fin 4) (Fin 4) ℂ)
     (hm : m ∈ Algebra.adjoin ℝ γSet) : ⟨m, hm⟩ ∈ ofCliffordAlgebra.range := by
   induction hm using Algebra.adjoin_induction with
   | mem y hy =>
-    -- y ∈ γSet, so y = γ i for some i
+    -- y ∈ γSet, so y = γ i for some i : Fin 1 ⊕ Fin 3
     obtain ⟨i, rfl⟩ := hy
     exact γ_subtype_in_range i
   | algebraMap r =>
@@ -191,6 +232,68 @@ theorem ofCliffordAlgebra_surjective : Function.Surjective ofCliffordAlgebra :=
   rw [← AlgHom.range_eq_top]
   exact ofCliffordAlgebra_range_eq_top
 
+/-! ### Dirac Slash Operators -/
+
+namespace Slash
+
+/-- The Dirac slash of a Lorentz vector. -/
+def slash (k : Lorentz.Vector) : Matrix (Fin 4) (Fin 4) ℂ :=
+  ∑ μ : Fin 1 ⊕ Fin 3, (k μ : ℂ) • γ μ
+/-- The notation for the Dirac slash operator, `k̸`. -/
+notation k "̸" => slash k
+
+/-- The componentwise complexification of a Lorentz vector in 1+3 dimensions. -/
+private def complex_vector (k : Lorentz.Vector) : Fin 1 ⊕ Fin 3 → ℂ :=
+  fun μ => (k μ : ℂ)
+
+@[simp]
+lemma slash_zero : slash (0 : Lorentz.Vector) = 0 := by
+  change (∑ μ : Fin 1 ⊕ Fin 3, complex_vector (0 : Lorentz.Vector) μ • γ μ) = 0
+  simp [complex_vector]
+
+@[simp]
+lemma slash_add (k l : Lorentz.Vector) : slash (k + l) = slash k + slash l := by
+  change (∑ μ : Fin 1 ⊕ Fin 3, complex_vector (k + l) μ • γ μ) =
+    (∑ μ : Fin 1 ⊕ Fin 3, complex_vector k μ • γ μ) +
+      (∑ μ : Fin 1 ⊕ Fin 3, complex_vector l μ • γ μ)
+  simp [complex_vector, add_smul, Finset.sum_add_distrib]
+
+@[simp]
+lemma slash_smul (c : ℝ) (k : Lorentz.Vector) : slash (c • k) = c • slash k := by
+  change (∑ μ : Fin 1 ⊕ Fin 3, complex_vector (c • k) μ • γ μ) =
+    c • (∑ μ : Fin 1 ⊕ Fin 3, complex_vector k μ • γ μ)
+  ext i j
+  fin_cases i <;> fin_cases j <;>
+    simp [complex_vector, Fintype.sum_sum_type, Fin.sum_univ_three] <;>
+    ring_nf
+
+/-- The Dirac slash as an `ℝ`-linear map. -/
+def slashLinear :
+    LinearMap (RingHom.id ℝ) Lorentz.Vector (Matrix (Fin 4) (Fin 4) ℂ) where
+  toFun := slash
+  map_add' := slash_add
+  map_smul' := slash_smul
+
+/-- Left multiplication by a slash matrix as a linear endomorphism. -/
+def slashMulLeft (k : Lorentz.Vector) :
+    LinearMap (RingHom.id ℂ) (Matrix (Fin 4) (Fin 4) ℂ) (Matrix (Fin 4) (Fin 4) ℂ) :=
+  LinearMap.mulLeft ℂ (slash k)
+
+/-- Product of list of slash factors, in left-to-right order. -/
+def slashProd (ks : List (Lorentz.Vector)) : Matrix (Fin 4) (Fin 4) ℂ :=
+  ((ks.map slashMulLeft).prod) 1
+
+@[simp]
+lemma slashProd_nil : slashProd [] = 1 := by
+  simp [slashProd]
+
+@[simp]
+lemma slashProd_cons (k : Lorentz.Vector) (ks : List (Lorentz.Vector)) :
+    slashProd (k :: ks) = slash k * slashProd ks := by
+  simp [slashProd, slashMulLeft]
+
+end Slash
+
 end γ
 
 end diracRepresentation