From 8c584431c40764c5ac3d56c3b4b046c645d4d684 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 24 Oct 2024 16:04:05 +0000
Subject: [PATCH] feat: Add symm of unit for complex lorentz

---
 .../SpaceTime/LorentzVector/Complex/Unit.lean | 22 ++++++++++++
 HepLean/SpaceTime/WeylFermion/Unit.lean       | 35 +++++++++++++++++++
 HepLean/Tensors/ComplexLorentz/Basic.lean     |  9 +++++
 3 files changed, 66 insertions(+)

diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean b/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean
index 1fdea5d..43fff62 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean
+++ b/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean
@@ -193,6 +193,28 @@ lemma contr_coContrUnit (x : complexContr) :
   simp only [Fin.isValue, one_smul]
   repeat rw [add_assoc]
 
+/-!
+
+## Symmetry properties of the units
+
+-/
+
+
+open CategoryTheory
+
+lemma contrCoUnit_symm :
+    (contrCoUnit.hom (1 : ℂ)) = (complexContr ◁ 𝟙 _).hom ((β_ complexCo complexContr).hom.hom
+    (coContrUnit.hom (1 : ℂ))) := by
+  rw [contrCoUnit_apply_one, contrCoUnitVal_expand_tmul]
+  rw [coContrUnit_apply_one, coContrUnitVal_expand_tmul]
+  rfl
+
+lemma coContrUnit_symm :
+    (coContrUnit.hom (1 : ℂ)) = (complexCo ◁ 𝟙 _).hom ((β_ complexContr complexCo).hom.hom
+    (contrCoUnit.hom (1 : ℂ))) := by
+  rw [coContrUnit_apply_one, coContrUnitVal_expand_tmul]
+  rw [contrCoUnit_apply_one, contrCoUnitVal_expand_tmul]
+  rfl
 
 end Lorentz
 end
diff --git a/HepLean/SpaceTime/WeylFermion/Unit.lean b/HepLean/SpaceTime/WeylFermion/Unit.lean
index b67e111..38d74d3 100644
--- a/HepLean/SpaceTime/WeylFermion/Unit.lean
+++ b/HepLean/SpaceTime/WeylFermion/Unit.lean
@@ -325,5 +325,40 @@ lemma contr_rightAltRightUnit (x : altRightHanded) :
   erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]
   simp only [Fin.isValue, one_smul]
 
+/-!
+
+## Symmetry properties of the units
+
+-/
+open CategoryTheory
+
+lemma altLeftLeftUnit_symm :
+    (altLeftLeftUnit.hom (1 : ℂ)) = (altLeftHanded ◁ 𝟙 _).hom ((β_ leftHanded altLeftHanded ).hom.hom
+    (leftAltLeftUnit.hom (1 : ℂ))) := by
+  rw [altLeftLeftUnit_apply_one, altLeftLeftUnitVal_expand_tmul]
+  rw [leftAltLeftUnit_apply_one, leftAltLeftUnitVal_expand_tmul]
+  rfl
+
+lemma leftAltLeftUnit_symm :
+    (leftAltLeftUnit.hom (1 : ℂ)) = (leftHanded ◁ 𝟙 _).hom ((β_ altLeftHanded leftHanded ).hom.hom
+    (altLeftLeftUnit.hom (1 : ℂ))) := by
+  rw [altLeftLeftUnit_apply_one, altLeftLeftUnitVal_expand_tmul]
+  rw [leftAltLeftUnit_apply_one, leftAltLeftUnitVal_expand_tmul]
+  rfl
+
+lemma altRightRightUnit_symm :
+    (altRightRightUnit.hom (1 : ℂ)) = (altRightHanded ◁ 𝟙 _).hom ((β_ rightHanded altRightHanded ).hom.hom
+    (rightAltRightUnit.hom (1 : ℂ))) := by
+  rw [altRightRightUnit_apply_one, altRightRightUnitVal_expand_tmul]
+  rw [rightAltRightUnit_apply_one, rightAltRightUnitVal_expand_tmul]
+  rfl
+
+lemma rightAltRightUnit_symm :
+    (rightAltRightUnit.hom (1 : ℂ)) = (rightHanded ◁ 𝟙 _).hom ((β_ altRightHanded rightHanded ).hom.hom
+    (altRightRightUnit.hom (1 : ℂ))) := by
+  rw [altRightRightUnit_apply_one, altRightRightUnitVal_expand_tmul]
+  rw [rightAltRightUnit_apply_one, rightAltRightUnitVal_expand_tmul]
+  rfl
+
 end
 end Fermion
diff --git a/HepLean/Tensors/ComplexLorentz/Basic.lean b/HepLean/Tensors/ComplexLorentz/Basic.lean
index 57fcf69..3d76eaf 100644
--- a/HepLean/Tensors/ComplexLorentz/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basic.lean
@@ -175,6 +175,15 @@ def complexLorentzTensor : TensorSpecies where
     | Color.downR => Fermion.contr_rightAltRightUnit
     | Color.up => Lorentz.contr_coContrUnit
     | Color.down => Lorentz.contr_contrCoUnit
+  unit_symm := fun c =>
+    match c with
+    | Color.upL => Fermion.altLeftLeftUnit_symm
+    | Color.downL => Fermion.leftAltLeftUnit_symm
+    | Color.upR => Fermion.altRightRightUnit_symm
+    | Color.downR => Fermion.rightAltRightUnit_symm
+    | Color.up => Lorentz.coContrUnit_symm
+    | Color.down => Lorentz.contrCoUnit_symm
+  contr_metric := by sorry
 
 instance : DecidableEq complexLorentzTensor.C := Fermion.instDecidableEqColor