Merge pull request #344 from HEPLean/Rebrand

feat: Properties of Pauli matrices

PhysLean.lean

@@ -60,18 +60,16 @@ import PhysLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
 import PhysLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
 import PhysLean.Lorentz.Algebra.Basic
 import PhysLean.Lorentz.Algebra.Basis
+import PhysLean.Lorentz.Bispinors.Basic
 import PhysLean.Lorentz.ComplexTensor.Basic
 import PhysLean.Lorentz.ComplexTensor.Basis
-import PhysLean.Lorentz.ComplexTensor.Bispinors.Basic
 import PhysLean.Lorentz.ComplexTensor.Lemmas
 import PhysLean.Lorentz.ComplexTensor.Metrics.Basic
 import PhysLean.Lorentz.ComplexTensor.Metrics.Basis
 import PhysLean.Lorentz.ComplexTensor.Metrics.Lemmas
 import PhysLean.Lorentz.ComplexTensor.OfRat
-import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basic
-import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basis
-import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Relations
 import PhysLean.Lorentz.ComplexTensor.Units.Basic
+import PhysLean.Lorentz.ComplexTensor.Units.Basis
 import PhysLean.Lorentz.ComplexTensor.Units.Symm
 import PhysLean.Lorentz.ComplexVector.Basic
 import PhysLean.Lorentz.ComplexVector.Contraction
@@ -88,6 +86,9 @@ import PhysLean.Lorentz.Group.Rotations
 import PhysLean.Lorentz.MinkowskiMatrix
 import PhysLean.Lorentz.PauliMatrices.AsTensor
 import PhysLean.Lorentz.PauliMatrices.Basic
+import PhysLean.Lorentz.PauliMatrices.Basis
+import PhysLean.Lorentz.PauliMatrices.Matrix
+import PhysLean.Lorentz.PauliMatrices.Relations
 import PhysLean.Lorentz.PauliMatrices.SelfAdjoint
 import PhysLean.Lorentz.RealVector.Basic
 import PhysLean.Lorentz.RealVector.Contraction

PhysLean/Lorentz/ComplexTensor/Bispinors/Basic.lean → PhysLean/Lorentz/Bispinors/Basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basic
+import PhysLean.Lorentz.PauliMatrices.Basic
 /-!
 
 ## Bispinors
@@ -24,7 +24,7 @@ open Fermion
 noncomputable section
 namespace complexLorentzTensor
 open Lorentz
-
+open PauliMatrix
 /-!
 
 ## Definitions
@@ -33,7 +33,8 @@ open Lorentz
 
 TODO "To increase the speed of these files `(vecNodeE complexLorentzTensor .up p).tensor | μ` is
   written out expliclity. Notation should be introduced so that we can just write `p | μ` or
-  similar without slowing things down."
+  similar without slowing things down.
+  This can be done by redefining bispinors in terms of actual tensors. "
 
 /-- A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`. -/
 def contrBispinorUp (p : complexContr) :=
@@ -115,87 +116,5 @@ lemma coBispinorDown_expand (p : complexCo) :
   rw [tensorNode_coBispinorDown p]
   rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_coBispinorUp p]
 
-set_option maxRecDepth 5000 in
-lemma contrBispinorDown_eq_pauliCoDown_contr (p : complexContr) :
-    {contrBispinorDown p | α β = pauliCoDown | μ α β ⊗
-    (vecNodeE complexLorentzTensor .up p).tensor | μ}ᵀ := by
-  conv =>
-    rhs
-    rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <|
-      pauliCoDown_eq_metric_mul_pauliCo]
-    rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_left _ _ _ _]
-    rw [perm_tensor_eq <| perm_contr_congr 2 2]
-    rw [perm_perm]
-    rw [perm_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _]
-    rw [perm_tensor_eq <| perm_contr_congr 2 2]
-    rw [perm_perm]
-    apply (perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_eq_id _ rfl _).trans
-    rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _]
-    rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr_congr 1 3]
-    rw [perm_tensor_eq <| perm_contr_congr 2 2]
-    rw [perm_perm]
-    erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <|
-      perm_eq_id _ rfl _]
-    rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <|
-      prod_assoc' _ _ _ _ _ _]
-    rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_contr_congr 0 4]
-    rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr_congr 1 3]
-    rw [perm_tensor_eq <| perm_contr_congr 2 2]
-    rw [perm_perm]
-  conv =>
-    lhs
-    rw [contrBispinorDown_expand p]
-    rw [contr_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _]
-    rw [contr_tensor_eq <| perm_contr_congr 0 3]
-    rw [perm_contr_congr 1 2]
-    apply (perm_tensor_eq <| contr_tensor_eq <| contr_contr _ _ _).trans
-    rw [perm_tensor_eq <| perm_contr _ _]
-    rw [perm_perm]
-    rw [perm_tensor_eq <| contr_contr _ _ _]
-    rw [perm_perm]
-  apply perm_congr _ rfl
-  decide
-
-set_option maxRecDepth 5000 in
-lemma coBispinorDown_eq_pauliContrDown_contr (p : complexCo) :
-    {coBispinorDown p | α β = pauliContrDown | μ α β ⊗
-    (vecNodeE complexLorentzTensor .down p).tensor | μ}ᵀ := by
-  conv =>
-    rhs
-    rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <|
-      pauliContrDown_eq_metric_mul_pauliContr]
-    rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_left _ _ _ _]
-    rw [perm_tensor_eq <| perm_contr_congr 2 2]
-    rw [perm_perm]
-    rw [perm_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _]
-    rw [perm_tensor_eq <| perm_contr_congr 2 2]
-    rw [perm_perm]
-    apply (perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_eq_id _ rfl _).trans
-    rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _]
-    rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr_congr 1 3]
-    rw [perm_tensor_eq <| perm_contr_congr 2 2]
-    rw [perm_perm]
-    erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <|
-      perm_eq_id _ rfl _]
-    rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <|
-      prod_assoc' _ _ _ _ _ _]
-    rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_contr_congr 0 4]
-    rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr_congr 1 3]
-    rw [perm_tensor_eq <| perm_contr_congr 2 2]
-    rw [perm_perm]
-  conv =>
-    lhs
-    rw [coBispinorDown_expand p]
-    rw [contr_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _]
-    rw [contr_tensor_eq <| perm_contr_congr 0 3]
-    rw [perm_contr_congr 1 2]
-    apply (perm_tensor_eq <| contr_tensor_eq <| contr_contr _ _ _).trans
-    rw [perm_tensor_eq <| perm_contr _ _]
-    rw [perm_perm]
-    rw [perm_tensor_eq <| contr_contr _ _ _]
-    rw [perm_perm]
-  apply perm_congr _ rfl
-  decide
-
 end complexLorentzTensor
 end

PhysLean/Lorentz/ComplexTensor/Basis.lean

@@ -13,9 +13,8 @@ import PhysLean.Meta.TODO.Basic
 
 ## Basis vectors associated with complex Lorentz tensors
 
-Note that this file will be much improved once:
-  https://github.com/leanprover-community/mathlib4/pull/11156
-is merged.
+The material in this file should slowly be replaced with
+tensorBasis.
 
 -/
 open IndexNotation