Merge pull request #187 from HEPLean/IndexNotation

feat: Contraction of indices
2024-10-11 16:19:20 +00:00 · 2024-10-11 16:19:20 +00:00 · 115ec7dfa0
commit 115ec7dfa0
parent 1a5bff7254 bdff1b2704
12 changed files with 593 additions and 142 deletions
--- a/HepLean.lean
+++ b/HepLean.lean
@ -91,7 +91,6 @@ import HepLean.SpaceTime.LorentzVector.NormOne
 import HepLean.SpaceTime.MinkowskiMetric
 import HepLean.SpaceTime.SL2C.Basic
 import HepLean.SpaceTime.WeylFermion.Basic
-import HepLean.SpaceTime.WeylFermion.ColorFun
 import HepLean.SpaceTime.WeylFermion.Modules
 import HepLean.StandardModel.Basic
 import HepLean.StandardModel.HiggsBoson.Basic
@ -100,7 +99,11 @@ import HepLean.StandardModel.HiggsBoson.PointwiseInnerProd
 import HepLean.StandardModel.HiggsBoson.Potential
 import HepLean.StandardModel.Representations
 import HepLean.Tensors.Basic
-import HepLean.Tensors.ColorCat.Basic
+import HepLean.Tensors.ComplexLorentz.Basic
+import HepLean.Tensors.ComplexLorentz.ColorFun
+import HepLean.Tensors.ComplexLorentz.ContrNatTransform
+import HepLean.Tensors.ComplexLorentz.Examples
+import HepLean.Tensors.ComplexLorentz.TensorStruct
 import HepLean.Tensors.Contraction
 import HepLean.Tensors.EinsteinNotation.Basic
 import HepLean.Tensors.EinsteinNotation.IndexNotation
@ -123,6 +126,9 @@ import HepLean.Tensors.IndexNotation.IndexList.Subperm
 import HepLean.Tensors.IndexNotation.IndexString
 import HepLean.Tensors.IndexNotation.TensorIndex
 import HepLean.Tensors.MulActionTensor
+import HepLean.Tensors.OverColor.Basic
+import HepLean.Tensors.OverColor.Functors
+import HepLean.Tensors.OverColor.Iso
 import HepLean.Tensors.RisingLowering
 import HepLean.Tensors.Tree.Basic
 import HepLean.Tensors.Tree.Dot
--- a/HepLean/Tensors/ComplexLorentz/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basic.lean
@ -0,0 +1,63 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.OverColor.Basic
+import HepLean.Mathematics.PiTensorProduct
+/-!
+
+## Complex Lorentz tensors
+
+-/
+
+namespace Fermion
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+
+/-- The colors associated with complex representations of SL(2, ℂ) of intrest to physics. -/
+inductive Color
+  | upL : Color
+  | downL : Color
+  | upR : Color
+  | downR : Color
+  | up : Color
+  | down : Color
+
+/-- The involution taking a colour to its dual. -/
+def τ : Color → Color
+  | Color.upL => Color.downL
+  | Color.downL => Color.upL
+  | Color.upR => Color.downR
+  | Color.downR => Color.upR
+  | Color.up => Color.down
+  | Color.down => Color.up
+
+/-- The function taking a color to the dimension of the basis of vectors. -/
+def evalNo : Color → ℕ
+  | Color.upL => 2
+  | Color.downL => 2
+  | Color.upR => 2
+  | Color.downR => 2
+  | Color.up => 4
+  | Color.down => 4
+
+noncomputable section
+/-- The corresponding representations associated with a color. -/
+def colorToRep (c : Color) : Rep ℂ SL(2, ℂ) :=
+  match c with
+  | Color.upL => Fermion.altLeftHanded
+  | Color.downL => Fermion.leftHanded
+  | Color.upR => Fermion.altRightHanded
+  | Color.downR => Fermion.rightHanded
+  | Color.up => Lorentz.complexContr
+  | Color.down => Lorentz.complexCo
+
+end
+end Fermion
--- a/HepLean/Tensors/ComplexLorentz/ColorFun.lean
+++ b/HepLean/Tensors/ComplexLorentz/ColorFun.lean
@ -3,7 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.Tensors.ColorCat.Basic
+import HepLean.Tensors.ComplexLorentz.Basic
+import HepLean.Tensors.OverColor.Basic
 import HepLean.Mathematics.PiTensorProduct
 /-!

@ -21,25 +22,6 @@ open TensorProduct
 open IndexNotation
 open CategoryTheory

