Merge pull request #210 from HEPLean/IndexNotation

feat: Additional axioms to TensorSpecies
2024-10-24 18:08:31 +00:00 · 2024-10-24 18:08:31 +00:00 · 5f1fb57efd
commit 5f1fb57efd
parent 16fb8fa5bc 9ec5746451
12 changed files with 606 additions and 14 deletions
--- a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
+++ b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
@ -52,7 +52,7 @@ lemma toSelfAdjointMatrix_apply_coe (x : LorentzVector 3) : (toSelfAdjointMatrix
    - x (Sum.inr 1) • PauliMatrix.σ2
    - x (Sum.inr 2) • PauliMatrix.σ3 := by
  rw [toSelfAdjointMatrix_apply]
-  simp only [Fin.isValue, AddSubgroupClass.coe_sub, selfAdjoint.val_smul]
+  rfl

 lemma toSelfAdjointMatrix_stdBasis (i : Fin 1 ⊕ Fin 3) :
    toSelfAdjointMatrix (LorentzVector.stdBasis i) = PauliMatrix.σSAL i := by
@ -68,21 +68,21 @@ lemma toSelfAdjointMatrix_stdBasis (i : Fin 1 ⊕ Fin 3) :
    simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
      Pi.single_eq_same, one_smul, zero_sub, Sum.inr.injEq, one_ne_zero, sub_zero, Fin.reduceEq,
      PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
-    refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl)
+    rfl
  | Sum.inr 1 =>
    simp only [LorentzVector.stdBasis, Fin.isValue]
    erw [Pi.basisFun_apply]
    simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
      Sum.inr.injEq, zero_ne_one, sub_self, Pi.single_eq_same, one_smul, zero_sub, Fin.reduceEq,
      sub_zero, PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
-    refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl)
+    rfl
  | Sum.inr 2 =>
    simp only [LorentzVector.stdBasis, Fin.isValue]
    erw [Pi.basisFun_apply]
    simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
      Sum.inr.injEq, Fin.reduceEq, sub_self, Pi.single_eq_same, one_smul, zero_sub,
      PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
-    refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl)
+    rfl

@[simp]
 lemma toSelfAdjointMatrix_symm_basis (i : Fin 1 ⊕ Fin 3) :
--- a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
+++ b/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
@ -44,7 +44,6 @@ def complexContrBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexContr := Basis.ofEqui
 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]
@ -72,7 +71,6 @@ def complexCoBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexCo := Basis.ofEquivFun
@[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]
--- a/HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean
+++ b/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
--- a/HepLean/SpaceTime/LorentzVector/Complex/Metric.lean
+++ b/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,63 @@ 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
--- a/HepLean/SpaceTime/LorentzVector/Complex/Two.lean
+++ b/HepLean/SpaceTime/LorentzVector/Complex/Two.lean
@ -66,6 +66,18 @@ def contrCoToMatrix : (complexContr ⊗ complexCo).V ≃ₗ[ℂ]
  Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
  LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)

+/-- Expansion of `contrCoToMatrix` in terms of the standard basis. -/
+lemma contrCoToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) :
+    contrCoToMatrix.symm M = ∑ i, ∑ j, M i j • (complexContrBasis i ⊗ₜ[ℂ] complexCoBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, contrCoToMatrix, LinearEquiv.trans_symm,
+    LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply complexContrBasis complexCoBasis i j]
+    rfl
+  · simp
+
 /-- Equivalence of `complexCo ⊗ complexContr` to `4 x 4` complex matrices. -/
 def coContrToMatrix : (complexCo ⊗ complexContr).V ≃ₗ[ℂ]
    Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
@ -73,6 +85,18 @@ def coContrToMatrix : (complexCo ⊗ complexContr).V ≃ₗ[ℂ]
  Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
  LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)

+/-- Expansion of `coContrToMatrix` in terms of the standard basis. -/
+lemma coContrToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) :
+    coContrToMatrix.symm M = ∑ i, ∑ j, M i j • (complexCoBasis i ⊗ₜ[ℂ] complexContrBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, coContrToMatrix, LinearEquiv.trans_symm,
+    LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply complexCoBasis complexContrBasis i j]
+    rfl
+  · simp
+
 /-!

 ## Group actions
--- a/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean
+++ b/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
@ -23,6 +24,20 @@ namespace Lorentz
 def contrCoUnitVal : (complexContr ⊗ complexCo).V :=
  contrCoToMatrix.symm 1

