feat: Add contraction of metric property for complex

HepLean/SpaceTime/LorentzVector/Complex/Metric.lean

@@ -5,6 +5,8 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzVector.Complex.Two
 import HepLean.SpaceTime.MinkowskiMetric
+import HepLean.SpaceTime.LorentzVector.Complex.Contraction
+import HepLean.SpaceTime.LorentzVector.Complex.Unit
 /-!
 
 # Metric for complex Lorentz vectors
@@ -128,5 +130,64 @@ lemma coMetric_apply_one : coMetric.hom (1 : ℂ) = coMetricVal := by
   simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
     coMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
 
+
+/-!
+
+## Contraction of metrics
+
+-/
+
+lemma contrCoContraction_apply_metric : (β_ complexContr complexCo).hom.hom
+    ((complexContr.V ◁ (λ_ complexCo.V).hom)
+    ((complexContr.V ◁ contrCoContraction.hom ▷ complexCo.V)
+    ((complexContr.V ◁ (α_ complexContr.V complexCo.V complexCo.V).inv)
+    ((α_ complexContr.V complexContr.V (complexCo.V ⊗ complexCo.V)).hom
+    (contrMetric.hom (1 : ℂ) ⊗ₜ[ℂ] coMetric.hom (1 : ℂ)))))) =
+    coContrUnit.hom (1 : ℂ) := by
+  rw [contrMetric_apply_one, coMetric_apply_one]
+  rw [contrMetricVal_expand_tmul, coMetricVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Fin.isValue, tmul_sub, add_tmul, neg_tmul, map_sub, map_add, map_neg, tmul_sub, sub_tmul]
+  have h1 (x1 x2 : complexContr) (y1 y2 :complexCo) :
+    (complexContr.V ◁ (λ_ complexCo.V).hom)
+    ((complexContr.V ◁ contrCoContraction.hom ▷ complexCo.V) (((complexContr.V ◁
+    (α_ complexContr.V complexCo.V complexCo.V).inv)
+    ((α_ complexContr.V complexContr.V (complexCo.V ⊗ complexCo.V)).hom
+    ((x1 ⊗ₜ[ℂ] x2) ⊗ₜ[ℂ] y1 ⊗ₜ[ℂ] y2)))))
+      = x1 ⊗ₜ[ℂ] ((λ_ complexCo.V).hom ((contrCoContraction.hom (x2 ⊗ₜ[ℂ] y1)) ⊗ₜ[ℂ] y2)) := rfl
+  repeat rw (config := { transparency := .instances }) [h1]
+  repeat rw [contrCoContraction_basis']
+  simp only [Fin.isValue, ↓reduceIte, ModuleCat.MonoidalCategory.leftUnitor_hom_apply, one_smul,
+    reduceCtorEq, zero_tmul, map_zero, tmul_zero, sub_zero, zero_sub, Sum.inr.injEq, one_ne_zero,
+    Fin.reduceEq, sub_neg_eq_add, zero_ne_one, sub_self]
+  erw [coContrUnit_apply_one, coContrUnitVal_expand_tmul]
+  rfl
+
+lemma coContrContraction_apply_metric : (β_ complexCo complexContr).hom.hom
+    ((complexCo.V ◁ (λ_ complexContr.V).hom)
+    ((complexCo.V ◁ coContrContraction.hom ▷ complexContr.V)
+    ((complexCo.V ◁ (α_ complexCo.V complexContr.V complexContr.V).inv)
+    ((α_ complexCo.V complexCo.V (complexContr.V ⊗ complexContr.V)).hom
+    (coMetric.hom (1 : ℂ) ⊗ₜ[ℂ] contrMetric.hom (1 : ℂ)))))) =
+    contrCoUnit.hom (1 : ℂ) := by
+  rw [coMetric_apply_one, contrMetric_apply_one]
+  rw [coMetricVal_expand_tmul, contrMetricVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Fin.isValue, tmul_sub, add_tmul, neg_tmul, map_sub, map_add, map_neg, tmul_sub, sub_tmul]
+  have h1 (x1 x2 : complexCo) (y1 y2 :complexContr) :
+    (complexCo.V ◁ (λ_ complexContr.V).hom)
+    ((complexCo.V ◁ coContrContraction.hom ▷ complexContr.V) (((complexCo.V ◁
+    (α_ complexCo.V complexContr.V complexContr.V).inv)
+    ((α_ complexCo.V complexCo.V (complexContr.V ⊗ complexContr.V)).hom
+    ((x1 ⊗ₜ[ℂ] x2) ⊗ₜ[ℂ] y1 ⊗ₜ[ℂ] y2)))))
+      = x1 ⊗ₜ[ℂ] ((λ_ complexContr.V).hom ((coContrContraction.hom (x2 ⊗ₜ[ℂ] y1)) ⊗ₜ[ℂ] y2)) := rfl
+  repeat rw (config := { transparency := .instances }) [h1]
+  repeat rw [coContrContraction_basis']
+  simp only [Fin.isValue, ↓reduceIte, ModuleCat.MonoidalCategory.leftUnitor_hom_apply, one_smul,
+    reduceCtorEq, zero_tmul, map_zero, tmul_zero, sub_zero, zero_sub, Sum.inr.injEq, one_ne_zero,
+    Fin.reduceEq, sub_neg_eq_add, zero_ne_one, sub_self]
+  erw [contrCoUnit_apply_one, contrCoUnitVal_expand_tmul]
+  rfl
+
 end Lorentz
 end

HepLean/SpaceTime/LorentzVector/Complex/Unit.lean

@@ -178,7 +178,7 @@ lemma contr_coContrUnit (x : complexContr) :
     Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
     Finset.sum_singleton, Fin.sum_univ_three, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add,
     _root_.map_smul]
-  have h1'  (x y :  CoeSort.coe complexContr) (z :  CoeSort.coe complexCo) :
+  have h1' (x y :  CoeSort.coe complexContr) (z :  CoeSort.coe complexCo) :
     (α_ complexContr.V complexCo.V complexContr.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl
   repeat rw [h1']
   have h1'' ( y :  CoeSort.coe complexContr) (z :  CoeSort.coe complexContr ⊗[ℂ] CoeSort.coe complexCo) :

HepLean/SpaceTime/WeylFermion/Metric.lean

@@ -7,6 +7,7 @@ import HepLean.SpaceTime.WeylFermion.Basic
 import HepLean.SpaceTime.WeylFermion.Contraction
 import Mathlib.LinearAlgebra.TensorProduct.Matrix
 import HepLean.SpaceTime.WeylFermion.Two
+import HepLean.SpaceTime.WeylFermion.Unit
 /-!
 
 # Metrics of Weyl fermions
@@ -274,5 +275,119 @@ lemma altRightMetric_apply_one : altRightMetric.hom (1 : ℂ) = altRightMetricVa
   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]
+
+/-!
+
+## Contraction of metrics
+
+-/
+
+lemma leftAltContraction_apply_metric : (β_ leftHanded altLeftHanded).hom.hom
+    ((leftHanded.V ◁ (λ_ altLeftHanded.V).hom)
+    ((leftHanded.V ◁ leftAltContraction.hom ▷ altLeftHanded.V)
+    ((leftHanded.V ◁ (α_ leftHanded.V altLeftHanded.V altLeftHanded.V).inv)
+    ((α_ leftHanded.V leftHanded.V (altLeftHanded.V ⊗ altLeftHanded.V)).hom
+    (leftMetric.hom (1 : ℂ) ⊗ₜ[ℂ] altLeftMetric.hom (1 : ℂ)))))) =
+    altLeftLeftUnit.hom (1 : ℂ) := by
+  rw [leftMetric_apply_one, altLeftMetric_apply_one]
+  rw [leftMetricVal_expand_tmul, altLeftMetricVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Fin.isValue, tmul_sub, add_tmul, neg_tmul, map_sub, map_add, map_neg]
+  have h1 (x1 x2 : leftHanded) (y1 y2 :altLeftHanded) :
+    (leftHanded.V ◁ (λ_ altLeftHanded.V).hom)
+    ((leftHanded.V ◁ leftAltContraction.hom ▷ altLeftHanded.V) (((leftHanded.V ◁
+    (α_ leftHanded.V altLeftHanded.V altLeftHanded.V).inv)
+    ((α_ leftHanded.V leftHanded.V (altLeftHanded.V ⊗ altLeftHanded.V)).hom
+    ((x1 ⊗ₜ[ℂ] x2) ⊗ₜ[ℂ] y1 ⊗ₜ[ℂ] y2)))))
+      = x1 ⊗ₜ[ℂ] ((λ_ altLeftHanded.V).hom ((leftAltContraction.hom (x2 ⊗ₜ[ℂ] y1)) ⊗ₜ[ℂ] y2)) := rfl
+  repeat rw (config := { transparency := .instances }) [h1]
+  repeat rw [leftAltContraction_basis]
+  simp only [Fin.isValue, Fin.val_one, Fin.val_zero, one_ne_zero, ↓reduceIte, zero_tmul, map_zero,
+    tmul_zero, neg_zero, ModuleCat.MonoidalCategory.leftUnitor_hom_apply, one_smul, zero_add,
+    zero_ne_one, add_zero, sub_neg_eq_add]
+  erw [altLeftLeftUnit_apply_one, altLeftLeftUnitVal_expand_tmul]
+  rw [add_comm]
+  rfl
+
+lemma altLeftContraction_apply_metric : (β_ altLeftHanded leftHanded).hom.hom
+    ((altLeftHanded.V ◁ (λ_ leftHanded.V).hom)
+    ((altLeftHanded.V ◁ altLeftContraction.hom ▷ leftHanded.V)
+    ((altLeftHanded.V ◁ (α_ altLeftHanded.V leftHanded.V leftHanded.V).inv)
+    ((α_ altLeftHanded.V altLeftHanded.V (leftHanded.V ⊗ leftHanded.V)).hom
+    (altLeftMetric.hom (1 : ℂ) ⊗ₜ[ℂ] leftMetric.hom (1 : ℂ)))))) =
+    leftAltLeftUnit.hom (1 : ℂ) := by
+  rw [leftMetric_apply_one, altLeftMetric_apply_one]
+  rw [leftMetricVal_expand_tmul, altLeftMetricVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Fin.isValue, tmul_add, tmul_neg, sub_tmul, map_add, map_neg, map_sub]
+  have h1 (x1 x2 : altLeftHanded) (y1 y2 : leftHanded) :
+    (altLeftHanded.V ◁ (λ_ leftHanded.V).hom)
+    ((altLeftHanded.V ◁ altLeftContraction.hom ▷ leftHanded.V) (((altLeftHanded.V ◁
+    (α_ altLeftHanded.V leftHanded.V leftHanded.V).inv)
+    ((α_ altLeftHanded.V altLeftHanded.V (leftHanded.V ⊗ leftHanded.V)).hom
+    ((x1 ⊗ₜ[ℂ] x2) ⊗ₜ[ℂ] y1 ⊗ₜ[ℂ] y2)))))
+      = x1 ⊗ₜ[ℂ] ((λ_ leftHanded.V).hom ((altLeftContraction.hom (x2 ⊗ₜ[ℂ] y1)) ⊗ₜ[ℂ] y2)) := rfl
+  repeat rw (config := { transparency := .instances }) [h1]
+  repeat rw [altLeftContraction_basis]
+  simp only [Fin.isValue, Fin.val_one, Fin.val_zero, one_ne_zero, ↓reduceIte, zero_tmul, map_zero,
+    tmul_zero, ModuleCat.MonoidalCategory.leftUnitor_hom_apply, one_smul, zero_sub, neg_neg,
+    zero_ne_one, sub_zero]
+  erw [leftAltLeftUnit_apply_one, leftAltLeftUnitVal_expand_tmul]
+  rw [add_comm]
+  rfl
+
+lemma rightAltContraction_apply_metric : (β_ rightHanded altRightHanded).hom.hom
+    ((rightHanded.V ◁ (λ_ altRightHanded.V).hom)
+    ((rightHanded.V ◁ rightAltContraction.hom ▷ altRightHanded.V)
+    ((rightHanded.V ◁ (α_ rightHanded.V altRightHanded.V altRightHanded.V).inv)
+    ((α_ rightHanded.V rightHanded.V (altRightHanded.V ⊗ altRightHanded.V)).hom
+    (rightMetric.hom (1 : ℂ) ⊗ₜ[ℂ] altRightMetric.hom (1 : ℂ)))))) =
+    altRightRightUnit.hom (1 : ℂ) := by
+  rw [rightMetric_apply_one, altRightMetric_apply_one]
+  rw [rightMetricVal_expand_tmul, altRightMetricVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Fin.isValue, tmul_sub, add_tmul, neg_tmul, map_sub, map_add, map_neg]
+  have h1 (x1 x2 : rightHanded) (y1 y2 : altRightHanded) :
+    (rightHanded.V ◁ (λ_ altRightHanded.V).hom)
+    ((rightHanded.V ◁ rightAltContraction.hom ▷ altRightHanded.V) (((rightHanded.V ◁
+    (α_ rightHanded.V altRightHanded.V altRightHanded.V).inv)
+    ((α_ rightHanded.V rightHanded.V (altRightHanded.V ⊗ altRightHanded.V)).hom
+    ((x1 ⊗ₜ[ℂ] x2) ⊗ₜ[ℂ] y1 ⊗ₜ[ℂ] y2)))))
+      = x1 ⊗ₜ[ℂ] ((λ_ altRightHanded.V).hom ((rightAltContraction.hom (x2 ⊗ₜ[ℂ] y1)) ⊗ₜ[ℂ] y2)) := rfl
+  repeat rw (config := { transparency := .instances }) [h1]
+  repeat rw [rightAltContraction_basis]
+  simp only [Fin.isValue, Fin.val_one, Fin.val_zero, one_ne_zero, ↓reduceIte, zero_tmul, map_zero,
+    tmul_zero, neg_zero, ModuleCat.MonoidalCategory.leftUnitor_hom_apply, one_smul, zero_add,
+    zero_ne_one, add_zero, sub_neg_eq_add]
+  erw [altRightRightUnit_apply_one, altRightRightUnitVal_expand_tmul]
+  rw [add_comm]
+  rfl
+
+lemma altRightContraction_apply_metric : (β_ altRightHanded rightHanded).hom.hom
+    ((altRightHanded.V ◁ (λ_ rightHanded.V).hom)
+    ((altRightHanded.V ◁ altRightContraction.hom ▷ rightHanded.V)
+    ((altRightHanded.V ◁ (α_ altRightHanded.V rightHanded.V rightHanded.V).inv)
+    ((α_ altRightHanded.V altRightHanded.V (rightHanded.V ⊗ rightHanded.V)).hom
+    (altRightMetric.hom (1 : ℂ) ⊗ₜ[ℂ] rightMetric.hom (1 : ℂ)))))) =
+    rightAltRightUnit.hom (1 : ℂ) := by
+  rw [rightMetric_apply_one, altRightMetric_apply_one]
+  rw [rightMetricVal_expand_tmul, altRightMetricVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Fin.isValue, tmul_add, tmul_neg, sub_tmul, map_add, map_neg, map_sub]
+  have h1 (x1 x2 : altRightHanded) (y1 y2 : rightHanded) : (altRightHanded.V ◁ (λ_ rightHanded.V).hom)
+    ((altRightHanded.V ◁ altRightContraction.hom ▷ rightHanded.V) (((altRightHanded.V ◁
+    (α_ altRightHanded.V rightHanded.V rightHanded.V).inv)
+    ((α_ altRightHanded.V altRightHanded.V (rightHanded.V ⊗ rightHanded.V)).hom
+    ((x1 ⊗ₜ[ℂ] x2) ⊗ₜ[ℂ] y1 ⊗ₜ[ℂ] y2)))))
+      = x1 ⊗ₜ[ℂ] ((λ_ rightHanded.V).hom ((altRightContraction.hom (x2 ⊗ₜ[ℂ] y1)) ⊗ₜ[ℂ] y2)) := rfl
+  repeat rw (config := { transparency := .instances }) [h1]
+  repeat rw [altRightContraction_basis]
+  simp only [Fin.isValue, Fin.val_one, Fin.val_zero, one_ne_zero, ↓reduceIte, zero_tmul, map_zero,
+    tmul_zero, ModuleCat.MonoidalCategory.leftUnitor_hom_apply, one_smul, zero_sub, neg_neg,
+    zero_ne_one, sub_zero]
+  erw [rightAltRightUnit_apply_one, rightAltRightUnitVal_expand_tmul]
+  rw [add_comm]
+  rfl
+
 end
 end Fermion

HepLean/Tensors/ComplexLorentz/Basic.lean

@@ -183,7 +183,14 @@ def complexLorentzTensor : TensorSpecies where
     | Color.downR => Fermion.rightAltRightUnit_symm
     | Color.up => Lorentz.coContrUnit_symm
     | Color.down => Lorentz.contrCoUnit_symm
-  contr_metric := by sorry
+  contr_metric :=  fun c =>
+    match c with
+    | Color.upL => by simpa using Fermion.leftAltContraction_apply_metric
+    | Color.downL => by simpa using Fermion.altLeftContraction_apply_metric
+    | Color.upR => by simpa using Fermion.rightAltContraction_apply_metric
+    | Color.downR => by simpa using Fermion.altRightContraction_apply_metric
+    | Color.up => by simpa using Lorentz.contrCoContraction_apply_metric
+    | Color.down => by simpa using Lorentz.coContrContraction_apply_metric
 
 instance : DecidableEq complexLorentzTensor.C := Fermion.instDecidableEqColor