feat: contr_unit for Complex Lorentz Tensors

HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean

@@ -97,6 +97,17 @@ lemma contrCoContraction_basis (i j : Fin 4) :
   refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
   simp only [EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff, eq_iff_iff, eq_comm]
 
+lemma contrCoContraction_basis' (i j : Fin 1 ⊕ Fin 3) :
+    contrCoContraction.hom (complexContrBasis i ⊗ₜ complexCoBasis j) =
+    if i = j 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)
+  exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
+
 /-- The linear map from complexCo ⊗ complexContr to ℂ given by
     summing over components of covariant Lorentz vector and
     contravariant Lorentz vector in the
@@ -126,6 +137,17 @@ lemma coContrContraction_basis (i j : Fin 4) :
   refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
   simp only [EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff, eq_iff_iff, eq_comm]
 
+lemma coContrContraction_basis' (i j : Fin 1 ⊕ Fin 3) :
+    coContrContraction.hom (complexCoBasis i ⊗ₜ complexContrBasis j) =
+    if i = j 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

HepLean/SpaceTime/LorentzVector/Complex/Unit.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzVector.Complex.Two
+import HepLean.SpaceTime.LorentzVector.Complex.Contraction
 /-!
 
 # Unit for complex Lorentz vectors
@@ -122,6 +123,76 @@ lemma coContrUnit_apply_one : coContrUnit.hom (1 : ℂ) = coContrUnitVal := by
   change coContrUnit.hom.toFun (1 : ℂ) = coContrUnitVal
   simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
     coContrUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+/-!