+/-- Expansion of `contrCoUnitVal` into basis. -/
+lemma contrCoUnitVal_expand_tmul : contrCoUnitVal =
+    complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)
+    + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)
+    + complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)
+    + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, contrCoUnitVal, Fin.isValue]
+  erw [contrCoToMatrix_symm_expand_tmul]
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three, ne_eq, reduceCtorEq, not_false_eq_true, one_apply_ne,
+    zero_smul, add_zero, one_apply_eq, one_smul, zero_add, Sum.inr.injEq, zero_ne_one, Fin.reduceEq,
+    one_ne_zero]
+  rfl
+
 /-- The contra-co unit for complex lorentz vectors as a morphism
  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo`, manifesting the invaraince under
  the `SL(2, ℂ)` action. -/
@ -51,10 +66,29 @@ def contrCoUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo where
    apply congrArg
    simp

+lemma contrCoUnit_apply_one : contrCoUnit.hom (1 : ℂ) = contrCoUnitVal := by
+  change contrCoUnit.hom.toFun (1 : ℂ) = contrCoUnitVal
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    contrCoUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+
 /-- The co-contra unit for complex lorentz vectors. Usually denoted `δᵢⁱ`. -/
 def coContrUnitVal : (complexCo ⊗ complexContr).V :=
  coContrToMatrix.symm 1

+/-- Expansion of `coContrUnitVal` into basis. -/
+lemma coContrUnitVal_expand_tmul : coContrUnitVal =
+    complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)
+    + complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)
+    + complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)
+    + complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, coContrUnitVal, Fin.isValue]
+  erw [coContrToMatrix_symm_expand_tmul]
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three, ne_eq, reduceCtorEq, not_false_eq_true, one_apply_ne,
+    zero_smul, add_zero, one_apply_eq, one_smul, zero_add, Sum.inr.injEq, zero_ne_one, Fin.reduceEq,
+    one_ne_zero]
+  rfl
+
 /-- The co-contra unit for complex lorentz vectors as a morphism
  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr`, manifesting the invaraince under
  the `SL(2, ℂ)` action. -/
@ -85,5 +119,105 @@ def coContrUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr where
    refine transpose_eq_one.mp ?h.h.h.a
    simp

+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]
+
+/-!
+
+## 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
--- a/HepLean/SpaceTime/PauliMatrices/AsTensor.lean
+++ b/HepLean/SpaceTime/PauliMatrices/AsTensor.lean
@ -41,10 +41,6 @@ lemma asTensor_expand_complexContrBasis : asTensor =
    + complexContrBasis (Sum.inr 0) ⊗ₜ leftRightToMatrix.symm (σSA (Sum.inr 0))
    + complexContrBasis (Sum.inr 1) ⊗ₜ leftRightToMatrix.symm (σSA (Sum.inr 1))
    + complexContrBasis (Sum.inr 2) ⊗ₜ leftRightToMatrix.symm (σSA (Sum.inr 2)) := by
-  simp only [Action.instMonoidalCategory_tensorObj_V, asTensor,
-    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]
  rfl

 /-- The expansion of the pauli matrix `σ₀` in terms of a basis of tensor product vectors. -/
--- a/HepLean/SpaceTime/WeylFermion/Basic.lean
+++ b/HepLean/SpaceTime/WeylFermion/Basic.lean
@ -61,7 +61,6 @@ lemma leftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
@[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
@ -94,7 +93,6 @@ def altLeftBasis : Basis (Fin 2) ℂ altLeftHanded := Basis.ofEquivFun
@[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]
@ -132,7 +130,6 @@ def rightBasis : Basis (Fin 2) ℂ rightHanded := Basis.ofEquivFun
@[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]
@ -174,7 +171,6 @@ def altRightBasis : Basis (Fin 2) ℂ altRightHanded := Basis.ofEquivFun
@[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]
--- a/HepLean/SpaceTime/WeylFermion/Metric.lean
+++ b/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,120 @@ 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
--- a/HepLean/SpaceTime/WeylFermion/Unit.lean
+++ b/HepLean/SpaceTime/WeylFermion/Unit.lean
@ -28,6 +28,14 @@ open CategoryTheory.MonoidalCategory
 def leftAltLeftUnitVal : (leftHanded ⊗ altLeftHanded).V :=
  leftAltLeftToMatrix.symm 1

+/-- Expansion of `leftAltLeftUnitVal` into the basis. -/
+lemma leftAltLeftUnitVal_expand_tmul : leftAltLeftUnitVal =
+    leftBasis 0 ⊗ₜ[ℂ] altLeftBasis 0 + leftBasis 1 ⊗ₜ[ℂ] altLeftBasis 1 := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, leftAltLeftUnitVal, Fin.isValue]
+  erw [leftAltLeftToMatrix_symm_expand_tmul]
+  simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one,
+    not_false_eq_true, one_apply_ne, zero_smul, add_zero, one_ne_zero, zero_add]
+
 /-- The left-alt-left unit `δᵃₐ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded `,
  manifesting the invariance under the `SL(2,ℂ)` action. -/
 def leftAltLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded where