-/-- The colors associated with complex representations of SL(2, ℂ) of intrest to physics. -/
-inductive Color
-  | upL : Color
-  | downL : Color
-  | upR : Color
-  | downR : Color
-  | up : Color
-  | down : Color
-
-/-- The corresponding representations associated with a color. -/
-def colorToRep (c : Color) : Rep ℂ SL(2, ℂ) :=
-  match c with
-  | Color.upL => altLeftHanded
-  | Color.downL => leftHanded
-  | Color.upR => altRightHanded
-  | Color.downR => rightHanded
-  | Color.up => Lorentz.complexContr
-  | Color.down => Lorentz.complexCo
-
 /-- The linear equivalence between `colorToRep c1` and `colorToRep c2` when `c1 = c2`. -/
 def colorToRepCongr {c1 c2 : Color} (h : c1 = c2) : colorToRep c1 ≃ₗ[ℂ] colorToRep c2 where
  toFun := Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)
@ -177,6 +159,12 @@ lemma map_tprod {X Y : OverColor Color} (p : (i : X.left) → (colorToRep (X.hom
      ((PiTensorProduct.tprod ℂ) p)) = _
  rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod]

+lemma obj_ρ_tprod (f : OverColor Color) (M : SL(2, ℂ))
+    (x : (i : f.left) → CoeSort.coe (colorToRep (f.hom i))) :
+    (colorFun.obj f).ρ M ((PiTensorProduct.tprod ℂ) x) =
+    PiTensorProduct.tprod ℂ (fun i => (colorToRep (f.hom i)).ρ M (x i)) := by
+  exact obj'_ρ_tprod _ _ _
+
@[simp]
 lemma obj_ρ_empty (g : SL(2, ℂ)) : (colorFun.obj (𝟙_ (OverColor Color))).ρ g = LinearMap.id := by
  erw [colorFun.obj'_ρ]
--- a/HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean
+++ b/HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean
@ -0,0 +1,108 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.OverColor.Basic
+import HepLean.Tensors.OverColor.Functors
+import HepLean.Tensors.ComplexLorentz.ColorFun
+import HepLean.Mathematics.PiTensorProduct
+/-!
+
+## The contraction monoidal natural transformation
+
+-/
+
+namespace Fermion
+
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+
+namespace pairwiseRepFun
+
+/-- Given an object `c : OverColor Color` the representation defined by
+  `⨂[R] x, colorToRep (c.hom x) ⊗[R] colorToRep (τ (c.hom x))`. -/
+def obj' (c : OverColor Color) : Rep ℂ SL(2, ℂ) := Rep.of {
+  toFun := fun M => PiTensorProduct.map (fun x =>
+    TensorProduct.map ((colorToRep (c.hom x)).ρ M) ((colorToRep (τ (c.hom x))).ρ M)),
+  map_one' := by
+    simp
+  map_mul' := fun x y => by
+    simp only [Functor.id_obj, _root_.map_mul]
+    ext x' : 2
+    simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.map_tprod, LinearMap.mul_apply]
+    apply congrArg
+    funext i
+    change _ = (TensorProduct.map _ _ ∘ₗ TensorProduct.map _ _) (x' i)
+    rw [← TensorProduct.map_comp]
+    rfl}
+
+/-- Given a morphism in `OverColor Color` the corresopnding linear equivalence between `obj' _`
+  induced by reindexing. -/
+def mapToLinearEquiv' {f g : OverColor Color} (m : f ⟶ g) : (obj' f).V ≃ₗ[ℂ] (obj' g).V :=
+  (PiTensorProduct.reindex ℂ (fun x => (colorToRep (f.hom x)).V ⊗[ℂ] (colorToRep (τ (f.hom x))).V)
+  (OverColor.Hom.toEquiv m)).trans
+  (PiTensorProduct.congr (fun i =>
+    TensorProduct.congr (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i))
+    ((colorToRepCongr (congrArg τ (OverColor.Hom.toEquiv_symm_apply m i))))))
+
+lemma mapToLinearEquiv'_tprod {f g : OverColor Color} (m : f ⟶ g)
+    (x : (i : f.left) → (colorToRep (f.hom i)).V ⊗[ℂ] (colorToRep (τ (f.hom i))).V) :
+    mapToLinearEquiv' m (PiTensorProduct.tprod ℂ x) =
+    PiTensorProduct.tprod ℂ fun i =>
+    (TensorProduct.congr (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i))
+    (colorToRepCongr (mapToLinearEquiv'.proof_4 m i))) (x ((OverColor.Hom.toEquiv m).symm i)) := by
+  simp [mapToLinearEquiv']
+  change (PiTensorProduct.congr fun i => TensorProduct.congr (colorToRepCongr _)
+    (colorToRepCongr _)) ((PiTensorProduct.reindex ℂ
+    (fun x => ↑(colorToRep (f.hom x)).V ⊗[ℂ] ↑(colorToRep (τ (f.hom x))).V)
+    (OverColor.Hom.toEquiv m)) ((PiTensorProduct.tprod ℂ) x)) = _
+  rw [PiTensorProduct.reindex_tprod]
+  erw [PiTensorProduct.congr_tprod]
+  rfl
+
+end pairwiseRepFun
+
+/-
+
+def contrPairPairwiseRep (c : OverColor Color) :
+    (colorFunMon.obj c) ⊗ colorFunMon.obj ((OverColor.map τ).obj c) ⟶
+    pairwiseRep c where
+  hom := TensorProduct.lift (PiTensorProduct.map₂ (fun x =>
+      TensorProduct.mk ℂ (colorToRep (c.hom x)).V (colorToRep (τ (c.hom x))).V))
+  comm M := by
+    refine HepLean.PiTensorProduct.induction_tmul (fun x y => ?_)
+    simp only [Functor.id_obj, CategoryStruct.comp, Action.instMonoidalCategory_tensorObj_V,
+      Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+      Action.FunctorCategoryEquivalence.functor_obj_obj, Action.tensor_ρ', LinearMap.coe_comp,
+      Function.comp_apply]
+    change (TensorProduct.lift
+      (PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V
+      ↑(colorToRep (τ (c.hom x))).V))
+      ((TensorProduct.map _ _)
+      ((PiTensorProduct.tprod ℂ) x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) y)) = _
+    rw [TensorProduct.map_tmul]
+    erw [colorFun.obj_ρ_tprod, colorFun.obj_ρ_tprod]
+    simp only [Functor.id_obj, lift.tmul]
+    erw [PiTensorProduct.map₂_tprod_tprod]
+    change _ = ((pairwiseRep c).ρ M)
+      ((TensorProduct.lift
+        (PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V
+        ↑(colorToRep (τ (c.hom x))).V))
+      ((PiTensorProduct.tprod ℂ) x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) y))
+    simp only [mk_apply, Functor.id_obj, lift.tmul]
+    rw [PiTensorProduct.map₂_tprod_tprod]
+    simp only [pairwiseRep, Functor.id_obj, Rep.coe_of, Rep.of_ρ, MonoidHom.coe_mk, OneHom.coe_mk,
+      mk_apply]
+    erw [PiTensorProduct.map_tprod]
+    rfl
+-/
+end
+end Fermion
--- a/HepLean/Tensors/ComplexLorentz/Examples.lean
+++ b/HepLean/Tensors/ComplexLorentz/Examples.lean
@ -0,0 +1,41 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.Tree.Basic
+import HepLean.Tensors.ComplexLorentz.TensorStruct
+import HepLean.Tensors.Tree.Elab
+/-!
+
+## The tensor structure for complex Lorentz tensors
+
+-/
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open IndexNotation
+open CategoryTheory
+
+noncomputable section
+
+namespace complexLorentzTensor
+
+/-- The color map for a 2d tensor with the first index up and the second index down. -/
+def upDown : Fin 2 → complexLorentzTensor.C
+  | 0 => Fermion.Color.up
+  | 1 => Fermion.Color.down
+
+variable (T S : complexLorentzTensor.F.obj (OverColor.mk upDown))
+
+/-
+#check {T | i m ⊗ S | m l}ᵀ.dot
+#check {T | i m ⊗ S | l τ(m)}ᵀ.dot
+-/
+end complexLorentzTensor
+
+end
--- a/HepLean/Tensors/ComplexLorentz/TensorStruct.lean
+++ b/HepLean/Tensors/ComplexLorentz/TensorStruct.lean
@ -0,0 +1,36 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.Tree.Basic
+import HepLean.Tensors.ComplexLorentz.ColorFun
+/-!
+
+## The tensor structure for complex Lorentz tensors
+
+-/
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open IndexNotation
+open CategoryTheory
+
+noncomputable section
+
+/-- The tensor structure for complex Lorentz tensors. -/
+def complexLorentzTensor : TensorStruct where
+  C := Fermion.Color
+  G := SL(2, ℂ)
+  G_group := inferInstance
+  k := ℂ
+  k_commRing := inferInstance
+  F := Fermion.colorFunMon
+  τ := Fermion.τ
+  evalNo := Fermion.evalNo
+
+end
--- a/HepLean/Tensors/OverColor/Basic.lean
+++ b/HepLean/Tensors/OverColor/Basic.lean
@ -13,7 +13,7 @@ import HepLean.SpaceTime.WeylFermion.Basic
 import HepLean.SpaceTime.LorentzVector.Complex
 /-!

-## Over category.
+## Over color category.

 -/

@ -65,6 +65,17 @@ lemma toEquiv_comp_inv_apply (m : f ⟶ g) (i : g.left) :
    f.hom ((OverColor.Hom.toEquiv m).symm i) = g.hom i := by
  simpa [toEquiv, types_comp] using congrFun m.inv.w i

+/-- Given a morphism in `OverColor C`, the corresponding isomorphism. -/
+def toIso (m : f ⟶ g) : f ≅ g := {
+  hom := m,
+  inv := m.symm,
+  hom_inv_id := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    simp only [CategoryStruct.comp, Iso.self_symm_id, Iso.refl_hom, Over.id_left, types_id_apply]
+    rfl,
+  inv_hom_id := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    simp only [CategoryStruct.comp, Iso.symm_self_id, Iso.refl_hom, Over.id_left, types_id_apply]
+    rfl}
+
 end Hom

 section monoidal
@ -234,116 +245,6 @@ def mk (f : X → C) : OverColor C := Over.mk f

 open MonoidalCategory

-/-- The monoidal functor from `OverColor C` to `OverColor D` constructed from a map
-  `f : C → D`. -/
-def map {C D : Type} (f : C → D) : MonoidalFunctor (OverColor C) (OverColor D) where
-  toFunctor := Core.functorToCore (Core.inclusion (Over C) ⋙ (Over.map f))
-  ε := Over.isoMk (Iso.refl _) (by
-    ext x
-    exact Empty.elim x)
-  μ X Y := Over.isoMk (Iso.refl _) (by
-    ext x
-    match x with
-    | Sum.inl x => rfl
-    | Sum.inr x => rfl)
-  μ_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl x => rfl
-    | Sum.inr x => rfl
-  μ_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl x => rfl
-    | Sum.inr x => rfl
-  associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl (Sum.inl x) => rfl
-    | Sum.inl (Sum.inr x) => rfl
-    | Sum.inr x => rfl
-  left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl x => rfl
-    | Sum.inr x => rfl
-  right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl x => rfl
-    | Sum.inr x => rfl
-
-/-- The tensor product on `OverColor C` as a monoidal functor. -/
-def tensor : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where
-  toFunctor := MonoidalCategory.tensor (OverColor C)
-  ε := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso (by
-    ext x
-    exact Empty.elim x)
-  μ X Y := Over.isoMk (Equiv.sumSumSumComm X.1.left X.2.left Y.1.left Y.2.left).toIso (by
-    ext x
-    match x with
-    | Sum.inl (Sum.inl x) => rfl
-    | Sum.inl (Sum.inr x) => rfl
-    | Sum.inr (Sum.inl x) => rfl
-    | Sum.inr (Sum.inr x) => rfl)
-  μ_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl (Sum.inl x) => rfl
-    | Sum.inl (Sum.inr x) => rfl
-    | Sum.inr (Sum.inl x) => rfl
-    | Sum.inr (Sum.inr x) => rfl
-  μ_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl (Sum.inl x) => rfl
-    | Sum.inl (Sum.inr x) => rfl
-    | Sum.inr (Sum.inl x) => rfl
-    | Sum.inr (Sum.inr x) => rfl
-  associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl (Sum.inl (Sum.inl x)) => rfl
-    | Sum.inl (Sum.inl (Sum.inr x)) => rfl
-    | Sum.inl (Sum.inr (Sum.inl x)) => rfl
-    | Sum.inl (Sum.inr (Sum.inr x)) => rfl
-    | Sum.inr (Sum.inl x) => rfl
-    | Sum.inr (Sum.inr x) => rfl
-  left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl x => exact Empty.elim x
-    | Sum.inr (Sum.inl x)=> rfl
-    | Sum.inr (Sum.inr x)=> rfl
-  right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl (Sum.inl x) => rfl
-    | Sum.inl (Sum.inr x) => rfl
-    | Sum.inr x => exact Empty.elim x
-
-/-!
-
-## Useful equivalences.
-
-/
-
-/-- The isomorphism between `c : X → C` and `c ∘ e.symm` as objects in `OverColor C` for an
-  equivalence `e`. -/
-def equivToIso {c : X → C} (e : X ≃ Y) : mk c ≅ mk (c ∘ e.symm) := {
-  hom := Over.isoMk e.toIso ((Iso.eq_inv_comp e.toIso).mp rfl),
-  inv := (Over.isoMk e.toIso ((Iso.eq_inv_comp e.toIso).mp rfl)).symm,
-  hom_inv_id := by
-    apply CategoryTheory.Iso.ext
-    erw [CategoryTheory.Iso.trans_hom]
-    simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
-    rfl,
-  inv_hom_id := by
-    apply CategoryTheory.Iso.ext
-    erw [CategoryTheory.Iso.trans_hom]
-    simp only [Iso.symm_hom, Iso.inv_hom_id]
-    rfl}
-
-/-- The equivalence between `Fin n.succ` and `Fin 1 ⊕ Fin n` extracting the
-  `i`th component. -/
-def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
-  (finCongr (by omega : n.succ = i + 1 + (n - i))).trans <|
-  finSumFinEquiv.symm.trans <|
-  (Equiv.sumCongr (finSumFinEquiv.symm.trans (Equiv.sumComm (Fin i) (Fin 1)))
-    (Equiv.refl (Fin (n-i)))).trans <|
-  (Equiv.sumAssoc (Fin 1) (Fin i) (Fin (n - i))).trans <|
-  Equiv.sumCongr (Equiv.refl (Fin 1)) (finSumFinEquiv.trans (finCongr (by omega)))
-
 end OverColor

 end IndexNotation
--- a/HepLean/Tensors/OverColor/Functors.lean
+++ b/HepLean/Tensors/OverColor/Functors.lean
@ -0,0 +1,132 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.OverColor.Basic
+/-!
+
+## Functors related to the OverColor category
+
+-/
+namespace IndexNotation
+namespace OverColor
+open CategoryTheory
+open MonoidalCategory
+
+/-- The monoidal functor from `OverColor C` to `OverColor D` constructed from a map
+  `f : C → D`. -/
+def map {C D : Type} (f : C → D) : MonoidalFunctor (OverColor C) (OverColor D) where
+  toFunctor := Core.functorToCore (Core.inclusion (Over C) ⋙ (Over.map f))
+  ε := Over.isoMk (Iso.refl _) (by
+    ext x
+    exact Empty.elim x)
+  μ X Y := Over.isoMk (Iso.refl _) (by
+    ext x
+    match x with
+    | Sum.inl x => rfl
+    | Sum.inr x => rfl)
+  μ_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    match x with
+    | Sum.inl x => rfl
+    | Sum.inr x => rfl
+  μ_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    match x with
+    | Sum.inl x => rfl
+    | Sum.inr x => rfl
+  associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    match x with
+    | Sum.inl (Sum.inl x) => rfl
+    | Sum.inl (Sum.inr x) => rfl
+    | Sum.inr x => rfl
+  left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    match x with
+    | Sum.inl x => rfl
+    | Sum.inr x => rfl
+  right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    match x with
+    | Sum.inl x => rfl
+    | Sum.inr x => rfl
+
+/-- The tensor product on `OverColor C` as a monoidal functor. -/
+def tensor (C : Type) : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where
+  toFunctor := MonoidalCategory.tensor (OverColor C)
+  ε := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso (by
+    ext x
+    exact Empty.elim x)
+  μ X Y := Over.isoMk (Equiv.sumSumSumComm X.1.left X.2.left Y.1.left Y.2.left).toIso (by
+    ext x
+    match x with
+    | Sum.inl (Sum.inl x) => rfl
+    | Sum.inl (Sum.inr x) => rfl
+    | Sum.inr (Sum.inl x) => rfl
+    | Sum.inr (Sum.inr x) => rfl)
+  μ_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    match x with
+    | Sum.inl (Sum.inl x) => rfl
+    | Sum.inl (Sum.inr x) => rfl
+    | Sum.inr (Sum.inl x) => rfl
+    | Sum.inr (Sum.inr x) => rfl
+  μ_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    match x with
+    | Sum.inl (Sum.inl x) => rfl
+    | Sum.inl (Sum.inr x) => rfl
+    | Sum.inr (Sum.inl x) => rfl
+    | Sum.inr (Sum.inr x) => rfl
+  associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    match x with
+    | Sum.inl (Sum.inl (Sum.inl x)) => rfl
+    | Sum.inl (Sum.inl (Sum.inr x)) => rfl
+    | Sum.inl (Sum.inr (Sum.inl x)) => rfl
+    | Sum.inl (Sum.inr (Sum.inr x)) => rfl
+    | Sum.inr (Sum.inl x) => rfl
+    | Sum.inr (Sum.inr x) => rfl
+  left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    match x with
+    | Sum.inl x => exact Empty.elim x
+    | Sum.inr (Sum.inl x)=> rfl
+    | Sum.inr (Sum.inr x)=> rfl
+  right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    match x with
+    | Sum.inl (Sum.inl x) => rfl
+    | Sum.inl (Sum.inr x) => rfl
+    | Sum.inr x => exact Empty.elim x
+
+/-- The monoidal functor from `OverColor C` to `OverColor C × OverColor C` landing on the
+  diagonal. -/
+def diag (C : Type) : MonoidalFunctor (OverColor C) (OverColor C × OverColor C) :=
+  MonoidalFunctor.diag (OverColor C)
+
+/-- The constant monoidal functor from `OverColor C` to itself landing on `𝟙_ (OverColor C)`. -/
+def const (C : Type) : MonoidalFunctor (OverColor C) (OverColor C) where
+  toFunctor := (Functor.const (OverColor C)).obj (𝟙_ (OverColor C))
+  ε := 𝟙 (𝟙_ (OverColor C))
+  μ _ _:= (λ_ (𝟙_ (OverColor C))).hom
+  μ_natural_left _ _ := by
+    simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerRight_id,
+      Category.id_comp, Iso.hom_inv_id, Category.comp_id]
+  μ_natural_right _ _ := by
+    simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerLeft_id,
+      Category.id_comp, Category.comp_id]
+  associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
+    match i with
+    | Sum.inl (Sum.inl i) => rfl
+    | Sum.inl (Sum.inr i) => rfl
+    | Sum.inr i => rfl
+  left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
+    match i with
+    | Sum.inl i => exact Empty.elim i
+    | Sum.inr i => exact Empty.elim i
+  right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
+    match i with
+    | Sum.inl i => exact Empty.elim i
+    | Sum.inr i => exact Empty.elim i
+
+/-- The monoidal functor from `OverColor C` to `OverColor C` taking `f` to `f ⊗ τ_* f`. -/
+def contrPair (C : Type) (τ : C → C) : MonoidalFunctor (OverColor C) (OverColor C) :=
+  OverColor.diag C
+  ⊗⋙ (MonoidalFunctor.prod (MonoidalFunctor.id (OverColor C)) (OverColor.map τ))
+  ⊗⋙ OverColor.tensor C
+
+end OverColor
+end IndexNotation
--- a/HepLean/Tensors/OverColor/Iso.lean
+++ b/HepLean/Tensors/OverColor/Iso.lean
@ -0,0 +1,174 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.OverColor.Functors
+/-!
+
+## Isomorphisms in the OverColor category
+
+-/
+namespace IndexNotation
+namespace OverColor
+open CategoryTheory
+open MonoidalCategory
+
+/-!
+
+## Useful equivalences.
+
+-/
+
+/-- The isomorphism between `c : X → C` and `c ∘ e.symm` as objects in `OverColor C` for an
+  equivalence `e`. -/
+def equivToIso {c : X → C} (e : X ≃ Y) : mk c ≅ mk (c ∘ e.symm) :=
+  Hom.toIso (Over.isoMk e.toIso ((Iso.eq_inv_comp e.toIso).mp rfl))
+
+/-- Given a map `X ⊕ Y → C`, the isomorphism `mk c ≅ mk (c ∘ Sum.inl) ⊗ mk (c ∘ Sum.inr)`. -/
+def mkSum (c : X ⊕ Y → C) : mk c ≅ mk (c ∘ Sum.inl) ⊗ mk (c ∘ Sum.inr) :=
+  Hom.toIso (Over.isoMk (Equiv.refl _).toIso (by
+    ext x
+    match x with
+    | Sum.inl x => rfl
+    | Sum.inr x => rfl))
+
+/-- The isomorphism between objects in `OverColor C` given equality of maps. -/
+def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 :=
+  Hom.toIso (Over.isoMk (Equiv.refl _).toIso (by
+    subst h
+    rfl))
+
+/-- The equivalence between `Fin n.succ` and `Fin 1 ⊕ Fin n` extracting the
+  `i`th component. -/
+def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
+  (finCongr (by omega : n.succ = i + 1 + (n - i))).trans <|
+  finSumFinEquiv.symm.trans <|
+  (Equiv.sumCongr (finSumFinEquiv.symm.trans (Equiv.sumComm (Fin i) (Fin 1)))
+    (Equiv.refl (Fin (n-i)))).trans <|
+  (Equiv.sumAssoc (Fin 1) (Fin i) (Fin (n - i))).trans <|
+  Equiv.sumCongr (Equiv.refl (Fin 1)) (finSumFinEquiv.trans (finCongr (by omega)))
+
+lemma finExtractOne_symm_inr {n : ℕ} (i : Fin n.succ) :
+    (finExtractOne i).symm ∘ Sum.inr = i.succAbove := by
+  ext x
+  simp only [Nat.succ_eq_add_one, finExtractOne, Function.comp_apply, Equiv.symm_trans_apply,
+    finCongr_symm, Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply,
+    Equiv.coe_refl, Sum.map_inr, finCongr_apply, Fin.coe_cast]
+  change (finSumFinEquiv
+    (Sum.map (⇑(finSumFinEquiv.symm.trans (Equiv.sumComm (Fin ↑i) (Fin 1))).symm) id
+    ((Equiv.sumAssoc (Fin 1) (Fin ↑i) (Fin (n - i))).symm
+    (Sum.inr (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)))))).val = _
+  by_cases hi : x.1 < i.1
+  · have h1 : (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)) =
+        Sum.inl ⟨x, hi⟩ := by
+      rw [← finSumFinEquiv_symm_apply_castAdd]
+      apply congrArg
+      ext
+      simp
+    rw [h1]
+    simp only [Nat.succ_eq_add_one, Equiv.sumAssoc_symm_apply_inr_inl, Sum.map_inl,
+      Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.sumComm_symm, Equiv.sumComm_apply,
+      Sum.swap_inr, finSumFinEquiv_apply_left, Fin.castAdd_mk]
+    rw [Fin.succAbove]
+    split
+    · rfl
+    rename_i hn
+    simp_all only [Nat.succ_eq_add_one, not_lt, Fin.le_def, Fin.coe_castSucc, Fin.val_succ,
+      self_eq_add_right, one_ne_zero]
+    omega
+  · have h1 : (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)) =
+        Sum.inr ⟨x - i, by omega⟩ := by
+      rw [← finSumFinEquiv_symm_apply_natAdd]
+      apply congrArg
+      ext
+      simp only [Nat.succ_eq_add_one, Fin.coe_cast, Fin.natAdd_mk]
+      omega
+    rw [h1, Fin.succAbove]
+    split
+    · rename_i hn
+      simp_all [Fin.lt_def]
+    simp only [Nat.succ_eq_add_one, Equiv.sumAssoc_symm_apply_inr_inr, Sum.map_inr, id_eq,
+      finSumFinEquiv_apply_right, Fin.natAdd_mk, Fin.val_succ]
+    omega
+
+@[simp]
+lemma finExtractOne_symm_inr_apply {n : ℕ} (i : Fin n.succ) (x : Fin n) :
+    (finExtractOne i).symm (Sum.inr x) = i.succAbove x := calc
+  _ = ((finExtractOne i).symm ∘ Sum.inr) x := rfl
+  _ = i.succAbove x := by rw [finExtractOne_symm_inr]
+
+@[simp]
+lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
+    (finExtractOne i).symm (Sum.inl 0) = i := by
+  simp only [Nat.succ_eq_add_one, finExtractOne, Fin.isValue, Equiv.symm_trans_apply, finCongr_symm,
+    Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply, Equiv.coe_refl,
+    Sum.map_inl, id_eq, Equiv.sumAssoc_symm_apply_inl, Equiv.sumComm_symm, Equiv.sumComm_apply,
+    Sum.swap_inl, finSumFinEquiv_apply_right, finSumFinEquiv_apply_left, finCongr_apply]
+  ext
+  rfl
+
+/-- The equivalence of types `Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n` extracting
+  the `i` and `(i.succAbove j)`. -/
+def finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
+    Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n :=
+  (finExtractOne i).trans <|
+  (Equiv.sumCongr (Equiv.refl (Fin 1)) (finExtractOne j)).trans <|
+  (Equiv.sumAssoc (Fin 1) (Fin 1) (Fin n)).symm
+
+lemma finExtractTwo_symm_inr {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
+    (finExtractTwo i j).symm ∘ Sum.inr = i.succAbove ∘ j.succAbove := by
+  rw [finExtractTwo]
+  ext1 x
+  simp
+
+@[simp]
+lemma finExtractTwo_symm_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) (x : Fin n) :
+    (finExtractTwo i j).symm (Sum.inr x) = i.succAbove (j.succAbove x) := by
+  rw [finExtractTwo]
+  simp
+
+@[simp]
+lemma finExtractTwo_symm_inl_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
+    (finExtractTwo i j).symm (Sum.inl (Sum.inr 0)) = i.succAbove j := by
+  rw [finExtractTwo]
+  simp
+
+@[simp]
+lemma finExtractTwo_symm_inl_inl_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
+    (finExtractTwo i j).symm (Sum.inl (Sum.inl 0)) = i := by
+  rw [finExtractTwo]
+  simp
+
+/-- The isomorphism between a `Fin 1 ⊕ Fin 1 → C` satisfying the condition
+  `c (Sum.inr 0) = τ (c (Sum.inl 0))`
+  and an object in the image of `contrPair`. -/
+def contrPairFin1Fin1 (τ : C → C) (c : Fin 1 ⊕ Fin 1 → C)
+    (h : c (Sum.inr 0) = τ (c (Sum.inl 0))) :
+    OverColor.mk c ≅ (contrPair C τ).obj (OverColor.mk (fun (_ : Fin 1) => c (Sum.inl 0))) :=
+  Hom.toIso (Over.isoMk (Equiv.refl _).toIso (by
+    ext x
+    match x with
+    | Sum.inl x =>
+      fin_cases x
+      rfl
+    | Sum.inr x =>
+      fin_cases x
+      change _ = c (Sum.inr 0)
+      rw [h]
+      rfl))
+
+/-- The Isomorphism between a `Fin n.succ.succ → C` and the product containing an object in the
+  image of `contrPair` based on the given values. -/
+def contrPairEquiv {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin n.succ.succ)
+    (j : Fin n.succ) (h : c (i.succAbove j) = τ (c i)) :
+    OverColor.mk c ≅ ((contrPair C τ).obj (Over.mk (fun (_ : Fin 1) => c i))) ⊗
+    (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
+  (equivToIso (finExtractTwo i j)).trans <|
+  (OverColor.mkSum (c ∘ ⇑(finExtractTwo i j).symm)).trans <|
+  tensorIso
+    (contrPairFin1Fin1 τ ((c ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inl) (by simpa using h)) <|
+    mkIso (by ext x; simp)
+
+end OverColor
+end IndexNotation
--- a/HepLean/Tensors/Tree/Basic.lean
+++ b/HepLean/Tensors/Tree/Basic.lean
@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.Tensors.ColorCat.Basic
+import HepLean.Tensors.OverColor.Iso
 import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
 /-!

@ -13,6 +13,7 @@ import Mathlib.CategoryTheory.Monoidal.NaturalTransformation

 open IndexNotation
 open CategoryTheory
+open MonoidalCategory

 /-- The sturcture of a type of tensors e.g. Lorentz tensors, Einstien tensors,
  complex Lorentz tensors.
@ -33,9 +34,9 @@ structure TensorStruct where
  F : MonoidalFunctor (OverColor C) (Rep k G)
  /-- A map from `C` to `C`. An involution. -/
  τ : C → C
-  /-- A monoidal natural isomorphism from OverColor.map τ ⊗⋙ F to F.
-    This will allow us to, for example, rise and lower indices. -/
-  dual : (OverColor.map τ ⊗⋙ F) ≅ F
+  /-
+  μContr : OverColor.contrPair C τ ⊗⋙ F ⟶ OverColor.const C ⊗⋙ F
+  dual : (OverColor.map τ ⊗⋙ F) ≅ F-/
  /-- A specification of the dimension of each color in C. This will be used for explicit
    evaluation of tensors. -/
  evalNo : C → ℕ
@ -63,7 +64,8 @@ inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Typ
    (i : Fin n.succ) → (j : Fin m.succ) → TensorTree S c → TensorTree S c1 →
    TensorTree S (Sum.elim (c ∘ Fin.succAbove i) (c1 ∘ Fin.succAbove j) ∘ finSumFinEquiv.symm)
  | contr {n : ℕ} {c : Fin n.succ.succ → S.C} : (i : Fin n.succ.succ) →
-    (j : Fin n.succ) → TensorTree S c → TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
+    (j : Fin n.succ) → (h : c (i.succAbove j) = S.τ (c i)) → TensorTree S c →
+    TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
  | jiggle {n : ℕ} {c : Fin n → S.C} : (i : Fin n) → TensorTree S c →
    TensorTree S (Function.update c i (S.τ (c i)))
  | eval {n : ℕ} {c : Fin n.succ → S.C} :
@ -85,7 +87,7 @@ def size : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → ℕ := fun
  | smul _ t => t.size + 1
  | prod t1 t2 => t1.size + t2.size + 1
  | mult _ _ t1 t2 => t1.size + t2.size + 1
-  | contr _ _ t => t.size + 1
+  | contr _ _ _ t => t.size + 1
  | jiggle _ t => t.size + 1
  | eval _ _ t => t.size + 1

--- a/HepLean/Tensors/Tree/Dot.lean
+++ b/HepLean/Tensors/Tree/Dot.lean
@ -53,7 +53,7 @@ def dotString (m : ℕ) (nt : ℕ) : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTr
    let jiggleNode := " node" ++ toString m ++ " [label=\"τ\", shape=box];\n"
    let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
    jiggleNode ++ dotString (m + 1) nt t1 ++ edge1
-  | contr i j t1 =>
+  | contr i j _ t1 =>
    let contrNode := " node" ++ toString m ++ " [label=\"contr " ++ toString i ++ " "
      ++ toString j ++ "\", shape=box];\n"
    let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@ -192,7 +192,7 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
 /-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.contr` to the given term. -/
 def contrSyntax (l : List (ℕ × ℕ)) (T : Term) : Term :=
  l.foldl (fun T' (x0, x1) => Syntax.mkApp (mkIdent ``TensorTree.contr)
-    #[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), T']) T
+    #[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), mkIdent ``rfl, T']) T

 /-- Creates the syntax associated with a tensor node. -/
 def syntaxFull (stx : Syntax) : TermElabM Term := do
@ -256,7 +256,7 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
 /-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.contr` to the given term. -/
 def contrSyntax (l : List (ℕ × ℕ)) (T : Term) : Term :=
  l.foldl (fun T' (x0, x1) => Syntax.mkApp (mkIdent ``TensorTree.contr)
-    #[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), T']) T
+    #[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), mkIdent ``rfl, T']) T

 /-- The syntax associated with a product of tensors. -/
 def prodSyntax (T1 T2 : Term) : Term :=