From 865164ca81b61d5884103a308858c4fbb1d01de4 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 23 Oct 2024 08:01:23 +0000
Subject: [PATCH] feat: Add contr of basis

---
 .../LorentzVector/Complex/Basic.lean          | 26 +++++++---
 .../LorentzVector/Complex/Contraction.lean    | 22 ++++++++
 HepLean/SpaceTime/WeylFermion/Basic.lean      | 24 +++++++++
 .../SpaceTime/WeylFermion/Contraction.lean    | 40 ++++++++++++++
 HepLean/Tensors/ComplexLorentz/Basic.lean     | 15 ++++++
 HepLean/Tensors/ComplexLorentz/Basis.lean     | 52 +++++++++++++++++++
 6 files changed, 173 insertions(+), 6 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean b/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
index 77e7b9c..20cf861 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
+++ b/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
@@ -40,9 +40,12 @@ def complexCo : Rep ℂ SL(2, ℂ) := Rep.of CoℂModule.SL2CRep
 def complexContrBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexContr := Basis.ofEquivFun
   (Equiv.linearEquiv ℂ ContrℂModule.toFin13ℂFun)
 
-/-- The standard basis of complex contravariant Lorentz vectors indexed by `Fin 4`. -/
-def complexContrBasisFin4 : Basis (Fin 4) ℂ complexContr :=
-  Basis.reindex complexContrBasis finSumFinEquiv
+@[simp]
+lemma complexContrBasis_toFin13ℂ (i :Fin 1 ⊕ Fin 3) :
+    (complexContrBasis i).toFin13ℂ = Pi.single i 1 := by
+  simp only [complexContrBasis, Basis.coe_ofEquivFun]
+  rw [Lorentz.ContrℂModule.toFin13ℂ]
+  rfl
 
 @[simp]
 lemma complexContrBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
@@ -58,13 +61,19 @@ lemma complexContrBasis_ρ_val (M : SL(2,ℂ)) (v : complexContr) :
     LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ v.val := by
   rfl
 
+/-- The standard basis of complex contravariant Lorentz vectors indexed by `Fin 4`. -/
+def complexContrBasisFin4 : Basis (Fin 4) ℂ complexContr :=
+  Basis.reindex complexContrBasis finSumFinEquiv
+
 /-- The standard basis of complex covariant Lorentz vectors. -/
 def complexCoBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexCo := Basis.ofEquivFun
   (Equiv.linearEquiv ℂ CoℂModule.toFin13ℂFun)
 
-/-- The standard basis of complex covariant Lorentz vectors indexed by `Fin 4`. -/
-def complexCoBasisFin4 : Basis (Fin 4) ℂ complexCo :=
-  Basis.reindex complexCoBasis finSumFinEquiv
+@[simp]
+lemma complexCoBasis_toFin13ℂ (i :Fin 1 ⊕ Fin 3) : (complexCoBasis i).toFin13ℂ = Pi.single i 1 := by
+  simp only [complexCoBasis, Basis.coe_ofEquivFun]
+  rw [Lorentz.CoℂModule.toFin13ℂ]
+  rfl
 
 @[simp]
 lemma complexCoBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
@@ -75,6 +84,11 @@ lemma complexCoBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
   change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ (Pi.single j 1)) i = _
   simp only [mulVec_single, transpose_apply, mul_one]
 
+/-- The standard basis of complex covariant Lorentz vectors indexed by `Fin 4`. -/
+def complexCoBasisFin4 : Basis (Fin 4) ℂ complexCo :=
+  Basis.reindex complexCoBasis finSumFinEquiv
+
+
 /-!
 
 ## Relation to real
diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean b/HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean
index 22b18de..4cd7e1c 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean
+++ b/HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean
@@ -86,6 +86,17 @@ lemma contrCoContraction_hom_tmul (ψ : complexContr) (φ : complexCo) :
     contrCoContraction.hom (ψ ⊗ₜ φ) = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ := by
   rfl
 
+lemma contrCoContraction_basis (i j : Fin 4) :
+    contrCoContraction.hom (complexContrBasisFin4 i ⊗ₜ complexCoBasisFin4 j) =
+    if i.1 = j.1 then (1 : ℂ) else 0 := by
+  rw [contrCoContraction_hom_tmul]
+  simp only [Action.instMonoidalCategory_tensorUnit_V, complexContrBasisFin4, Basis.coe_reindex,
+    Function.comp_apply, complexContrBasis_toFin13ℂ, complexCoBasisFin4, complexCoBasis_toFin13ℂ,
+    dotProduct_single, mul_one]
+  rw [Pi.single_apply]
+  refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
+  simp only [EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff, eq_iff_iff, eq_comm]
+
 /-- The linear map from complexCo ⊗ complexContr to ℂ given by
     summing over components of covariant Lorentz vector and
     contravariant Lorentz vector in the