@ -55,10 +63,23 @@ def leftAltLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded
    apply congrArg
    simp

+lemma leftAltLeftUnit_apply_one : leftAltLeftUnit.hom (1 : ℂ) = leftAltLeftUnitVal := by
+  change leftAltLeftUnit.hom.toFun (1 : ℂ) = leftAltLeftUnitVal
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    leftAltLeftUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+
 /-- The alt-left-left unit `δₐᵃ` as an element of `(altLeftHanded ⊗ leftHanded).V`. -/
 def altLeftLeftUnitVal : (altLeftHanded ⊗ leftHanded).V :=
  altLeftLeftToMatrix.symm 1

+/-- Expansion of `altLeftLeftUnitVal` into the basis. -/
+lemma altLeftLeftUnitVal_expand_tmul : altLeftLeftUnitVal =
+    altLeftBasis 0 ⊗ₜ[ℂ] leftBasis 0 + altLeftBasis 1 ⊗ₜ[ℂ] leftBasis 1 := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, altLeftLeftUnitVal, Fin.isValue]
+  erw [altLeftLeftToMatrix_symm_expand_tmul]
+  simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one,
+    not_false_eq_true, one_apply_ne, zero_smul, add_zero, one_ne_zero, zero_add]
+
 /-- The alt-left-left unit `δₐᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded `,
  manifesting the invariance under the `SL(2,ℂ)` action. -/
 def altLeftLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded where
@ -87,11 +108,24 @@ def altLeftLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded
    simp only [mul_one, ← transpose_mul, SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq,
      one_ne_zero, not_false_eq_true, mul_nonsing_inv, transpose_one]

+lemma altLeftLeftUnit_apply_one : altLeftLeftUnit.hom (1 : ℂ) = altLeftLeftUnitVal := by
+  change altLeftLeftUnit.hom.toFun (1 : ℂ) = altLeftLeftUnitVal
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    altLeftLeftUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+
 /-- The right-alt-right unit `δ^{dot a}_{dot a}` as an element of
  `(rightHanded ⊗ altRightHanded).V`. -/
 def rightAltRightUnitVal : (rightHanded ⊗ altRightHanded).V :=
  rightAltRightToMatrix.symm 1

+/-- Expansion of `rightAltRightUnitVal` into the basis. -/
+lemma rightAltRightUnitVal_expand_tmul : rightAltRightUnitVal =
+    rightBasis 0 ⊗ₜ[ℂ] altRightBasis 0 + rightBasis 1 ⊗ₜ[ℂ] altRightBasis 1 := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, rightAltRightUnitVal, Fin.isValue]
+  erw [rightAltRightToMatrix_symm_expand_tmul]
+  simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one,
+    not_false_eq_true, one_apply_ne, zero_smul, add_zero, one_ne_zero, zero_add]
+
 /-- The right-alt-right unit `δ^{dot a}_{dot a}` as a morphism
  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHanded`, manifesting
  the invariance under the `SL(2,ℂ)` action. -/
@ -126,11 +160,24 @@ def rightAltRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHa
    rw [@conjTranspose_nonsing_inv]
    simp

+lemma rightAltRightUnit_apply_one : rightAltRightUnit.hom (1 : ℂ) = rightAltRightUnitVal := by
+  change rightAltRightUnit.hom.toFun (1 : ℂ) = rightAltRightUnitVal
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    rightAltRightUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+
 /-- The alt-right-right unit `δ_{dot a}^{dot a}` as an element of
  `(rightHanded ⊗ altRightHanded).V`. -/
 def altRightRightUnitVal : (altRightHanded ⊗ rightHanded).V :=
  altRightRightToMatrix.symm 1

+/-- Expansion of `altRightRightUnitVal` into the basis. -/
+lemma altRightRightUnitVal_expand_tmul : altRightRightUnitVal =
+    altRightBasis 0 ⊗ₜ[ℂ] rightBasis 0 + altRightBasis 1 ⊗ₜ[ℂ] rightBasis 1 := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, altRightRightUnitVal, Fin.isValue]
+  erw [altRightRightToMatrix_symm_expand_tmul]
+  simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one,
+    not_false_eq_true, one_apply_ne, zero_smul, add_zero, one_ne_zero, zero_add]
+
 /-- The alt-right-right unit `δ_{dot a}^{dot a}` as a morphism
  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHanded`, manifesting
  the invariance under the `SL(2,ℂ)` action. -/
