From ca55da6a34a1ad8be26df049be5d014f6ca2081c Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 23 Oct 2024 11:19:22 +0000
Subject: [PATCH] feat: Expansion of metrics in terms of basis

---
 HepLean/SpaceTime/WeylFermion/Metric.lean | 57 ++++++++++++++
 HepLean/Tensors/ComplexLorentz/Basis.lean | 93 +++++++++++++++++++++--
 HepLean/Tensors/Tree/Elab.lean            | 10 +++
 3 files changed, 154 insertions(+), 6 deletions(-)

diff --git a/HepLean/SpaceTime/WeylFermion/Metric.lean b/HepLean/SpaceTime/WeylFermion/Metric.lean
index 0472876..ea565e2 100644
--- a/HepLean/SpaceTime/WeylFermion/Metric.lean
+++ b/HepLean/SpaceTime/WeylFermion/Metric.lean
@@ -70,6 +70,15 @@ lemma metricRaw_comm_star (M : SL(2,ℂ)) : metricRaw * M.1.map star = ((M.1)⁻
 def leftMetricVal : (leftHanded ⊗ leftHanded).V :=
   leftLeftToMatrix.symm (- metricRaw)
 
+/-- Expansion of `leftMetricVal` into the left basis. -/
+lemma leftMetricVal_expand_tmul : leftMetricVal =
+    - leftBasis 0 ⊗ₜ[ℂ] leftBasis 1 + leftBasis 1 ⊗ₜ[ℂ] leftBasis 0 := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, leftMetricVal, Fin.isValue]
+  erw [leftLeftToMatrix_symm_expand_tmul]
+  simp only [metricRaw, neg_apply, of_apply, cons_val', empty_val', cons_val_fin_one, neg_smul,
+    Finset.sum_neg_distrib, Fin.sum_univ_two, Fin.isValue, cons_val_zero, cons_val_one, head_cons,
+    neg_add_rev, one_smul, zero_smul, neg_zero, add_zero, head_fin_const, neg_neg, zero_add]
+
 /-- The metric `εₐₐ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded`,
   making manifest its invariance under the action of `SL(2,ℂ)`. -/
 def leftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded where
@@ -99,10 +108,25 @@ def leftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded where
     simp only [SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero,
       not_false_eq_true, mul_nonsing_inv, transpose_one, mul_one]
 
+lemma leftMetric_apply_one : leftMetric.hom (1 : ℂ) = leftMetricVal := by
+  change leftMetric.hom.toFun (1 : ℂ) = leftMetricVal
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    leftMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+
 /-- The metric `εᵃᵃ` as an element of `(altLeftHanded ⊗ altLeftHanded).V`. -/
 def altLeftMetricVal : (altLeftHanded ⊗ altLeftHanded).V :=
   altLeftaltLeftToMatrix.symm metricRaw
 
+/-- Expansion of `altLeftMetricVal` into the left basis. -/
+lemma altLeftMetricVal_expand_tmul : altLeftMetricVal =
+    altLeftBasis 0 ⊗ₜ[ℂ] altLeftBasis 1 - altLeftBasis 1 ⊗ₜ[ℂ] altLeftBasis 0 := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, altLeftMetricVal, Fin.isValue]
+  erw [altLeftaltLeftToMatrix_symm_expand_tmul]
+  simp only [metricRaw, neg_apply, of_apply, cons_val', empty_val', cons_val_fin_one, neg_smul,
+    Finset.sum_neg_distrib, Fin.sum_univ_two, Fin.isValue, cons_val_zero, cons_val_one, head_cons,
+    neg_add_rev, one_smul, zero_smul, neg_zero, add_zero, head_fin_const, neg_neg, zero_add]
+  rfl
+
 /-- The metric `εᵃᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHanded`,
   making manifest its invariance under the action of `SL(2,ℂ)`. -/
 def altLeftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHanded where
@@ -132,10 +156,24 @@ def altLeftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHande
     simp only [SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero,
       not_false_eq_true, mul_nonsing_inv, mul_one]
 
+lemma altLeftMetric_apply_one : altLeftMetric.hom (1 : ℂ) = altLeftMetricVal := by
+  change altLeftMetric.hom.toFun (1 : ℂ) = altLeftMetricVal
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    altLeftMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+
 /-- The metric `ε_{dot a}_{dot a}` as an element of `(rightHanded ⊗ rightHanded).V`. -/
 def rightMetricVal : (rightHanded ⊗ rightHanded).V :=
   rightRightToMatrix.symm (- metricRaw)
 