@@ -104,6 +115,17 @@ lemma coContrContraction_hom_tmul (φ : complexCo) (ψ : complexContr) :
     coContrContraction.hom (φ ⊗ₜ ψ) = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ := by
   rfl
 
+lemma coContrContraction_basis (i j : Fin 4) :
+    coContrContraction.hom (complexCoBasisFin4 i ⊗ₜ complexContrBasisFin4 j) =
+    if i.1 = j.1 then (1 : ℂ) else 0 := by
+  rw [coContrContraction_hom_tmul]
+  simp only [Action.instMonoidalCategory_tensorUnit_V, complexCoBasisFin4, Basis.coe_reindex,
+    Function.comp_apply, complexCoBasis_toFin13ℂ, complexContrBasisFin4, complexContrBasis_toFin13ℂ,
+    dotProduct_single, mul_one]
+  rw [Pi.single_apply]
+  refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
+  simp only [EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff, eq_iff_iff, eq_comm]
+
 /-!
 
 ## Symmetry
diff --git a/HepLean/SpaceTime/WeylFermion/Basic.lean b/HepLean/SpaceTime/WeylFermion/Basic.lean
index c335682..d8d6487 100644
--- a/HepLean/SpaceTime/WeylFermion/Basic.lean
+++ b/HepLean/SpaceTime/WeylFermion/Basic.lean
@@ -58,6 +58,12 @@ lemma leftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
   change (M.1 *ᵥ (Pi.single j 1)) i = _
   simp only [mulVec_single, mul_one]
 
