From d8e31f9b821fdf80abf5e6b58dcfa7dd86b4b8ee Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Thu, 18 Jun 2026 11:18:23 -0500 Subject: [PATCH 1/9] feat: gamma anticommutator and slash of Lorentz vector --- Physlib/Relativity/CliffordAlgebra.lean | 57 +++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/Physlib/Relativity/CliffordAlgebra.lean b/Physlib/Relativity/CliffordAlgebra.lean index f1029532c..8b202ef41 100644 --- a/Physlib/Relativity/CliffordAlgebra.lean +++ b/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 From 63fb1066316c13245994669334fc6d0e4a0e9380 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Fri, 19 Jun 2026 10:22:50 -0500 Subject: [PATCH 2/9] =?UTF-8?q?fix:=20def=20=CE=B3=20:=20Fin=201=20?= =?UTF-8?q?=E2=8A=95=20Fin=203;=20imports?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Physlib/Relativity/CliffordAlgebra.lean | 64 ++++++++++++++----------- 1 file changed, 36 insertions(+), 28 deletions(-) diff --git a/Physlib/Relativity/CliffordAlgebra.lean b/Physlib/Relativity/CliffordAlgebra.lean index 8b202ef41..bebf58d26 100644 --- a/Physlib/Relativity/CliffordAlgebra.lean +++ b/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,6 +19,7 @@ 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 @@ -81,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) ℂ) := @@ -104,11 +110,11 @@ 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 4) : +theorem gamma_anticomm (μ ν : Fin 1 ⊕ Fin 3) : γ μ * γ ν + γ ν * γ μ = (2 * ((minkowskiMatrix (finSumFinEquiv.symm μ) (finSumFinEquiv.symm ν) : ℝ) : ℂ)) • (1 : Matrix (Fin 4) (Fin 4) ℂ) := by @@ -127,10 +133,15 @@ 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, @@ -138,15 +149,16 @@ def ofCliffordAlgebra : CliffordAlgebra diracForm →ₐ[ℝ] diracAlgebra := 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 @@ -154,9 +166,9 @@ lemma ofCliffordAlgebra_ι_single (i : Fin 4) (r : ℝ) : /-! ### 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. -/ @@ -164,7 +176,7 @@ 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 => @@ -214,25 +226,21 @@ def coord (k : Lorentz.Vector 3) : Fin 4 → ℂ := /-- The Dirac slash of a Lorentz vector. -/ def slash (k : Lorentz.Vector 3) : Matrix (Fin 4) (Fin 4) ℂ := - ∑ μ, coord k μ • γ μ + ∑ μ : Fin 1 ⊕ Fin 3, 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 [slash, coord] @[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 [slash, coord, add_smul, Finset.sum_add_distrib] @[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] + fin_cases i <;> fin_cases j <;> + simp [slash, coord, Fintype.sum_sum_type, Fin.sum_univ_three] <;> ring_nf /-- Product of list of slash factors, in left-to-right order. -/ From 35cbc8dd8a5fad30152d3e6f8e2a94600c16e01b Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Fri, 19 Jun 2026 10:23:43 -0500 Subject: [PATCH 3/9] fix: def slash (k : Lorentz.Vector) --- Physlib/Relativity/CliffordAlgebra.lean | 36 ++++++++++++++----------- 1 file changed, 20 insertions(+), 16 deletions(-) diff --git a/Physlib/Relativity/CliffordAlgebra.lean b/Physlib/Relativity/CliffordAlgebra.lean index bebf58d26..c6f0ef8c4 100644 --- a/Physlib/Relativity/CliffordAlgebra.lean +++ b/Physlib/Relativity/CliffordAlgebra.lean @@ -218,40 +218,44 @@ theorem ofCliffordAlgebra_surjective : Function.Surjective ofCliffordAlgebra := 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) ℂ := - ∑ μ : Fin 1 ⊕ Fin 3, coord k μ • γ μ +def slash (k : Lorentz.Vector) : Matrix (Fin 4) (Fin 4) ℂ := + ∑ μ : Fin 1 ⊕ Fin 3, (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 3) = 0 := by - simp [slash, coord] +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 3) : slash (k + l) = slash k + slash l := by - simp [slash, coord, add_smul, Finset.sum_add_distrib] +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 3) : slash (c • k) = c • slash k := by +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 [slash, coord, Fintype.sum_sum_type, Fin.sum_univ_three] <;> + simp [complex_vector, Fintype.sum_sum_type, Fin.sum_univ_three] <;> 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) ℂ := +def slashProd (ks : List (Lorentz.Vector)) : 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)) : +lemma slashProd_cons (k : Lorentz.Vector) (ks : List (Lorentz.Vector)) : slashProd (k :: ks) = slash k * slashProd ks := rfl end Slash From 4c89feb76e4a2ece3e4d27828083672c91641b61 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Fri, 19 Jun 2026 12:04:30 -0500 Subject: [PATCH 4/9] =?UTF-8?q?fix:=20gamma=5Fanticomm=20proof=20by=20?= =?UTF-8?q?=CE=B30=5Fmul=5F=CE=B30=20etc=20reuse?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Physlib/Relativity/CliffordAlgebra.lean | 26 +++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/Physlib/Relativity/CliffordAlgebra.lean b/Physlib/Relativity/CliffordAlgebra.lean index c6f0ef8c4..8dfe0c3b4 100644 --- a/Physlib/Relativity/CliffordAlgebra.lean +++ b/Physlib/Relativity/CliffordAlgebra.lean @@ -116,10 +116,28 @@ lemma γ_in_diracAlgebra (μ : Fin 1 ⊕ Fin 3) : γ μ ∈ diracAlgebra := /-- The Clifford anticommutator identity for gamma matrices. -/ theorem gamma_anticomm (μ ν : Fin 1 ⊕ Fin 3) : γ μ * γ ν + γ ν * γ μ = - (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] + (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!] From f3ea91eeb62110d6544258cc2312f2686a0e692d Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Fri, 19 Jun 2026 12:06:18 -0500 Subject: [PATCH 5/9] =?UTF-8?q?feat:=20Dirac=20slash=20as=20an=20=E2=84=9D?= =?UTF-8?q?-linear=20map?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Physlib/Relativity/CliffordAlgebra.lean | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/Physlib/Relativity/CliffordAlgebra.lean b/Physlib/Relativity/CliffordAlgebra.lean index 8dfe0c3b4..efd0b95ec 100644 --- a/Physlib/Relativity/CliffordAlgebra.lean +++ b/Physlib/Relativity/CliffordAlgebra.lean @@ -265,16 +265,30 @@ lemma slash_smul (c : ℝ) (k : Lorentz.Vector) : slash (c • k) = c • slash 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 slash).prod + ((ks.map slashMulLeft).prod) 1 @[simp] -lemma slashProd_nil : slashProd [] = 1 := rfl +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 := rfl + slashProd (k :: ks) = slash k * slashProd ks := by + simp [slashProd, slashMulLeft] end Slash From 9eb177455277719c22a2791885f301966da26919 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Fri, 19 Jun 2026 12:10:19 -0500 Subject: [PATCH 6/9] feat: slash notation --- Physlib/Relativity/CliffordAlgebra.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Physlib/Relativity/CliffordAlgebra.lean b/Physlib/Relativity/CliffordAlgebra.lean index efd0b95ec..42d732adc 100644 --- a/Physlib/Relativity/CliffordAlgebra.lean +++ b/Physlib/Relativity/CliffordAlgebra.lean @@ -239,6 +239,7 @@ namespace Slash /-- The Dirac slash of a Lorentz vector. -/ def slash (k : Lorentz.Vector) : Matrix (Fin 4) (Fin 4) ℂ := ∑ μ : Fin 1 ⊕ Fin 3, (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 → ℂ := From 88e9ac257d7a1715c2bceb540dfbae5e76641329 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Fri, 19 Jun 2026 13:01:06 -0500 Subject: [PATCH 7/9] fix: docstring for notation --- Physlib/Relativity/CliffordAlgebra.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Physlib/Relativity/CliffordAlgebra.lean b/Physlib/Relativity/CliffordAlgebra.lean index 42d732adc..4aae93d83 100644 --- a/Physlib/Relativity/CliffordAlgebra.lean +++ b/Physlib/Relativity/CliffordAlgebra.lean @@ -239,6 +239,7 @@ 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. -/ From e022b0f6e7aa832c51206624e84c357018f2c350 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Sun, 21 Jun 2026 11:21:28 -0500 Subject: [PATCH 8/9] fix: use notation for linear map --- Physlib/Relativity/CliffordAlgebra.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Physlib/Relativity/CliffordAlgebra.lean b/Physlib/Relativity/CliffordAlgebra.lean index 4aae93d83..e0f4bacaa 100644 --- a/Physlib/Relativity/CliffordAlgebra.lean +++ b/Physlib/Relativity/CliffordAlgebra.lean @@ -268,15 +268,14 @@ lemma slash_smul (c : ℝ) (k : Lorentz.Vector) : slash (c • k) = c • slash ring_nf /-- The Dirac slash as an `ℝ`-linear map. -/ -def slashLinear : - LinearMap (RingHom.id ℝ) Lorentz.Vector (Matrix (Fin 4) (Fin 4) ℂ) where +def slashLinear : 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) ℂ) := + 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. -/ From ef272b9fc6571005919ea9ea6eedaa589969d328 Mon Sep 17 00:00:00 2001 From: Wouter Deconinck Date: Sun, 21 Jun 2026 11:23:36 -0500 Subject: [PATCH 9/9] fix: mv toComplexVector to Lorentz.Vector --- Physlib/Relativity/CliffordAlgebra.lean | 22 ++++++++----------- .../Tensors/RealTensor/Vector/Basic.lean | 4 ++++ 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Physlib/Relativity/CliffordAlgebra.lean b/Physlib/Relativity/CliffordAlgebra.lean index e0f4bacaa..61c0a1cda 100644 --- a/Physlib/Relativity/CliffordAlgebra.lean +++ b/Physlib/Relativity/CliffordAlgebra.lean @@ -242,29 +242,25 @@ def slash (k : Lorentz.Vector) : Matrix (Fin 4) (Fin 4) ℂ := /-- 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] + change (∑ μ : Fin 1 ⊕ Fin 3, Lorentz.Vector.toComplexVector (0 : Lorentz.Vector) μ • γ μ) = 0 + simp [Lorentz.Vector.toComplexVector] @[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] + change (∑ μ : Fin 1 ⊕ Fin 3, Lorentz.Vector.toComplexVector (k + l) μ • γ μ) = + (∑ μ : Fin 1 ⊕ Fin 3, Lorentz.Vector.toComplexVector k μ • γ μ) + + (∑ μ : Fin 1 ⊕ Fin 3, Lorentz.Vector.toComplexVector l μ • γ μ) + simp [Lorentz.Vector.toComplexVector, 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 μ • γ μ) + change (∑ μ : Fin 1 ⊕ Fin 3, Lorentz.Vector.toComplexVector (c • k) μ • γ μ) = + c • (∑ μ : Fin 1 ⊕ Fin 3, Lorentz.Vector.toComplexVector k μ • γ μ) ext i j fin_cases i <;> fin_cases j <;> - simp [complex_vector, Fintype.sum_sum_type, Fin.sum_univ_three] <;> + simp [Lorentz.Vector.toComplexVector, Fintype.sum_sum_type, Fin.sum_univ_three] <;> ring_nf /-- The Dirac slash as an `ℝ`-linear map. -/ diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean index e81e382d1..a79e2e397 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean @@ -160,6 +160,10 @@ lemma neg_apply {d : ℕ} (v : Vector d) (i : Fin 1 ⊕ Fin d) : lemma zero_apply {d : ℕ} (i : Fin 1 ⊕ Fin d) : (0 : Vector d) i = 0 := rfl +/-- The componentwise complexification of a Lorentz vector. -/ +def toComplexVector {d : ℕ} (k : Vector d) : Fin 1 ⊕ Fin d → ℂ := + fun μ => (k μ : ℂ) + /-- The continuous linear map from a Lorentz vector to one of its coordinates. -/ def coordCLM {d : ℕ} (i : Fin 1 ⊕ Fin d) : Vector d →L[ℝ] ℝ := LinearMap.toContinuousLinearMap { toFun v := v i