@ -163,5 +210,154 @@ def altRightRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHa
    rw [@conjTranspose_nonsing_inv]
    simp

+lemma altRightRightUnit_apply_one : altRightRightUnit.hom (1 : ℂ) = altRightRightUnitVal := by
+  change altRightRightUnit.hom.toFun (1 : ℂ) = altRightRightUnitVal
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    altRightRightUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+
+/-!
+
+## Contraction of the units
+
+-/
+
+/-- 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
+  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]
+
+/-!
+
+## 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
--- a/HepLean/Tensors/ComplexLorentz/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basic.lean
@ -167,6 +167,30 @@ 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
+  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 := 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

--- a/HepLean/Tensors/Tree/Basic.lean
+++ b/HepLean/Tensors/Tree/Basic.lean
@ -55,6 +55,32 @@ structure TensorSpecies where
      (y : FDiscrete.obj (Discrete.mk (τ c))) :
    (contr.app (Discrete.mk c)).hom (x ⊗ₜ[k] y) = (contr.app (Discrete.mk (τ c))).hom
      (y ⊗ₜ (FDiscrete.map (Discrete.eqToHom (τ_involution c).symm)).hom x)
+  /-- Contraction with unit leaves invariant. -/
+  contr_unit (c : C) (x : FDiscrete.obj (Discrete.mk (c))) :
+    (λ_ (FDiscrete.obj (Discrete.mk (c)))).hom.hom
+    (((contr.app (Discrete.mk c)) ▷ (FDiscrete.obj (Discrete.mk (c)))).hom
+    ((α_ _ _ (FDiscrete.obj (Discrete.mk (c)))).inv.hom
+    (x ⊗ₜ[k] (unit.app (Discrete.mk c)).hom (1 : k)))) = x
+  /-- The unit is symmetric. -/
+  unit_symm (c : C) :
+    ((unit.app (Discrete.mk c)).hom (1 : k)) =
+    ((FDiscrete.obj (Discrete.mk (τ (c)))) ◁
+      (FDiscrete.map (Discrete.eqToHom (τ_involution c)))).hom
+    ((β_ (FDiscrete.obj (Discrete.mk (τ (τ c)))) (FDiscrete.obj (Discrete.mk (τ (c))))).hom.hom
+    ((unit.app (Discrete.mk (τ c))).hom (1 : k)))
+  /-- On contracting metrics we get back the unit. -/
+  contr_metric (c : C) :
+    (β_ (FDiscrete.obj (Discrete.mk c)) (FDiscrete.obj (Discrete.mk (τ c)))).hom.hom
+    (((FDiscrete.obj (Discrete.mk c)) ◁ (λ_ (FDiscrete.obj (Discrete.mk (τ c)))).hom).hom
+    (((FDiscrete.obj (Discrete.mk c)) ◁ ((contr.app (Discrete.mk c)) ▷
+    (FDiscrete.obj (Discrete.mk (τ c))))).hom
+    (((FDiscrete.obj (Discrete.mk c)) ◁ (α_ (FDiscrete.obj (Discrete.mk (c)))
+      (FDiscrete.obj (Discrete.mk (τ c))) (FDiscrete.obj (Discrete.mk (τ c)))).inv).hom
+    ((α_ (FDiscrete.obj (Discrete.mk (c))) (FDiscrete.obj (Discrete.mk (c)))
+      (FDiscrete.obj (Discrete.mk (τ c)) ⊗ FDiscrete.obj (Discrete.mk (τ c)))).hom.hom
+    ((metric.app (Discrete.mk c)).hom (1 : k) ⊗ₜ[k]
+      (metric.app (Discrete.mk (τ c))).hom (1 : k))))))
+    = (unit.app (Discrete.mk c)).hom (1 : k)

 noncomputable section