+/-- Expansion of `rightMetricVal` into the left basis. -/
+lemma rightMetricVal_expand_tmul : rightMetricVal =
+    - rightBasis 0 ⊗ₜ[ℂ] rightBasis 1 + rightBasis 1 ⊗ₜ[ℂ] rightBasis 0 := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, rightMetricVal, Fin.isValue]
+  erw [rightRightToMatrix_symm_expand_tmul]
+  simp only [metricRaw, neg_apply, of_apply, cons_val', empty_val', cons_val_fin_one, neg_smul,
+    Finset.sum_neg_distrib, Fin.sum_univ_two, Fin.isValue, cons_val_zero, cons_val_one, head_cons,
+    neg_add_rev, one_smul, zero_smul, neg_zero, add_zero, head_fin_const, neg_neg, zero_add]
+
 /-- The metric `ε_{dot a}_{dot a}` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded`,
   making manifest its invariance under the action of `SL(2,ℂ)`. -/
 def rightMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded where
@@ -173,10 +211,25 @@ def rightMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded wher
     · rw [← rightRightToMatrix_ρ_symm metricRaw M]
       rfl
 
+lemma rightMetric_apply_one : rightMetric.hom (1 : ℂ) = rightMetricVal := by
+  change rightMetric.hom.toFun (1 : ℂ) = rightMetricVal
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    rightMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+
 /-- The metric `ε^{dot a}^{dot a}` as an element of `(altRightHanded ⊗ altRightHanded).V`. -/
 def altRightMetricVal : (altRightHanded ⊗ altRightHanded).V :=
   altRightAltRightToMatrix.symm (metricRaw)
 
+/-- Expansion of `rightMetricVal` into the left basis. -/
+lemma altRightMetricVal_expand_tmul : altRightMetricVal =
+    altRightBasis 0 ⊗ₜ[ℂ] altRightBasis 1 - altRightBasis 1 ⊗ₜ[ℂ] altRightBasis 0 := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, altRightMetricVal, Fin.isValue]
+  erw [altRightAltRightToMatrix_symm_expand_tmul]
+  simp only [metricRaw, neg_apply, of_apply, cons_val', empty_val', cons_val_fin_one, neg_smul,
+    Finset.sum_neg_distrib, Fin.sum_univ_two, Fin.isValue, cons_val_zero, cons_val_one, head_cons,
+    neg_add_rev, one_smul, zero_smul, neg_zero, add_zero, head_fin_const, neg_neg, zero_add]
+  rfl
+
 /-- The metric `ε^{dot a}^{dot a}` as a morphism
   `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ altRightHanded`,
   making manifest its invariance under the action of `SL(2,ℂ)`. -/
@@ -217,5 +270,9 @@ def altRightMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ altRightHa
     · rw [← altRightAltRightToMatrix_ρ_symm metricRaw M]
       rfl
 
+lemma altRightMetric_apply_one : altRightMetric.hom (1 : ℂ) = altRightMetricVal := by
+  change altRightMetric.hom.toFun (1 : ℂ) = altRightMetricVal
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    altRightMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
 end
 end Fermion
diff --git a/HepLean/Tensors/ComplexLorentz/Basis.lean b/HepLean/Tensors/ComplexLorentz/Basis.lean
index ce9c1da..61f9d31 100644
--- a/HepLean/Tensors/ComplexLorentz/Basis.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basis.lean
@@ -114,15 +114,15 @@ lemma prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     basisVector (Sum.elim c c1 ∘ finSumFinEquiv.symm) (fun i =>
     prodBasisVecEquiv (finSumFinEquiv.symm i)
     ((HepLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))) := by
-  rw [prod_tensor]
-  simp
-  rw [basisVector, basisVector]
-  simp [TensorSpecies.F_def]
+  rw [prod_tensor, basisVector, basisVector]
+  simp only [TensorSpecies.F_def, Functor.id_obj, OverColor.mk_hom,
+    Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    tensorNode_tensor]
   have h1 := OverColor.lift.μ_tmul_tprod_mk complexLorentzTensor.FDiscrete
     (fun i => (complexLorentzTensor.basis (c i)) (b i))
     (fun i => (complexLorentzTensor.basis (c1 i)) (b1 i))
-  erw [h1]
-  erw [OverColor.lift.map_tprod]
+  erw [h1, OverColor.lift.map_tprod]
   apply congrArg
   funext i
   obtain ⟨k, hk⟩ := finSumFinEquiv.surjective i
@@ -135,6 +135,21 @@ lemma prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
   | Sum.inl k => rfl
   | Sum.inr k => rfl
 
+lemma eval_basisVector  {n : ℕ} {c : Fin n.succ → complexLorentzTensor.C}
+    {i : Fin n.succ} (j : Fin (complexLorentzTensor.repDim (c i)))
+    (b : Π k, Fin (complexLorentzTensor.repDim (c k))) :
+    (eval i j (tensorNode (basisVector c b))).tensor = (if j = b i then (1 : ℂ) else 0) •
+    basisVector (c ∘ Fin.succAbove i) (fun k => b (i.succAbove k)) := by
+  rw [eval_tensor, basisVector, basisVector]
+  simp only [Nat.succ_eq_add_one, Functor.id_obj, OverColor.mk_hom, tensorNode_tensor,
+    Function.comp_apply, one_smul, zero_smul]
+  erw [TensorSpecies.evalMap_tprod]
+  congr 1
+  have h1 : Fin.ofNat' ↑j (@Fin.size_pos' (complexLorentzTensor.repDim (c i)) _) = j := by
+    simpa [Fin.ext_iff] using Nat.mod_eq_of_lt j.prop
+  rw [Basis.repr_self, Finsupp.single_apply, h1]
+  exact ite_congr (Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a))
+    (congrFun rfl) (congrFun rfl)
 
 /-!
 
@@ -193,6 +208,72 @@ lemma contrMatrix_basis_expand : {Lorentz.contrMetric | μ ν}ᵀ.tensor =
       simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply]
       rfl
 
+lemma leftMetric_expand : {Fermion.leftMetric | α β}ᵀ.tensor =
+   - basisVector ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1)
+    + basisVector ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0) := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue]
+  erw [Fermion.leftMetric_apply_one, Fermion.leftMetricVal_expand_tmul]
+  simp only [Fin.isValue, map_add, map_neg]
+  congr 1
+  congr 1
+  all_goals
+    erw [pairIsoSep_tmul, basisVector]
+    apply congrArg
+    funext i
+    fin_cases i
+    · rfl
+    · rfl
+
+lemma altLeftMetric_expand : {Fermion.altLeftMetric | α β}ᵀ.tensor =
+    basisVector ![Color.downL, Color.downL] (fun | 0 => 0 | 1 => 1)
+    - basisVector ![Color.downL, Color.downL] (fun | 0 => 1 | 1 => 0) := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue]
+  erw [Fermion.altLeftMetric_apply_one, Fermion.altLeftMetricVal_expand_tmul]
+  simp only [Fin.isValue, map_sub]
+  congr 1
+  all_goals
+    erw [pairIsoSep_tmul, basisVector]
+    apply congrArg
+    funext i
+    fin_cases i
+    · rfl
+    · rfl
+
+lemma rightMetric_expand : {Fermion.rightMetric | α β}ᵀ.tensor =
+    - basisVector ![Color.upR, Color.upR] (fun | 0 => 0 | 1 => 1)
+    + basisVector ![Color.upR, Color.upR] (fun | 0 => 1 | 1 => 0) := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue]
+  erw [Fermion.rightMetric_apply_one, Fermion.rightMetricVal_expand_tmul]
+  simp only [Fin.isValue, map_add, map_neg]
+  congr 1
+  congr 1
+  all_goals
+    erw [pairIsoSep_tmul, basisVector]
+    apply congrArg
+    funext i
+    fin_cases i
+    · rfl
+    · rfl
+
+lemma altRightMetric_expand : {Fermion.altRightMetric | α β}ᵀ.tensor =
+    basisVector ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1)
+    - basisVector ![Color.downR, Color.downR] (fun | 0 => 1 | 1 => 0) := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue]
+  erw [Fermion.altRightMetric_apply_one, Fermion.altRightMetricVal_expand_tmul]
+  simp only [Fin.isValue, map_sub]
+  congr 1
+  all_goals
+    erw [pairIsoSep_tmul, basisVector]
+    apply congrArg
+    funext i
+    fin_cases i
+    · rfl
+    · rfl
+
 /-- The expansion of the Pauli matrices `σ^μ^a^{dot a}` in terms of basis vectors. -/
 lemma pauliMatrix_basis_expand : {PauliMatrix.asConsTensor | μ α β}ᵀ.tensor =
     basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 0 | 2 => 0)
diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean
index a8da69f..885302c 100644
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@@ -218,6 +218,16 @@ def specialTypes : List (String × (Term → Term)) := [
       mkIdent ``Fermion.complexLorentzTensor,
       mkIdent ``Fermion.Color.upL,
       mkIdent ``Fermion.Color.upL, T]),
+  ("𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Fermion.altLeftHanded ⊗ Fermion.altLeftHanded", fun T =>
+    Syntax.mkApp (mkIdent ``TensorTree.constTwoNodeE) #[
+      mkIdent ``Fermion.complexLorentzTensor,
+      mkIdent ``Fermion.Color.downL,
+      mkIdent ``Fermion.Color.downL, T]),
+  ("𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Fermion.altRightHanded ⊗ Fermion.altRightHanded", fun T =>
+    Syntax.mkApp (mkIdent ``TensorTree.constTwoNodeE) #[
+      mkIdent ``Fermion.complexLorentzTensor,
+      mkIdent ``Fermion.Color.downR,
+      mkIdent ``Fermion.Color.downR, T]),
   ("𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Fermion.rightHanded ⊗ Fermion.rightHanded", fun T =>
     Syntax.mkApp (mkIdent ``TensorTree.constTwoNodeE) #[
       mkIdent ``Fermion.complexLorentzTensor,