+@[simp]
+lemma leftBasis_toFin2ℂ (i : Fin 2) : (leftBasis i).toFin2ℂ = Pi.single i 1 := by
+  simp only [leftBasis, Basis.coe_ofEquivFun]
+  rw [LeftHandedModule.toFin2ℂ]
+  rfl
+
 /-- The vector space ℂ^2 carrying the representation of SL(2,C) given by
     M → (M⁻¹)ᵀ. In index notation corresponds to a Weyl fermion with indices ψ_a. -/
 def altLeftHanded : Rep ℂ SL(2,ℂ) := Rep.of {
@@ -85,6 +91,12 @@ def altLeftHanded : Rep ℂ SL(2,ℂ) := Rep.of {
 def altLeftBasis : Basis (Fin 2) ℂ altLeftHanded := Basis.ofEquivFun
   (Equiv.linearEquiv ℂ AltLeftHandedModule.toFin2ℂFun)
 
+@[simp]
+lemma altLeftBasis_toFin2ℂ (i : Fin 2) : (altLeftBasis i).toFin2ℂ = Pi.single i 1 := by
+  simp only [altLeftBasis, Basis.coe_ofEquivFun]
+  rw [AltLeftHandedModule.toFin2ℂ]
+  rfl
+
 @[simp]
 lemma altLeftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
     (LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M) i j = (M.1⁻¹)ᵀ i j := by
@@ -117,6 +129,12 @@ def rightHanded : Rep ℂ SL(2,ℂ) := Rep.of {
 def rightBasis : Basis (Fin 2) ℂ rightHanded := Basis.ofEquivFun
   (Equiv.linearEquiv ℂ RightHandedModule.toFin2ℂFun)
 
+@[simp]
+lemma rightBasis_toFin2ℂ (i : Fin 2) : (rightBasis i).toFin2ℂ = Pi.single i 1 := by
+  simp only [rightBasis, Basis.coe_ofEquivFun]
+  rw [RightHandedModule.toFin2ℂ]
+  rfl
+
 @[simp]
 lemma rightBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
     (LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M) i j = (M.1.map star) i j := by
@@ -153,6 +171,12 @@ def altRightHanded : Rep ℂ SL(2,ℂ) := Rep.of {
 def altRightBasis : Basis (Fin 2) ℂ altRightHanded := Basis.ofEquivFun
   (Equiv.linearEquiv ℂ AltRightHandedModule.toFin2ℂFun)
 
+@[simp]
+lemma altRightBasis_toFin2ℂ (i : Fin 2) : (altRightBasis i).toFin2ℂ = Pi.single i 1 := by
+  simp only [altRightBasis, Basis.coe_ofEquivFun]
+  rw [AltRightHandedModule.toFin2ℂ]
+  rfl
+
 @[simp]
 lemma altRightBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
     (LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M) i j =
diff --git a/HepLean/SpaceTime/WeylFermion/Contraction.lean b/HepLean/SpaceTime/WeylFermion/Contraction.lean
index 558782c..38968f6 100644
--- a/HepLean/SpaceTime/WeylFermion/Contraction.lean
+++ b/HepLean/SpaceTime/WeylFermion/Contraction.lean
@@ -137,6 +137,16 @@ lemma leftAltContraction_hom_tmul (ψ : leftHanded) (φ : altLeftHanded) :
     leftAltContraction.hom (ψ ⊗ₜ φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ := by
   rfl
 
+lemma leftAltContraction_basis (i j : Fin 2) :
+    leftAltContraction.hom (leftBasis i ⊗ₜ altLeftBasis j) = if i.1 = j.1 then (1 : ℂ) else 0 := by
+  rw [leftAltContraction_hom_tmul]
+  simp only [Action.instMonoidalCategory_tensorUnit_V, leftBasis_toFin2ℂ, altLeftBasis_toFin2ℂ,
+    dotProduct_single, mul_one]
+  rw [Pi.single_apply]
+  simp only [Fin.ext_iff]
+  refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
+  exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
+
 /-- The linear map from altLeftHandedWeyl ⊗ leftHandedWeyl to ℂ given by
     summing over components of altLeftHandedWeyl and leftHandedWeyl in the
     standard basis (i.e. the dot product).
@@ -153,6 +163,16 @@ lemma altLeftContraction_hom_tmul (φ : altLeftHanded) (ψ : leftHanded) :
     altLeftContraction.hom (φ ⊗ₜ ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ := by
   rfl
 
+lemma altLeftContraction_basis (i j : Fin 2) :
+    altLeftContraction.hom (altLeftBasis i ⊗ₜ leftBasis j) = if i.1 = j.1 then (1 : ℂ) else 0 := by
+  rw [altLeftContraction_hom_tmul]
+  simp only [Action.instMonoidalCategory_tensorUnit_V, leftBasis_toFin2ℂ, altLeftBasis_toFin2ℂ,
+    dotProduct_single, mul_one]
+  rw [Pi.single_apply]
+  simp only [Fin.ext_iff]
+  refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
+  exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
+
 /--
 The linear map from rightHandedWeyl ⊗ altRightHandedWeyl to ℂ given by
   summing over components of rightHandedWeyl and altRightHandedWeyl in the
@@ -182,6 +202,16 @@ lemma rightAltContraction_hom_tmul (ψ : rightHanded) (φ : altRightHanded) :
     rightAltContraction.hom (ψ ⊗ₜ φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ := by
   rfl
 
+lemma rightAltContraction_basis (i j : Fin 2) :
+    rightAltContraction.hom (rightBasis i ⊗ₜ altRightBasis j) = if i.1 = j.1 then (1 : ℂ) else 0 := by
+  rw [rightAltContraction_hom_tmul]
+  simp only [Action.instMonoidalCategory_tensorUnit_V, rightBasis_toFin2ℂ, altRightBasis_toFin2ℂ,
+    dotProduct_single, mul_one]
+  rw [Pi.single_apply]
+  simp only [Fin.ext_iff]
+  refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
+  exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
+
 /--
   The linear map from altRightHandedWeyl ⊗ rightHandedWeyl to ℂ given by
     summing over components of altRightHandedWeyl and rightHandedWeyl in the
@@ -211,6 +241,16 @@ lemma altRightContraction_hom_tmul (φ : altRightHanded) (ψ : rightHanded) :
     altRightContraction.hom (φ ⊗ₜ ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ := by
   rfl
 
+lemma altRightContraction_basis (i j : Fin 2) :
+    altRightContraction.hom (altRightBasis i ⊗ₜ rightBasis j) = if i.1 = j.1 then (1 : ℂ) else 0 := by
+  rw [altRightContraction_hom_tmul]
+  simp only [Action.instMonoidalCategory_tensorUnit_V, rightBasis_toFin2ℂ, altRightBasis_toFin2ℂ,
+    dotProduct_single, mul_one]
+  rw [Pi.single_apply]
+  simp only [Fin.ext_iff]
+  refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
+  exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
+
 /-!
 
 ## Symmetry properties
diff --git a/HepLean/Tensors/ComplexLorentz/Basic.lean b/HepLean/Tensors/ComplexLorentz/Basic.lean
index 979ab28..067b2b9 100644
--- a/HepLean/Tensors/ComplexLorentz/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basic.lean
@@ -170,5 +170,20 @@ def complexLorentzTensor : TensorSpecies where
 
 instance : DecidableEq complexLorentzTensor.C := Fermion.instDecidableEqColor
 
+lemma basis_contr (c : complexLorentzTensor.C) (i : Fin (complexLorentzTensor.repDim c))
+    (j : Fin (complexLorentzTensor.repDim (complexLorentzTensor.τ c))) :
+    complexLorentzTensor.castToField
+    ((complexLorentzTensor.contr.app {as := c}).hom
+    (complexLorentzTensor.basis c i ⊗ₜ complexLorentzTensor.basis (complexLorentzTensor.τ c) j)) =
+    if i.val = j.val then 1 else 0 :=
+  match c with
+  | Color.upL => Fermion.leftAltContraction_basis _ _
+  | Color.downL => Fermion.altLeftContraction_basis _ _
+  | Color.upR => Fermion.rightAltContraction_basis _ _
+  | Color.downR => Fermion.altRightContraction_basis _ _
+  | Color.up => Lorentz.contrCoContraction_basis _ _
+  | Color.down => Lorentz.coContrContraction_basis _ _
+
+
 end
 end Fermion
diff --git a/HepLean/Tensors/ComplexLorentz/Basis.lean b/HepLean/Tensors/ComplexLorentz/Basis.lean
index 4bb852d..545ad9a 100644
--- a/HepLean/Tensors/ComplexLorentz/Basis.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basis.lean
@@ -42,6 +42,58 @@ def basisVector {n : ℕ} (c : Fin n → complexLorentzTensor.C)
     complexLorentzTensor.F.obj (OverColor.mk c) :=
   PiTensorProduct.tprod ℂ (fun i => complexLorentzTensor.basis (c i) (b i))
 
+lemma perm_basisVector_cast {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
+    {c1 : Fin m → complexLorentzTensor.C}
+    (σ : OverColor.mk c ⟶ OverColor.mk c1) (i : Fin m) :
+    complexLorentzTensor.repDim (c ((OverColor.Hom.toEquiv σ).symm i)) =
+    complexLorentzTensor.repDim (c1 i) := by
+  have h1 := OverColor.Hom.toEquiv_symm_apply σ i
+  simp only [Functor.const_obj_obj, OverColor.mk_hom] at h1
+  rw [h1]
+
+/-! TODO: Generalize `basis_eq_FDiscrete`. -/
+lemma basis_eq_FDiscrete {n : ℕ} (c : Fin n → complexLorentzTensor.C)
+    (b : Π j, Fin (complexLorentzTensor.repDim (c j))) (i : Fin n)
+    (h : { as := c i } = { as := c1 }) :
+    (complexLorentzTensor.FDiscrete.map (eqToHom h)).hom
+    (complexLorentzTensor.basis (c i) (b i)) =
+    (complexLorentzTensor.basis c1 (Fin.cast (by simp_all) (b i))) := by
+  have h' : c i = c1 := by
+    simp_all only [Discrete.mk.injEq]
+  subst h'
+  rfl
+
+lemma perm_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
+    {c1 : Fin m → complexLorentzTensor.C} (σ : OverColor.mk c ⟶ OverColor.mk c1)
+    (b : Π j, Fin (complexLorentzTensor.repDim (c j))) :
+    (perm σ (tensorNode (basisVector c b))).tensor =
+    (basisVector c1 (fun i => Fin.cast (perm_basisVector_cast σ i)
+    (b ((OverColor.Hom.toEquiv σ).symm i)))) := by
+  rw [perm_tensor]
+  simp only [TensorSpecies.F_def, tensorNode_tensor]
+  rw [basisVector, basisVector]
+  erw [OverColor.lift.map_tprod]
+  apply congrArg
+  funext i
+  simp only [OverColor.mk_hom, OverColor.lift.discreteFunctorMapEqIso, Functor.mapIso_hom,
+    eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, LinearEquiv.ofLinear_apply]
+  rw [basis_eq_FDiscrete]
+
+lemma contr_basisVector {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} {i : Fin n.succ.succ} {j : Fin n.succ}
+    {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)} (b : Π k, Fin (complexLorentzTensor.repDim (c k))) :
+    (contr i j h (tensorNode (basisVector c b))).tensor = (if (b i).val = ((b (i.succAbove j))).val then (1 : ℂ) else 0) •
+    basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
+      (fun k => b (i.succAbove (j.succAbove k))) := by
+  rw [contr_tensor]
+  simp only [Nat.succ_eq_add_one, tensorNode_tensor]
+  rw [basisVector]
+  erw [TensorSpecies.contrMap_tprod]
+  congr 1
+  rw [basis_eq_FDiscrete]
+  simp
+  erw [basis_contr]
+  rfl
+
 /-!
 
 ## Useful expansions.