+
+## Contraction of the units
+
+-/
+
+/-- Contraction on the right with `contrCoUnit` does nothing. -/
+lemma contr_contrCoUnit (x : complexCo) :
+    (λ_ complexCo).hom.hom
+    ((coContrContraction ▷ complexCo).hom
+    ((α_ _ _ complexCo).inv.hom
+    (x ⊗ₜ[ℂ] contrCoUnit.hom (1 : ℂ)))) = x := by
+  obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span complexCoBasis x)
+  subst hc
+  rw [contrCoUnit_apply_one, contrCoUnitVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom,
+    Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    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 complexCo) (z :  CoeSort.coe complexContr) :
+    (α_ complexCo.V complexContr.V complexCo.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl
+  repeat rw [h1']
+  have h1'' ( y :  CoeSort.coe complexCo) (z :  CoeSort.coe complexCo ⊗[ℂ] CoeSort.coe complexContr) :
+    (coContrContraction.hom ▷ complexCo.V) (z ⊗ₜ[ℂ] y) = (coContrContraction.hom z) ⊗ₜ[ℂ] y := rfl
+  repeat rw (config := { transparency := .instances }) [h1'']
+  repeat rw [coContrContraction_basis']
+  simp only [Fin.isValue, leftUnitor, ModuleCat.MonoidalCategory.leftUnitor, ModuleCat.of_coe,
+    CategoryTheory.Iso.trans_hom, LinearEquiv.toModuleIso_hom, ModuleCat.ofSelfIso_hom,
+    CategoryTheory.Category.comp_id, Action.instMonoidalCategory_tensorUnit_V, ↓reduceIte,
+    reduceCtorEq, zero_tmul, map_zero, smul_zero, add_zero, Sum.inr.injEq, one_ne_zero,
+    Fin.reduceEq, zero_add, zero_ne_one]
+  erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul, TensorProduct.lid_tmul,
+    TensorProduct.lid_tmul]
+  simp only [Fin.isValue, one_smul]
+  repeat rw [add_assoc]
+
+/-- Contraction on the right with `coContrUnit`. -/
+lemma contr_coContrUnit (x : complexContr) :
+    (λ_ complexContr).hom.hom
+    ((contrCoContraction ▷ complexContr).hom
+    ((α_ _ _ complexContr).inv.hom
+    (x ⊗ₜ[ℂ] coContrUnit.hom (1 : ℂ)))) = x := by
+  obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span complexContrBasis x)
+  subst hc
+  rw [coContrUnit_apply_one, coContrUnitVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom,
+    Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    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) :
+    (α_ 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) :
+    (contrCoContraction.hom ▷ complexContr.V) (z ⊗ₜ[ℂ] y) = (contrCoContraction.hom z) ⊗ₜ[ℂ] y := rfl
+  repeat rw (config := { transparency := .instances }) [h1'']
+  repeat rw [contrCoContraction_basis']
+  simp only [Fin.isValue, Action.instMonoidalCategory_tensorUnit_V, ↓reduceIte, reduceCtorEq,
+    zero_tmul, map_zero, smul_zero, add_zero, Sum.inr.injEq, one_ne_zero, Fin.reduceEq, zero_add,
+    zero_ne_one]
+  erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul, TensorProduct.lid_tmul,
+    TensorProduct.lid_tmul]
+  simp only [Fin.isValue, one_smul]
+  repeat rw [add_assoc]
+
 
 end Lorentz
 end

HepLean/SpaceTime/WeylFermion/Unit.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 LLMLean
 /-!
 
 # Units of Weyl fermions
@@ -221,11 +222,108 @@ lemma altRightRightUnit_apply_one : altRightRightUnit.hom (1 : ℂ) = altRightRi
 
 -/
 
-lemma contr_leftAltLeftUnitVal (x : leftHanded) :
+/-- Contraction on the right with `altLeftLeftUnit` does nothing. -/
+lemma contr_altLeftLeftUnit (x : leftHanded) :
     (λ_ leftHanded).hom.hom
     (((leftAltContraction) ▷ leftHanded).hom
     ((α_ _ _ leftHanded).inv.hom
     (x ⊗ₜ[ℂ] altLeftLeftUnit.hom (1 : ℂ)))) = x := by
-  sorry
+  obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span leftBasis x)
+  subst hc
+  rw [altLeftLeftUnit_apply_one, altLeftLeftUnitVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom,
+    Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    Fin.sum_univ_two, Fin.isValue, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add,
+    _root_.map_smul]
+  have h1 (x y : leftHanded) (z : altLeftHanded) : (leftAltContraction.hom ▷ leftHanded.V)
+    ((α_ leftHanded.V altLeftHanded.V leftHanded.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y)) =
+    (leftAltContraction.hom (x ⊗ₜ[ℂ] z)) ⊗ₜ[ℂ] y := rfl
+  erw [h1, h1, h1, h1]
+  repeat rw [leftAltContraction_basis]
+  simp only [Fin.isValue, leftUnitor, ModuleCat.MonoidalCategory.leftUnitor, ModuleCat.of_coe,
+    CategoryTheory.Iso.trans_hom, LinearEquiv.toModuleIso_hom, ModuleCat.ofSelfIso_hom,
+    CategoryTheory.Category.comp_id, Action.instMonoidalCategory_tensorUnit_V, Fin.val_zero,
+    ↓reduceIte, Fin.val_one, one_ne_zero, zero_tmul, map_zero, smul_zero, add_zero, zero_ne_one,
+    zero_add]
+  erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]
+  simp only [Fin.isValue, one_smul]
+
+/-- Contraction on the right with `leftAltLeftUnit` does nothing. -/
+lemma contr_leftAltLeftUnit  (x : altLeftHanded) :
+    (λ_ altLeftHanded).hom.hom
+    (((altLeftContraction) ▷ altLeftHanded).hom
+    ((α_ _ _ altLeftHanded).inv.hom
+    (x ⊗ₜ[ℂ] leftAltLeftUnit.hom (1 : ℂ)))) = x := by
+  obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span altLeftBasis x)
+  subst hc
+  rw [leftAltLeftUnit_apply_one, leftAltLeftUnitVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom,
+    Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    Fin.sum_univ_two, Fin.isValue, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add,
+    _root_.map_smul]
+  have h1 (x y : altLeftHanded) (z : leftHanded) : (altLeftContraction.hom ▷ altLeftHanded.V)
+    ((α_ altLeftHanded.V leftHanded.V altLeftHanded.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y)) =
+    (altLeftContraction.hom (x ⊗ₜ[ℂ] z)) ⊗ₜ[ℂ] y := rfl
+  erw [h1, h1, h1, h1]
+  repeat rw [altLeftContraction_basis]
+  simp only [Fin.isValue, Action.instMonoidalCategory_tensorUnit_V, Fin.val_zero, ↓reduceIte,
+    Fin.val_one, one_ne_zero, zero_tmul, map_zero, smul_zero, add_zero, zero_ne_one, zero_add]
+  erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]
+  simp only [Fin.isValue, one_smul]
+
+/-- Contraction on the right with `altRightRightUnit` does nothing. -/
+lemma contr_altRightRightUnit (x : rightHanded) :
+    (λ_ rightHanded).hom.hom
+    (((rightAltContraction) ▷ rightHanded).hom
+    ((α_ _ _ rightHanded).inv.hom
+    (x ⊗ₜ[ℂ] altRightRightUnit.hom (1 : ℂ)))) = x := by
+  obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span rightBasis x)
+  subst hc
+  rw [altRightRightUnit_apply_one, altRightRightUnitVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom,
+    Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    Fin.sum_univ_two, Fin.isValue, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add,
+    _root_.map_smul]
+  have h1 (x y : rightHanded) (z : altRightHanded) : (rightAltContraction.hom ▷ rightHanded.V)
+    ((α_ rightHanded.V altRightHanded.V rightHanded.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y)) =
+    (rightAltContraction.hom (x ⊗ₜ[ℂ] z)) ⊗ₜ[ℂ] y := rfl
+  erw [h1, h1, h1, h1]
+  repeat rw [rightAltContraction_basis]
+  simp only [Fin.isValue, Action.instMonoidalCategory_tensorUnit_V, Fin.val_zero, ↓reduceIte,
+    Fin.val_one, one_ne_zero, zero_tmul, map_zero, smul_zero, add_zero, zero_ne_one, zero_add]
+  erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]
+  simp only [Fin.isValue, one_smul]
+
+/-- Contraction on the right with `rightAltRightUnit` does nothing. -/
+lemma contr_rightAltRightUnit (x : altRightHanded) :
+    (λ_ altRightHanded).hom.hom
+    (((altRightContraction) ▷ altRightHanded).hom
+    ((α_ _ _ altRightHanded).inv.hom
+    (x ⊗ₜ[ℂ] rightAltRightUnit.hom (1 : ℂ)))) = x := by
+  obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span altRightBasis x)
+  subst hc
+  rw [rightAltRightUnit_apply_one, rightAltRightUnitVal_expand_tmul]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom,
+    Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    Fin.sum_univ_two, Fin.isValue, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add,
+    _root_.map_smul]
+  have h1 (x y : altRightHanded) (z : rightHanded) : (altRightContraction.hom ▷ altRightHanded.V)
+    ((α_ altRightHanded.V rightHanded.V altRightHanded.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y)) =
+    (altRightContraction.hom (x ⊗ₜ[ℂ] z)) ⊗ₜ[ℂ] y := rfl
+  erw [h1, h1, h1, h1]
+  repeat rw [altRightContraction_basis]
+  simp only [Fin.isValue, Action.instMonoidalCategory_tensorUnit_V, Fin.val_zero, ↓reduceIte,
+    Fin.val_one, one_ne_zero, zero_tmul, map_zero, smul_zero, add_zero, zero_ne_one, zero_add]
+  erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]
+  simp only [Fin.isValue, one_smul]
+
 end
 end Fermion

HepLean/Tensors/ComplexLorentz/Basic.lean

@@ -167,6 +167,14 @@ def complexLorentzTensor : TensorSpecies where
     | Color.downR => Fermion.altRightContraction_tmul_symm
     | Color.up => Lorentz.contrCoContraction_tmul_symm
     | Color.down => Lorentz.coContrContraction_tmul_symm
+  contr_unit := fun c =>
+    match c with
+    | Color.upL => Fermion.contr_altLeftLeftUnit
+    | Color.downL => Fermion.contr_leftAltLeftUnit
+    | Color.upR => Fermion.contr_altRightRightUnit
+    | Color.downR => Fermion.contr_rightAltRightUnit
+    | Color.up => Lorentz.contr_coContrUnit
+    | Color.down => Lorentz.contr_contrCoUnit
 
 instance : DecidableEq complexLorentzTensor.C := Fermion.instDecidableEqColor