From d02e94886d4c30df8ac574de6537ee369d411907 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 6 Aug 2024 15:43:58 -0400
Subject: [PATCH] feat: Double contraction of indices lemma

---
 HepLean.lean                                  |   1 -
 HepLean/SpaceTime/LorentzTensor/Basic.lean    | 138 +++++---
 .../SpaceTime/LorentzTensor/Contraction.lean  | 310 ++++++++++++------
 HepLean/SpaceTime/LorentzTensor/Fin.lean      | 110 -------
 .../LorentzTensor/IndexNotation/Basic.lean    |  20 ++
 .../IndexNotation/IndexListColor.lean         |  37 +++
 .../IndexNotation/IndexString.lean            |   5 +-
 .../IndexNotation/TensorIndex.lean            |  80 ++++-
 .../LorentzTensor/Real/IndexNotation.lean     |   4 +-
 .../LorentzTensor/RisingLowering.lean         | 200 +++++------
 10 files changed, 543 insertions(+), 362 deletions(-)
 delete mode 100644 HepLean/SpaceTime/LorentzTensor/Fin.lean

diff --git a/HepLean.lean b/HepLean.lean
index 3c66e66..72a54e4 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -72,7 +72,6 @@ import HepLean.SpaceTime.LorentzGroup.Restricted
 import HepLean.SpaceTime.LorentzGroup.Rotations
 import HepLean.SpaceTime.LorentzTensor.Basic
 import HepLean.SpaceTime.LorentzTensor.Contraction
-import HepLean.SpaceTime.LorentzTensor.Fin
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexListColor
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexString
diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean
index 526001d..0807543 100644
--- a/HepLean/SpaceTime/LorentzTensor/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean
@@ -45,7 +45,7 @@ structure TensorColor where
 namespace TensorColor
 
 variable (𝓒 : TensorColor) [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
-variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
+variable {d : ℕ} {X X' Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
   [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
 
 /-- A relation on colors which is true if the two colors are equal or are duals. -/
@@ -95,6 +95,55 @@ instance (μ ν : 𝓒.Color) : Decidable (μ ≈ ν) :=
 
 instance : DecidableEq (Quotient 𝓒.colorSetoid) :=
   instDecidableEqQuotientOfDecidableEquiv
+
+/-- The types of maps from an `X` to `𝓒.Color`. -/
+def ColorMap (X : Type) := X → 𝓒.Color
+
+namespace ColorMap
+
+variable {𝓒 : TensorColor} [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
+
+variable (cX : ColorMap 𝓒 X) (cY : ColorMap 𝓒 Y) (cZ : ColorMap 𝓒 Z)
+
+def MapIso (e : X ≃ Y) (cX : ColorMap 𝓒 X) (cY : ColorMap 𝓒 Y) : Prop := cX = cY ∘ e
+
+def sum (cX : ColorMap 𝓒 X) (cY : ColorMap 𝓒 Y) : ColorMap 𝓒 (Sum X Y) :=
+  Sum.elim cX cY
+
+def dual (cX : ColorMap 𝓒 X) : ColorMap 𝓒 X := 𝓒.τ ∘ cX
+
+namespace MapIso
+
+variable {e : X ≃ Y} {e' : Y ≃ Z} {cX : ColorMap 𝓒 X} {cY : ColorMap 𝓒 Y} {cZ : ColorMap 𝓒 Z}
+variable {cX' : ColorMap 𝓒 X'} {cY' : ColorMap 𝓒 Y'}
+
+lemma symm (h : cX.MapIso e cY) : cY.MapIso e.symm cX := by
+  rw [MapIso] at h
+  exact (Equiv.eq_comp_symm e cY cX).mpr h.symm
+
+lemma trans (h : cX.MapIso e cY) (h' : cY.MapIso e' cZ) :
+    cX.MapIso (e.trans e') cZ:= by
+  funext a
+  subst h h'
+  simp
+
+lemma sum  {eX : X ≃ X'} {eY : Y ≃ Y'} (hX : cX.MapIso eX cX') (hY : cY.MapIso eY cY') :
+    (cX.sum cY).MapIso (eX.sumCongr eY) (cX'.sum cY') := by
+  funext x
+  subst hX hY
+  match x with
+  | Sum.inl x => rfl
+  | Sum.inr x => rfl
+
+lemma dual {e : X ≃ Y} (h : cX.MapIso e cY) :
+   cX.dual.MapIso e  cY.dual  := by
+  subst h
+  rfl
+
+end MapIso
+
+end ColorMap
+
 end TensorColor
 
 noncomputable section
@@ -179,8 +228,8 @@ variable (𝓣 : TensorStructure R)
 
 variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
   [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
-  {cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color}
-  {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν η : 𝓣.Color}
+  {cX cX2 : 𝓣.ColorMap X} {cY : 𝓣.ColorMap Y} {cZ : 𝓣.ColorMap Z}
+  {cW : 𝓣.ColorMap W} {cY' : 𝓣.ColorMap Y'} {μ ν η : 𝓣.Color}
 
 instance : AddCommMonoid (𝓣.ColorModule μ) := 𝓣.colorModule_addCommMonoid μ
 
@@ -188,7 +237,7 @@ instance : Module R (𝓣.ColorModule μ) := 𝓣.colorModule_module μ
 
 /-- The type of tensors given a map from an indexing set `X` to the type of colors,
   specifying the color of that index. -/
-def Tensor (c : X → 𝓣.Color) : Type := ⨂[R] x, 𝓣.ColorModule (c x)
+def Tensor (c : 𝓣.ColorMap X) : Type := ⨂[R] x, 𝓣.ColorModule (c x)
 
 instance : AddCommMonoid (𝓣.Tensor cX) :=
   PiTensorProduct.instAddCommMonoid fun i => 𝓣.ColorModule (cX i)
@@ -246,20 +295,14 @@ lemma tensorProd_piTensorProd_ext {M : Type} [AddCommMonoid M] [Module R M]
 -/
 
 /-- An linear equivalence of tensor spaces given a color-preserving equivalence of indexing sets. -/
-def mapIso {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = d ∘ e) :
+def mapIso {c : 𝓣.ColorMap X} {d : 𝓣.ColorMap Y} (e : X ≃ Y) (h : c.MapIso e d) :
     𝓣.Tensor c ≃ₗ[R] 𝓣.Tensor d :=
   (PiTensorProduct.reindex R _ e) ≪≫ₗ
   (PiTensorProduct.congr (fun y => 𝓣.colorModuleCast (by rw [h]; simp)))
 
-lemma mapIso_trans_cond {e : X ≃ Y} {e' : Y ≃ Z} (h : cX = cY ∘ e) (h' : cY = cZ ∘ e') :
-    cX = cZ ∘ (e.trans e') := by
-  funext a
-  subst h h'
-  simp
-
 @[simp]
-lemma mapIso_trans (e : X ≃ Y) (e' : Y ≃ Z) (h : cX = cY ∘ e) (h' : cY = cZ ∘ e') :
-    (𝓣.mapIso e h ≪≫ₗ 𝓣.mapIso e' h') = 𝓣.mapIso (e.trans e') (𝓣.mapIso_trans_cond h h') := by
+lemma mapIso_trans (e : X ≃ Y) (e' : Y ≃ Z) (h : cX.MapIso e cY) (h' : cY.MapIso e' cZ) :
+    (𝓣.mapIso e h ≪≫ₗ 𝓣.mapIso e' h') = 𝓣.mapIso (e.trans e') (h.trans h') := by
   refine LinearEquiv.toLinearMap_inj.mp ?_
   apply PiTensorProduct.ext
   apply MultilinearMap.ext
@@ -276,14 +319,14 @@ lemma mapIso_trans (e : X ≃ Y) (e' : Y ≃ Z) (h : cX = cY ∘ e) (h' : cY = c
   simp [colorModuleCast]
 
 @[simp]
-lemma mapIso_mapIso (e : X ≃ Y) (e' : Y ≃ Z) (h : cX = cY ∘ e) (h' : cY = cZ ∘ e')
+lemma mapIso_mapIso (e : X ≃ Y) (e' : Y ≃ Z) (h : cX.MapIso e cY) (h' : cY.MapIso e' cZ)
     (T : 𝓣.Tensor cX) :
-    (𝓣.mapIso e' h') (𝓣.mapIso e h T) = 𝓣.mapIso (e.trans e') (𝓣.mapIso_trans_cond h h') T := by
+    (𝓣.mapIso e' h') (𝓣.mapIso e h T) = 𝓣.mapIso (e.trans e') (h.trans h') T := by
   rw [← LinearEquiv.trans_apply, mapIso_trans]
 
 @[simp]
-lemma mapIso_symm (e : X ≃ Y) (h : cX = cY ∘ e) :
-    (𝓣.mapIso e h).symm = 𝓣.mapIso e.symm ((Equiv.eq_comp_symm e cY cX).mpr h.symm) := by
+lemma mapIso_symm (e : X ≃ Y) (h : cX.MapIso e cY) :
+    (𝓣.mapIso e h).symm = 𝓣.mapIso e.symm (h.symm) := by
   refine LinearEquiv.toLinearMap_inj.mp ?_
   apply PiTensorProduct.ext
   apply MultilinearMap.ext
@@ -321,10 +364,10 @@ lemma mapIso_refl : 𝓣.mapIso (Equiv.refl X) (rfl : cX = cX) = LinearEquiv.ref
   rfl
 
 @[simp]
-lemma mapIso_tprod {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = d ∘ e)
+lemma mapIso_tprod {c : 𝓣.ColorMap X} {d : 𝓣.ColorMap Y} (e : X ≃ Y) (h : c.MapIso e d)
     (f : (i : X) → 𝓣.ColorModule (c i)) : (𝓣.mapIso e h) (PiTensorProduct.tprod R f) =
     (PiTensorProduct.tprod R (fun i => 𝓣.colorModuleCast (by rw [h]; simp) (f (e.symm i)))) := by
-  simp [mapIso]
+  simp only [mapIso, LinearEquiv.trans_apply]
   change (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _)
     ((PiTensorProduct.reindex R _ e) ((PiTensorProduct.tprod R) f)) = _
   rw [PiTensorProduct.reindex_tprod]
@@ -523,26 +566,26 @@ lemma tensoratorEquiv_tmul_tprod (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor c
     lift.tmul, LinearMap.coe_mk, AddHom.coe_mk, PiTensorProduct.lift.tprod]
   exact PiTensorProduct.lift.tprod q
 
-lemma tensoratorEquiv_mapIso_cond {e : X ≃ Y} {e' : Z ≃ Y} {e'' : W ≃ X}
-    (h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : bW = cX ∘ e'') :
-    Sum.elim bW cZ = Sum.elim cX cY ∘ ⇑(e''.sumCongr e') := by
-  subst h h' h''
-  funext x
-  match x with
-  | Sum.inl x => rfl
-  | Sum.inr x => rfl
+@[simp]
+lemma tensoratorEquiv_symm_tprod (f : 𝓣.PureTensor (Sum.elim cX cY)) :
+    (𝓣.tensoratorEquiv cX cY).symm ((PiTensorProduct.tprod R) f) =
+    (PiTensorProduct.tprod R) (𝓣.inlPureTensor f) ⊗ₜ[R] (PiTensorProduct.tprod R) (𝓣.inrPureTensor f) := by
+  simp [tensoratorEquiv, tensorator]
+  change (PiTensorProduct.lift 𝓣.domCoprod) ((PiTensorProduct.tprod R) f) =  _
+  simp [domCoprod]
 
 @[simp]
-lemma tensoratorEquiv_mapIso (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X)
-    (h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : bW = cX ∘ e'') :
+lemma tensoratorEquiv_mapIso (e' : Z ≃ Y) (e'' : W ≃ X)
+    (h' : cZ.MapIso e' cY) (h'' : cW.MapIso e'' cX) :
     (TensorProduct.congr (𝓣.mapIso e'' h'') (𝓣.mapIso e' h')) ≪≫ₗ (𝓣.tensoratorEquiv cX cY)
-    = (𝓣.tensoratorEquiv bW cZ)
-    ≪≫ₗ (𝓣.mapIso (Equiv.sumCongr e'' e') (𝓣.tensoratorEquiv_mapIso_cond h h' h'')) := by
+    = (𝓣.tensoratorEquiv cW cZ) ≪≫ₗ (𝓣.mapIso (Equiv.sumCongr e'' e') (h''.sum h')) := by
   apply LinearEquiv.toLinearMap_inj.mp
   apply tensorProd_piTensorProd_ext
   intro p q
   simp only [LinearEquiv.coe_coe, LinearEquiv.trans_apply, congr_tmul, mapIso_tprod,
-    tensoratorEquiv_tmul_tprod, Equiv.sumCongr_symm, Equiv.sumCongr_apply]
+    tensoratorEquiv_tmul_tprod]
+  erw [LinearEquiv.trans_apply]
+  simp only [tensoratorEquiv_tmul_tprod, mapIso_tprod, Equiv.sumCongr_symm, Equiv.sumCongr_apply]
   apply congrArg
   funext x
   match x with
@@ -550,30 +593,26 @@ lemma tensoratorEquiv_mapIso (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X)
   | Sum.inr x => rfl
 
 @[simp]
-lemma tensoratorEquiv_mapIso_apply (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X)
-    (h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : cW = cX ∘ e'')
+lemma tensoratorEquiv_mapIso_apply (e' : Z ≃ Y) (e'' : W ≃ X)
+    (h' : cZ.MapIso e' cY) (h'' : cW.MapIso e'' cX)
     (x : 𝓣.Tensor cW ⊗[R] 𝓣.Tensor cZ) :
     (𝓣.tensoratorEquiv cX cY) ((TensorProduct.congr (𝓣.mapIso e'' h'') (𝓣.mapIso e' h')) x) =
-    (𝓣.mapIso (Equiv.sumCongr e'' e') (𝓣.tensoratorEquiv_mapIso_cond h h' h''))
+    (𝓣.mapIso (Equiv.sumCongr e'' e') (h''.sum h'))
     ((𝓣.tensoratorEquiv cW cZ) x) := by
   trans ((TensorProduct.congr (𝓣.mapIso e'' h'') (𝓣.mapIso e' h')) ≪≫ₗ
     (𝓣.tensoratorEquiv cX cY)) x
   rfl
   rw [tensoratorEquiv_mapIso]
   rfl
-  exact e
-  exact h
 
-lemma tensoratorEquiv_mapIso_tmul (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X)
-    (h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : cW = cX ∘ e'')
+lemma tensoratorEquiv_mapIso_tmul (e' : Z ≃ Y) (e'' : W ≃ X)
+    (h' : cZ.MapIso e' cY) (h'' : cW.MapIso e'' cX)
     (x : 𝓣.Tensor cW) (y : 𝓣.Tensor cZ) :
     (𝓣.tensoratorEquiv cX cY) ((𝓣.mapIso e'' h'' x) ⊗ₜ[R] (𝓣.mapIso e' h' y)) =
-    (𝓣.mapIso (Equiv.sumCongr e'' e') (𝓣.tensoratorEquiv_mapIso_cond h h' h''))
+    (𝓣.mapIso (Equiv.sumCongr e'' e') (h''.sum h'))
     ((𝓣.tensoratorEquiv cW cZ) (x ⊗ₜ y)) := by
   rw [← tensoratorEquiv_mapIso_apply]
   rfl
-  exact e
-  exact h
 
 /-!
 
@@ -626,9 +665,24 @@ lemma contrDual_symm_contrRightAux_apply_tmul (h : ν = η)
 
 /-!
 
+## Of empty
+
+-/
+
+def isEmptyEquiv [IsEmpty X] : 𝓣.Tensor cX ≃ₗ[R] R :=
+  PiTensorProduct.isEmptyEquiv X
+
+@[simp]
+def isEmptyEquiv_tprod [IsEmpty X] (f : 𝓣.PureTensor cX) :
+    𝓣.isEmptyEquiv (PiTensorProduct.tprod R f) = 1 := by
+  simp only [isEmptyEquiv]
+  erw [PiTensorProduct.isEmptyEquiv_apply_tprod]
+/-!
+
 ## Splitting tensors into tensor products
 
 -/
+/-! TODO: Delete the content of this section. -/
 
 /-- The decomposition of a set into a direct sum based on the image of an injection. -/
 def decompEmbedSet (f : Y ↪ X) :
diff --git a/HepLean/SpaceTime/LorentzTensor/Contraction.lean b/HepLean/SpaceTime/LorentzTensor/Contraction.lean
index e08da05..5479db3 100644
--- a/HepLean/SpaceTime/LorentzTensor/Contraction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Contraction.lean
@@ -40,6 +40,78 @@ open MulActionTensor
 
 variable {R : Type} [CommSemiring R]
 
+namespace TensorColor
+
+variable {d : ℕ} {X X' Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
+  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
+variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
+  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
+  [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P]
+
+namespace ColorMap
+
+variable {𝓒 : TensorColor} [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
+
+variable (cX : ColorMap 𝓒 X) (cY : ColorMap 𝓒 Y) (cZ : ColorMap 𝓒 Z)
+
+def ContrAll (e : X ≃ Y) (cX : ColorMap 𝓒 X) (cY : ColorMap 𝓒 Y) : Prop :=
+  cX = 𝓒.τ ∘ cY ∘ e
+
+namespace ContrAll
+
+variable {e : X ≃ Y} {e' : Y ≃ Z} {cX : ColorMap 𝓒 X} {cY : ColorMap 𝓒 Y} {cZ : ColorMap 𝓒 Z}
+variable {cX' : ColorMap 𝓒 X'} {cY' : ColorMap 𝓒 Y'}
+
+lemma toMapIso (h : cX.ContrAll e cY) : cX.MapIso e cY.dual := by
+  subst h
+  rfl
+
+lemma symm (h : cX.ContrAll e cY) : cY.ContrAll e.symm cX := by
+  subst h
+  funext x
+  simp only [Function.comp_apply, Equiv.apply_symm_apply]
+  exact (𝓒.τ_involutive (cY x)).symm
+
+lemma trans_mapIso {e : X ≃ Y} {e' : Z ≃ Y}
+    (h : cX.ContrAll e cY) (h' : cZ.MapIso e' cY) : cX.ContrAll (e.trans e'.symm) cZ  := by
+  subst h h'
+  funext x
+  simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply]
+
+lemma mapIso_trans {e : X ≃ Y} {e' : Z ≃ X}
+    (h : cX.ContrAll e cY) (h' : cZ.MapIso e' cX) : cZ.ContrAll (e'.trans e) cY := by
+  subst h h'
+  funext x
+  simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply]
+
+end ContrAll
+
+def contr (e : (C ⊕ C) ⊕ P ≃ X) (cX : ColorMap 𝓒 X) : ColorMap 𝓒 P :=
+  cX ∘ e ∘ Sum.inr
+
+def contrLeft (e : (C ⊕ C) ⊕ P ≃ X) (cX : ColorMap 𝓒 X) : ColorMap 𝓒 C :=
+  cX ∘ e ∘ Sum.inl ∘ Sum.inl
+
+def contrRight (e : (C ⊕ C) ⊕ P ≃ X) (cX : ColorMap 𝓒 X) : ColorMap 𝓒 C :=
+  cX ∘ e ∘ Sum.inl ∘ Sum.inr
+
+def ContrCond (e : (C ⊕ C) ⊕ P ≃ X) (cX : ColorMap 𝓒 X) : Prop :=
+    cX ∘ e ∘ Sum.inl ∘ Sum.inl = 𝓒.τ ∘ cX ∘ e ∘ Sum.inl ∘ Sum.inr
+
+namespace ContrCond
+
+variable {e : (C ⊕ C) ⊕ P ≃ X} {e' : Y ≃ Z} {cX : ColorMap 𝓒 X} {cY : ColorMap 𝓒 Y} {cZ : ColorMap 𝓒 Z}
+variable {cX' : ColorMap 𝓒 X'} {cY' : ColorMap 𝓒 Y'}
+
+lemma to_contrAll (h : cX.ContrCond e) :
+    (cX.contrLeft e).ContrAll (Equiv.refl _) (cX.contrRight e) := h
+
+end ContrCond
+
+end ColorMap
+
+end TensorColor
+
 namespace TensorStructure
 
 variable (𝓣 : TensorStructure R)
@@ -47,8 +119,8 @@ variable (𝓣 : TensorStructure R)
 variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
   [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
   [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P]
-  {cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color}
-  {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
+  {cX cX2 : 𝓣.ColorMap X} {cY : 𝓣.ColorMap Y} {cZ : 𝓣.ColorMap Z}
+  {cW : 𝓣.ColorMap W} {cY' : 𝓣.ColorMap Y'} {μ ν: 𝓣.Color}
 
 variable {G H : Type} [Group G] [Group H] [MulActionTensor G 𝓣]
 local infixl:101 " • " => 𝓣.rep
@@ -79,6 +151,14 @@ def pairProd : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cX2 →ₗ[R]
     PiTensorProduct.map₂ (fun x =>
       TensorProduct.mk R (𝓣.ColorModule (cX x)) (𝓣.ColorModule (cX2 x))))
 
+lemma pairProd_tmul_tprod_tprod (fx : (i : X) → 𝓣.ColorModule (cX i))
+    (fx2 : (i : X) → 𝓣.ColorModule (cX2 i)) :
+    𝓣.pairProd (PiTensorProduct.tprod R fx ⊗ₜ[R] PiTensorProduct.tprod R fx2) =
+    PiTensorProduct.tprod R (fun x => fx x ⊗ₜ[R] fx2 x) := by
+  simp [pairProd]
+  erw [PiTensorProduct.map₂_tprod_tprod]
+  rfl
+
 lemma mkPiAlgebra_equiv (e : X ≃ Y) :
     (PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R X R)) =
     (PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R Y R)) ∘ₗ
@@ -97,17 +177,47 @@ def contrAll' : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor (𝓣.τ ∘ cX) →ₗ[R] R :
   (PiTensorProduct.map (fun x => 𝓣.contrDual (cX x))) ∘ₗ
   (𝓣.pairProd)
 
-lemma contrAll'_mapIso_cond {e : X ≃ Y} (h : cX = cY ∘ e) :
-    𝓣.τ ∘ cY = (𝓣.τ ∘ cX) ∘ ⇑e.symm := by
-  subst h
-  exact (Equiv.eq_comp_symm e (𝓣.τ ∘ cY) (𝓣.τ ∘ cY ∘ ⇑e)).mpr rfl
+lemma contrAll'_tmul_tprod_tprod (fx : (i : X) → 𝓣.ColorModule (cX i))
+    (fy : (i : X) → 𝓣.ColorModule (𝓣.τ (cX i))) :
+    𝓣.contrAll' (PiTensorProduct.tprod R fx ⊗ₜ[R] PiTensorProduct.tprod R fy) =
+    (PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R X R))
+    (PiTensorProduct.tprod R (fun x => 𝓣.contrDual (cX x) (fx x ⊗ₜ[R] fy x))) := by
+  simp only [contrAll', Function.comp_apply, LinearMap.coe_comp, PiTensorProduct.lift.tprod,
+    MultilinearMap.mkPiAlgebra_apply]
+  erw [pairProd_tmul_tprod_tprod]
+  simp only [Function.comp_apply, PiTensorProduct.map_tprod, PiTensorProduct.lift.tprod,
+    MultilinearMap.mkPiAlgebra_apply]
 
 @[simp]
-lemma contrAll'_mapIso (e : X ≃ Y) (h : c = cY ∘ e) :
+lemma contrAll'_isEmpty_tmul [IsEmpty X] (x :  𝓣.Tensor cX) (y : 𝓣.Tensor (𝓣.τ ∘ cX)) :
+    𝓣.contrAll' (x ⊗ₜ y) = 𝓣.isEmptyEquiv x * 𝓣.isEmptyEquiv y := by
+  refine PiTensorProduct.induction_on' x ?_ (by
+    intro a b hx hy
+    simp [map_add, add_tmul, add_mul, hx, hy])
+  intro rx fx
+  refine PiTensorProduct.induction_on' y ?_ (by
+      intro a b hx hy
+      simp at hx hy
+      simp [map_add, tmul_add, mul_add, hx, hy])
+  intro ry fy
+  simp [smul_tmul]
+  ring_nf
+  rw [mul_assoc, mul_assoc]
+  apply congrArg
+  apply congrArg
+  simp [contrAll']
+  erw [pairProd_tmul_tprod_tprod]
+  simp only [Function.comp_apply, PiTensorProduct.map_tprod, PiTensorProduct.lift.tprod,
+    MultilinearMap.mkPiAlgebra_apply, Finset.univ_eq_empty, Finset.prod_empty]
+  erw [isEmptyEquiv_tprod]
+
+
+@[simp]
+lemma contrAll'_mapIso (e : X ≃ Y) (h : cX.MapIso e cY) :
     𝓣.contrAll' ∘ₗ
       (TensorProduct.congr (𝓣.mapIso e h) (LinearEquiv.refl R _)).toLinearMap =
     𝓣.contrAll' ∘ₗ (TensorProduct.congr (LinearEquiv.refl R _)
-      (𝓣.mapIso e.symm (𝓣.contrAll'_mapIso_cond h))).toLinearMap := by
+      (𝓣.mapIso e.symm h.symm.dual)).toLinearMap := by
   apply TensorProduct.ext'
   refine fun x ↦
     PiTensorProduct.induction_on' x ?_ (by
@@ -120,110 +230,86 @@ lemma contrAll'_mapIso (e : X ≃ Y) (h : c = cY ∘ e) :
       simp at hx hy
       simp [map_add, tmul_add, hx, hy])
   intro ry fy
-  simp [contrAll']
+  simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, Function.comp_apply, tmul_smul,
+    LinearMapClass.map_smul, LinearMap.coe_comp, LinearEquiv.coe_coe, congr_tmul, mapIso_tprod,
+    LinearEquiv.refl_apply, smul_eq_mul, smul_tmul]
+  apply congrArg
+  apply congrArg
+  erw [contrAll'_tmul_tprod_tprod ]
+  erw [TensorProduct.congr_tmul]
+  simp only [PiTensorProduct.lift.tprod, LinearEquiv.refl_apply]
+  erw [mapIso_tprod]
+  erw [contrAll'_tmul_tprod_tprod]
   rw [mkPiAlgebra_equiv e]
+  simp only [ Equiv.symm_symm_apply, LinearMap.coe_comp,
+    LinearEquiv.coe_coe, Function.comp_apply, PiTensorProduct.reindex_tprod,
+    PiTensorProduct.lift.tprod]
   apply congrArg
-  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply]
+  funext y
+  rw [𝓣.contrDual_cast (congrFun h.symm y)]
   apply congrArg
-  rw [← LinearEquiv.symm_apply_eq]
-  rw [PiTensorProduct.reindex_symm]
-  rw [← PiTensorProduct.map_reindex]
-  subst h
-  simp only [Equiv.symm_symm_apply, Function.comp_apply]
-  apply congrArg
-  rw [pairProd, pairProd]
-  simp only [Function.comp_apply, lift.tmul, LinearMapClass.map_smul, LinearMap.smul_apply]
-  apply congrArg
-  change _ = ((PiTensorProduct.map₂ fun x => TensorProduct.mk R (𝓣.ColorModule (cY (e x)))
-      (𝓣.ColorModule (𝓣.τ (cY (e x)))))
-      ((PiTensorProduct.tprod R) fx))
-    ((𝓣.mapIso e.symm _) ((PiTensorProduct.tprod R) fy))
-  rw [mapIso_tprod]
-  simp only [Equiv.symm_symm_apply, Function.comp_apply]
-  rw [PiTensorProduct.map₂_tprod_tprod]
-  change PiTensorProduct.reindex R _ e.symm
-    ((PiTensorProduct.map₂ _
-        ((PiTensorProduct.tprod R) fun i => (𝓣.colorModuleCast _) (fx (e.symm i))))
-      ((PiTensorProduct.tprod R) fy)) = _
-  rw [PiTensorProduct.map₂_tprod_tprod]
-  simp only [Equiv.symm_symm_apply, Function.comp_apply, mk_apply]
-  erw [PiTensorProduct.reindex_tprod]
-  apply congrArg
-  funext i
-  simp only [Equiv.symm_symm_apply]
-  congr
+  congr 1
   simp [colorModuleCast]
+  symm
   apply cast_eq_iff_heq.mpr
-  rw [Equiv.symm_apply_apply]
+  simp [colorModuleCast, Equiv.apply_symm_apply]
+  rw [Equiv.apply_symm_apply]
+  exact HEq.symm (cast_heq _ _)
 
 @[simp]
-lemma contrAll'_mapIso_tmul (e : X ≃ Y) (h : c = cY ∘ e) (x : 𝓣.Tensor c)
+lemma contrAll'_mapIso_tmul (e : X ≃ Y) (h : cX.MapIso e cY) (x : 𝓣.Tensor cX)
     (y : 𝓣.Tensor (𝓣.τ ∘ cY)) : 𝓣.contrAll' ((𝓣.mapIso e h) x ⊗ₜ[R] y) =
-    𝓣.contrAll' (x ⊗ₜ[R] (𝓣.mapIso e.symm (𝓣.contrAll'_mapIso_cond h) y)) := by
+    𝓣.contrAll' (x ⊗ₜ[R] (𝓣.mapIso e.symm h.symm.dual y)) := by
   change (𝓣.contrAll' ∘ₗ
     (TensorProduct.congr (𝓣.mapIso e h) (LinearEquiv.refl R _)).toLinearMap) (x ⊗ₜ[R] y) = _
   rw [contrAll'_mapIso]
   rfl
 
 /-- The contraction of all the indices of two tensors with dual colors. -/
-def contrAll (e : X ≃ Y) (h : cX = 𝓣.τ ∘ cY ∘ e) : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY →ₗ[R] R :=
+def contrAll (e : X ≃ Y) (h : cX.ContrAll e cY) : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY →ₗ[R] R :=
   𝓣.contrAll' ∘ₗ (TensorProduct.congr (LinearEquiv.refl _ _)
-    (𝓣.mapIso e.symm (by funext a; simpa [h] using (𝓣.τ_involutive _).symm))).toLinearMap
+    (𝓣.mapIso e.symm h.symm.toMapIso)).toLinearMap
 
-lemma contrAll_symm_cond {e : X ≃ Y} (h : c = 𝓣.τ ∘ cY ∘ e) :
-    cY = 𝓣.τ ∘ c ∘ ⇑e.symm := by
-  subst h
-  ext1 x
-  simp only [Function.comp_apply, Equiv.apply_symm_apply]
-  rw [𝓣.τ_involutive]
-
-lemma contrAll_mapIso_right_cond {e : X ≃ Y} {e' : Z ≃ Y}
-    (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') : c = 𝓣.τ ∘ cZ ∘ ⇑(e.trans e'.symm) := by
-  subst h h'
-  ext1 x
-  simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply]
+lemma contrAll_tmul (e : X ≃ Y) (h : cX.ContrAll e cY) (x : 𝓣.Tensor cX) (y : 𝓣.Tensor cY) :
+    𝓣.contrAll e h (x ⊗ₜ[R] y) = 𝓣.contrAll' (x ⊗ₜ[R] ((𝓣.mapIso e.symm h.symm.toMapIso) y)) := by
+  rw [contrAll]
+  simp only [LinearMap.coe_comp, Function.comp_apply]
+  rfl
 
 @[simp]
 lemma contrAll_mapIso_right_tmul (e : X ≃ Y) (e' : Z ≃ Y)
-    (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (x : 𝓣.Tensor c) (z : 𝓣.Tensor cZ) :
+    (h : c.ContrAll e  cY ) (h' : cZ.MapIso e' cY) (x : 𝓣.Tensor c) (z : 𝓣.Tensor cZ) :
     𝓣.contrAll e h (x ⊗ₜ[R] 𝓣.mapIso e' h' z) =
-    𝓣.contrAll (e.trans e'.symm) (𝓣.contrAll_mapIso_right_cond h h') (x ⊗ₜ[R] z) := by
-  rw [contrAll, contrAll]
-  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul,
+    𝓣.contrAll (e.trans e'.symm) (h.trans_mapIso h') (x ⊗ₜ[R] z) := by
+  simp only [contrAll_tmul, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul,
     LinearEquiv.refl_apply, mapIso_mapIso]
-  congr
+  apply congrArg
+  rfl
 
 @[simp]
 lemma contrAll_comp_mapIso_right (e : X ≃ Y) (e' : Z ≃ Y)
-    (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') : 𝓣.contrAll e h ∘ₗ
+    (h : c.ContrAll e  cY ) (h' : cZ.MapIso e' cY) : 𝓣.contrAll e h ∘ₗ
     (TensorProduct.congr (LinearEquiv.refl R (𝓣.Tensor c)) (𝓣.mapIso e' h')).toLinearMap
-    = 𝓣.contrAll (e.trans e'.symm) (𝓣.contrAll_mapIso_right_cond h h') := by
+    = 𝓣.contrAll (e.trans e'.symm) (h.trans_mapIso h') := by
   apply TensorProduct.ext'
   intro x y
   exact 𝓣.contrAll_mapIso_right_tmul e e' h h' x y
 
-lemma contrAll_mapIso_left_cond {e : X ≃ Y} {e' : Z ≃ X}
-    (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = c ∘ e') : cZ = 𝓣.τ ∘ cY ∘ ⇑(e'.trans e) := by
-  subst h h'
-  ext1 x
-  simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply]
-
 @[simp]
 lemma contrAll_mapIso_left_tmul {e : X ≃ Y} {e' : Z ≃ X}
-    (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = c ∘ e') (x : 𝓣.Tensor cZ) (y : 𝓣.Tensor cY) :
+    (h : cX.ContrAll e cY) (h' : cZ.MapIso e' cX ) (x : 𝓣.Tensor cZ) (y : 𝓣.Tensor cY) :
     𝓣.contrAll e h (𝓣.mapIso e' h' x ⊗ₜ[R] y) =
-    𝓣.contrAll (e'.trans e) (𝓣.contrAll_mapIso_left_cond h h') (x ⊗ₜ[R] y) := by
-  rw [contrAll, contrAll]
-  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul,
+    𝓣.contrAll (e'.trans e) (h.mapIso_trans h') (x ⊗ₜ[R] y) := by
+  simp only [contrAll_tmul, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul,
     LinearEquiv.refl_apply, contrAll'_mapIso_tmul, mapIso_mapIso]
-  congr
+  rfl
 
 @[simp]
 lemma contrAll_mapIso_left {e : X ≃ Y} {e' : Z ≃ X}
-    (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = c ∘ e') :
+    (h : cX.ContrAll e cY) (h' : cZ.MapIso e' cX ) :
     𝓣.contrAll e h ∘ₗ
     (TensorProduct.congr (𝓣.mapIso e' h') (LinearEquiv.refl R (𝓣.Tensor cY))).toLinearMap
-    = 𝓣.contrAll (e'.trans e) (𝓣.contrAll_mapIso_left_cond h h') := by
+    = 𝓣.contrAll (e'.trans e) (h.mapIso_trans h') := by
   apply TensorProduct.ext'
   intro x y
   exact 𝓣.contrAll_mapIso_left_tmul h h' x y
@@ -231,7 +317,7 @@ lemma contrAll_mapIso_left {e : X ≃ Y} {e' : Z ≃ X}
 /-- The linear map from `𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY ⊗[R] 𝓣.Tensor cZ` to
   `𝓣.Tensor cZ` obtained by contracting all indices in `𝓣.Tensor cX` and `𝓣.Tensor cY`,
   given a proof that this is possible. -/
-def contrAllLeft (e : X ≃ Y) (h : cX = 𝓣.τ ∘ cY ∘ e) :
+def contrAllLeft (e : X ≃ Y) (h : cX.ContrAll e cY) :
     𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY ⊗[R] 𝓣.Tensor cZ →ₗ[R] 𝓣.Tensor cZ :=
   (TensorProduct.lid R _).toLinearMap ∘ₗ
   TensorProduct.map (𝓣.contrAll e h) (LinearEquiv.refl R (𝓣.Tensor cZ)).toLinearMap
@@ -240,7 +326,7 @@ def contrAllLeft (e : X ≃ Y) (h : cX = 𝓣.τ ∘ cY ∘ e) :
 /-- The linear map from `(𝓣.Tensor cW ⊗[R] 𝓣.Tensor cX) ⊗[R] (𝓣.Tensor cY ⊗[R] 𝓣.Tensor cZ)`
   to `𝓣.Tensor cW ⊗[R] 𝓣.Tensor cZ` obtained by contracting all indices of the tensors
   in the middle. -/
-def contrAllMid (e : X ≃ Y) (h : cX = 𝓣.τ ∘ cY ∘ e) :
+def contrAllMid (e : X ≃ Y) (h : cX.ContrAll e cY) :
     (𝓣.Tensor cW ⊗[R] 𝓣.Tensor cX) ⊗[R] (𝓣.Tensor cY ⊗[R] 𝓣.Tensor cZ) →ₗ[R]
     𝓣.Tensor cW ⊗[R] 𝓣.Tensor cZ :=
   (TensorProduct.map (LinearEquiv.refl R _).toLinearMap (𝓣.contrAllLeft e h)) ∘ₗ
@@ -249,7 +335,7 @@ def contrAllMid (e : X ≃ Y) (h : cX = 𝓣.τ ∘ cY ∘ e) :
 /-- The linear map from `𝓣.Tensor (Sum.elim cW cX) ⊗[R] 𝓣.Tensor (Sum.elim cY cZ)`
   to `𝓣.Tensor (Sum.elim cW cZ)` formed by contracting the indices specified by
   `cX` and `cY`, which are assumed to be dual. -/
-def contrElim (e : X ≃ Y) (h : cX = 𝓣.τ ∘ cY ∘ e) :
+def contrElim (e : X ≃ Y) (h : cX.ContrAll e cY) :
     𝓣.Tensor (Sum.elim cW cX) ⊗[R] 𝓣.Tensor (Sum.elim cY cZ) →ₗ[R] 𝓣.Tensor (Sum.elim cW cZ) :=
     (𝓣.tensoratorEquiv cW cZ).toLinearMap ∘ₗ 𝓣.contrAllMid e h ∘ₗ
     (TensorProduct.congr (𝓣.tensoratorEquiv cW cX).symm
@@ -262,7 +348,7 @@ def contrElim (e : X ≃ Y) (h : cX = 𝓣.τ ∘ cY ∘ e) :
 -/
 
 @[simp]
-lemma contrAll_rep {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) (g : G) :
+lemma contrAll_rep (e : X ≃ Y) (h : cX.ContrAll e cY) (g : G) :
     𝓣.contrAll e h ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) = 𝓣.contrAll e h := by
   apply TensorProduct.ext'
   refine fun x ↦ PiTensorProduct.induction_on' x ?_ (by
@@ -274,22 +360,21 @@ lemma contrAll_rep {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (
       simp at hx hy
       simp [map_add, tmul_add, hx, hy])
   intro ry fy
-  simp [contrAll, TensorProduct.smul_tmul]
+  simp only [contrAll_tmul, PiTensorProduct.tprodCoeff_eq_smul_tprod, tmul_smul, smul_tmul,
+    LinearMapClass.map_smul, LinearMap.coe_comp, Function.comp_apply, map_tmul, rep_tprod,
+    smul_eq_mul]
   apply congrArg
   apply congrArg
-  simp [contrAll']
+  simp only [contrAll', mapIso_tprod, Equiv.symm_symm_apply, colorModuleCast_equivariant_apply,
+    LinearMap.coe_comp, Function.comp_apply]
   apply congrArg
-  simp [pairProd]
-  change (PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _) =
-    (PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _)
-  rw [PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map_tprod,
-  PiTensorProduct.map_tprod]
-  simp only [mk_apply]
+  erw [pairProd_tmul_tprod_tprod, pairProd_tmul_tprod_tprod, PiTensorProduct.map_tprod,
+    PiTensorProduct.map_tprod]
   apply congrArg
   funext x
-  rw [← colorModuleCast_equivariant_apply]
-  nth_rewrite 2 [← contrDual_inv (c x) g]
-  simp
+  nth_rewrite 2 [← contrDual_inv (cX x) g]
+  rfl
+
 
 @[simp]
 lemma contrAll_rep_apply {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e)
@@ -312,9 +397,8 @@ lemma contrAll_rep_tmul {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃
 -/
 
 lemma contr_cond (e : (C ⊕ C) ⊕ P ≃ X) :
-    cX = Sum.elim (Sum.elim (cX ∘ ⇑e ∘ Sum.inl ∘ Sum.inl) (cX ∘ ⇑e ∘ Sum.inl ∘ Sum.inr)) (
-      cX ∘ ⇑e ∘ Sum.inr) ∘ ⇑e.symm := by
-  rw [Equiv.eq_comp_symm]
+    cX.MapIso e.symm (Sum.elim (Sum.elim (cX.contrLeft e) (cX.contrRight e)) (cX.contr e)):= by
+  rw [TensorColor.ColorMap.MapIso, Equiv.eq_comp_symm]
   funext x
   match x with
   | Sum.inl (Sum.inl x) => rfl
@@ -323,24 +407,46 @@ lemma contr_cond (e : (C ⊕ C) ⊕ P ≃ X) :
 
 /-- Contraction of indices based on an equivalence `(C ⊕ C) ⊕ P ≃ X`. The indices
   in `C` are contracted pair-wise, whilst the indices in `P` are preserved. -/
-def contr (e : (C ⊕ C) ⊕ P ≃ X)
-    (h : cX ∘ e ∘ Sum.inl ∘ Sum.inl = 𝓣.τ ∘ cX ∘ e ∘ Sum.inl ∘ Sum.inr) :
-    𝓣.Tensor cX →ₗ[R] 𝓣.Tensor (cX ∘ e ∘ Sum.inr) :=
+def contr (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrCond e) :
+    𝓣.Tensor cX →ₗ[R] 𝓣.Tensor (cX.contr e) :=
   (TensorProduct.lid R _).toLinearMap ∘ₗ
-  (TensorProduct.map (𝓣.contrAll (Equiv.refl C) (by simpa using h)) LinearMap.id) ∘ₗ
+  (TensorProduct.map (𝓣.contrAll (Equiv.refl C) h.to_contrAll) LinearMap.id) ∘ₗ
   (TensorProduct.congr (𝓣.tensoratorEquiv _ _).symm (LinearEquiv.refl R _)).toLinearMap ∘ₗ
   (𝓣.tensoratorEquiv _ _).symm.toLinearMap ∘ₗ
   (𝓣.mapIso e.symm (𝓣.contr_cond e)).toLinearMap
 
+open PiTensorProduct in
+lemma contr_tprod (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrCond e) (f : (i : X) → 𝓣.ColorModule (cX i)) :
+    𝓣.contr e h (tprod R f) = (𝓣.contrAll (Equiv.refl C) h.to_contrAll
+        (tprod R (fun i => f (e (Sum.inl (Sum.inl i)))) ⊗ₜ[R]
+        tprod R (fun i => f (e (Sum.inl (Sum.inr i)))))) •
+        tprod R (fun (p : P) => f (e (Sum.inr p))) := by
+  simp only [contr, LinearEquiv.comp_coe, LinearMap.coe_comp, LinearEquiv.coe_coe,
+    Function.comp_apply, LinearEquiv.trans_apply, mapIso_tprod, Equiv.symm_symm_apply,
+    tensoratorEquiv_symm_tprod, congr_tmul, LinearEquiv.refl_apply, map_tmul, LinearMap.id_coe,
+    id_eq, lid_tmul]
+  rw [contrAll_tmul]
+  rfl
+
+open PiTensorProduct in
+@[simp]
+lemma contr_tprod_isEmpty [IsEmpty C] (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrCond e)
+    (f : (i : X) → 𝓣.ColorModule (cX i)) :
+    𝓣.contr e h (tprod R f) = tprod R (fun (p : P) => f (e (Sum.inr p))) := by
+  rw [contr_tprod]
+  rw [contrAll_tmul, contrAll'_isEmpty_tmul]
+  simp only [isEmptyEquiv_tprod, Equiv.refl_symm, mapIso_tprod, Equiv.refl_apply, one_mul]
+  erw [isEmptyEquiv_tprod]
+  simp
+
 /-- The contraction of indices via `contr` is equivariant. -/
 @[simp]
-lemma contr_equivariant (e : (C ⊕ C) ⊕ P ≃ X)
-    (h : cX ∘ e ∘ Sum.inl ∘ Sum.inl = 𝓣.τ ∘ cX ∘ e ∘ Sum.inl ∘ Sum.inr)
+lemma contr_equivariant (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrCond e)
     (g : G) (x : 𝓣.Tensor cX) : 𝓣.contr e h (g • x) = g • 𝓣.contr e h x := by
-  simp only [contr, TensorProduct.congr, LinearEquiv.refl_toLinearMap, LinearEquiv.symm_symm,
-    LinearEquiv.refl_symm, LinearEquiv.ofLinear_toLinearMap, LinearEquiv.comp_coe,
-    LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.trans_apply,
-    rep_mapIso_apply, rep_tensoratorEquiv_symm_apply]
+  simp only [TensorColor.ColorMap.contr, contr, TensorProduct.congr, LinearEquiv.refl_toLinearMap,
+    LinearEquiv.symm_symm, LinearEquiv.refl_symm, LinearEquiv.ofLinear_toLinearMap,
+    LinearEquiv.comp_coe, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
+    LinearEquiv.trans_apply, rep_mapIso_apply, rep_tensoratorEquiv_symm_apply]
   rw [← LinearMap.comp_apply (TensorProduct.map _ _), ← TensorProduct.map_comp]
   rw [← LinearMap.comp_apply (TensorProduct.map _ _), ← TensorProduct.map_comp]
   rw [LinearMap.comp_assoc, rep_tensoratorEquiv_symm, ← LinearMap.comp_assoc]
diff --git a/HepLean/SpaceTime/LorentzTensor/Fin.lean b/HepLean/SpaceTime/LorentzTensor/Fin.lean
deleted file mode 100644
index f69396e..0000000
--- a/HepLean/SpaceTime/LorentzTensor/Fin.lean
+++ /dev/null
@@ -1,110 +0,0 @@
-/-
-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.SpaceTime.LorentzTensor.Basic
-import HepLean.SpaceTime.LorentzTensor.MulActionTensor
-/-!
-
-# Lorentz tensors indexed by Fin n
-
-In physics, in many (if not all) cases, we index our Lorentz tensors by `Fin n`.
-
-In this file we set up the machinery to deal with Lorentz tensors indexed by `Fin n`
-in a way that is convenient for physicists, and general caculation.
-
-## Note
-
-This file is currently a stub.
-
--/
-
-open TensorProduct
-
-noncomputable section
-
-namespace TensorStructure
-
-variable {n m : ℕ}
-
-variable {R : Type} [CommSemiring R] (𝓣 : TensorStructure R)
-
-variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
-  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
-  {cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color}
-  {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
-  {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color}
-
-variable {G H : Type} [Group G] [Group H] [MulActionTensor G 𝓣]
-local infixl:101 " • " => 𝓣.rep
-
-open MulActionTensor
-
-/-- Casting a tensor defined on `Fin n` to `Fin m` where `n = m`. -/
-@[simp]
-def finCast (h : n = m) (hc : cn = cm ∘ Fin.castOrderIso h) : 𝓣.Tensor cn ≃ₗ[R] 𝓣.Tensor cm :=
-  𝓣.mapIso (Fin.castOrderIso h) hc
-
-/-- An equivalence between `𝓣.Tensor cn ⊗[R] 𝓣.Tensor cm` indexed by `Fin n` and `Fin m`,
-  and `𝓣.Tensor (Sum.elim cn cm ∘ finSumFinEquiv.symm)` indexed by `Fin (n + m)`. -/
-@[simp]
-def finSumEquiv : 𝓣.Tensor cn ⊗[R] 𝓣.Tensor cm ≃ₗ[R]
-    𝓣.Tensor (Sum.elim cn cm ∘ finSumFinEquiv.symm) :=
-  (𝓣.tensoratorEquiv cn cm).trans (𝓣.mapIso finSumFinEquiv (by funext a; simp))
-
-/-!
-
-## Vectors as tensors & singletons
-
--/
-
-/-- Tensors on `Fin 1` are equivalent to a constant Pi tensor product. -/
-def tensorSingeletonEquiv : 𝓣.Tensor ![μ] ≃ₗ[R] ⨂[R] _ : (Fin 1), 𝓣.ColorModule μ := by
-  refine LinearEquiv.ofLinear (PiTensorProduct.map (fun i =>
-      match i with
-      | 0 => LinearMap.id)) (PiTensorProduct.map (fun i =>
-    match i with
-    | 0 => LinearMap.id)) ?_ ?_
-  all_goals
-    apply LinearMap.ext
-    refine fun x ↦
-      PiTensorProduct.induction_on' x ?_ (by
-        intro a b hx a
-        simp_all only [Nat.succ_eq_add_one, Matrix.cons_val_zero, LinearMap.coe_comp,
-          Function.comp_apply, LinearMap.id_coe, id_eq, map_add])
-    intro r x
-    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Matrix.cons_val_zero,
-      PiTensorProduct.tprodCoeff_eq_smul_tprod, LinearMapClass.map_smul, LinearMap.coe_comp,
-      Function.comp_apply, LinearMap.id_coe, id_eq]
-    change r •
-      (PiTensorProduct.map _) ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) x)) = _
-    rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod]
-    repeat apply congrArg
-    funext i
-    fin_cases i
-    rfl
-
-/-- An equivalence between the `ColorModule` for a color and a `Fin 1` tensor with that color. -/
-def vecAsTensor : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.Tensor ![μ] :=
-  ((PiTensorProduct.subsingletonEquiv 0).symm : _ ≃ₗ[R] ⨂[R] _ : (Fin 1), 𝓣.ColorModule μ)
-    ≪≫ₗ 𝓣.tensorSingeletonEquiv.symm
-
-/-- The equivalence `vecAsTensor` is equivariant with respect to `MulActionTensor`-actions. -/
-@[simp]
-lemma vecAsTensor_equivariant (g : G) (v : 𝓣.ColorModule μ) :
-    𝓣.vecAsTensor (repColorModule μ g v) = g • 𝓣.vecAsTensor v := by
-  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, vecAsTensor, Fin.isValue, tensorSingeletonEquiv,
-    Matrix.cons_val_zero, LinearEquiv.trans_apply, PiTensorProduct.subsingletonEquiv_symm_apply,
-    LinearEquiv.ofLinear_symm_apply]
-  change (PiTensorProduct.map _) ((PiTensorProduct.tprod R) _) =
-    (𝓣.rep g) ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) fun _ => v))
-  rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod, rep_tprod]
-  apply congrArg
-  funext i
-  fin_cases i
-  rfl
-
-end TensorStructure
-
-end
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
index 655355e..c5a6cba 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
@@ -193,6 +193,11 @@ def colorMap : Fin l.numIndices → X :=
 def idMap : Fin l.numIndices → Nat :=
   fun i => (l.get i).id
 
+lemma idMap_cast {l1 l2 : IndexList X} (h : l1 = l2) (i : Fin l1.numIndices) :
+    l1.idMap i = l2.idMap (Fin.cast (by rw [h]) i) := by
+  subst h
+  rfl
+
 /-- Given a list of indices a subset of `Fin l.numIndices × Index X`
   of pairs of positions in `l` and the corresponding item in `l`. -/
 def toPosSet (l : IndexList X) : Set (Fin l.numIndices × Index X) :=
@@ -366,6 +371,15 @@ lemma hasNoContr_color_eq_of_id_eq (h : l.HasNoContr) (i j : Fin l.length) :
   apply l.hasNoContr_id_inj h at h1
   rw [h1]
 
+@[simp]
+lemma hasNoContr_noContrFinset_card (h : l.HasNoContr) :
+    l.noContrFinset.card = List.length l := by
+  simp only [noContrFinset]
+  rw [Finset.filter_true_of_mem]
+  simp
+  intro x _
+  exact h x
+
 /-!
 
 ## The contracted index list
@@ -439,6 +453,12 @@ instance : DecidablePred fun x => x ∈ l.contrPairSet := fun _ =>
 
 instance : Fintype l.contrPairSet := setFintype _
 
+lemma contrPairSet_isEmpty_of_hasNoContr (h : l.HasNoContr) :
+    IsEmpty l.contrPairSet := by
+  simp only [contrPairSet, Subtype.coe_lt_coe, Set.coe_setOf, isEmpty_subtype, not_and, Prod.forall]
+  refine fun a b h' =>  h a.1 b.1 (Fin.ne_of_lt h')
+
+
 lemma getDual_lt_self_mem_contrPairSet {i : l.contrSubtype}
     (h : (l.getDual i).1 < i.1) : (l.getDual i, i) ∈ l.contrPairSet :=
   And.intro h (l.getDual_id i).symm
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean
index c47b07e..9c247ce 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean
@@ -192,6 +192,18 @@ lemma splitContr_map :
   rw [contrPairSet_fst_eq_dual_snd _ _]
   exact l.prop.2 _
 
+lemma splitContr_symm_apply_of_hasNoContr (h : l.1.HasNoContr) (x : Fin (l.1.noContrFinset).card) :
+    l.splitContr.symm (Sum.inr x) = Fin.castOrderIso (l.1.hasNoContr_noContrFinset_card h) x := by
+  simp [splitContr, noContrSubtypeEquiv, noContrFinset]
+  trans (Finset.univ.orderEmbOfFin (by rw [l.1.hasNoContr_noContrFinset_card h]; simp)) x
+  congr
+  rw [Finset.filter_true_of_mem (fun x _ => h x )]
+  rw [@Finset.orderEmbOfFin_apply]
+  simp only [List.get_eq_getElem, Fin.sort_univ, List.getElem_finRange]
+  rfl
+
+
+
 /-!
 
 ## The contracted index list
@@ -372,6 +384,31 @@ lemma toEquiv_trans {s1 s2 s3 : IndexListColor 𝓒} (h1 : PermContr s1 s2) (h2
   simp [toEquiv]
   rw [← get_trans]
 
+lemma of_contr_eq {s1 s2 : IndexListColor 𝓒} (hc : s1.contr = s2.contr) :
+    PermContr s1 s2 := by
+  simp [PermContr]
+  rw [hc]
+  simp
+  refine hasNoContr_color_eq_of_id_eq s2.contr.1 (s2.1.contrIndexList_hasNoContr)
+
+lemma toEquiv_contr_eq {s1 s2 : IndexListColor 𝓒} (hc : s1.contr = s2.contr) :
+    (of_contr_eq hc).toEquiv = (Fin.castOrderIso (by rw [hc])).toEquiv := by
+  apply Equiv.ext
+  intro x
+  simp [toEquiv, of_contr_eq, hc, get]
+  have h1 : (Fin.find fun j => (s1.contr).1.idMap x = (s2.contr).1.idMap j) =
+      some ((Fin.castOrderIso (by rw [hc]; rfl)).toEquiv x) := by
+    rw [Fin.find_eq_some_iff]
+    apply And.intro
+    rw [idMap_cast (congrArg Subtype.val hc)]
+    rfl
+    intro j hj
+    rw [idMap_cast (congrArg Subtype.val hc)] at hj
+    have h2 := s2.contr.1.hasNoContr_id_inj (s2.1.contrIndexList_hasNoContr) hj
+    subst h2
+    rfl
+  simp only [h1, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Option.get_some]
+
 end PermContr
 
 /-! TODO: Show that `rel` is indeed an equivalence relation. -/
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean
index 02ccf47..e90a776 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean
@@ -264,8 +264,9 @@ noncomputable def fromIndexString (T : 𝓣.Tensor cn) (s : String)
     (hn : n = (IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)).length)
     (hc : IndexListColorProp 𝓣.toTensorColor (
       IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)))
-    (hd : TensorColor.DualMap (IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)).colorMap
-    (cn ∘ Fin.cast hn.symm)) : 𝓣.TensorIndex :=
+    (hd : TensorColor.ColorMap.DualMap
+      (IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)).colorMap
+      (cn ∘ Fin.cast hn.symm)) : 𝓣.TensorIndex :=
   TensorStructure.TensorIndex.mkDualMap T
     ⟨(IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)), hc⟩ hn hd
 
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
index 4ace483..b55ee19 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
@@ -58,15 +58,28 @@ lemma ext (T₁ T₂ : 𝓣.TensorIndex) (hi : T₁.index = T₂.index)
   subst hi
   simp_all
 
+lemma index_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) : T₁.index = T₂.index := by
+  cases h
+  rfl
+lemma tensor_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) : T₁.tensor =
+   𝓣.mapIso (Fin.castOrderIso (by rw [index_eq_of_eq h])).toEquiv
+    (index_eq_colorMap_eq (index_eq_of_eq h)) T₂.tensor := by
+  have hi := index_eq_of_eq h
+  cases T₁
+  cases T₂
+  simp at hi
+  subst hi
+  simpa using h
+
 /-- The construction of a `TensorIndex` from a tensor, a IndexListColor, and a condition
   on the dual maps. -/
 def mkDualMap (T : 𝓣.Tensor cn) (l : IndexListColor 𝓣.toTensorColor) (hn : n = l.1.length)
-    (hd : DualMap l.1.colorMap (cn ∘ Fin.cast hn.symm)) :
+    (hd : ColorMap.DualMap l.1.colorMap (cn ∘ Fin.cast hn.symm)) :
     𝓣.TensorIndex where
   index := l
   tensor :=
-      𝓣.mapIso (Equiv.refl _) (DualMap.split_dual' (by simp [hd])) <|
-      𝓣.dualize (DualMap.split l.1.colorMap (cn ∘ Fin.cast hn.symm)) <|
+      𝓣.mapIso (Equiv.refl _) (ColorMap.DualMap.split_dual' (by simp [hd])) <|
+      𝓣.dualize (ColorMap.DualMap.split l.1.colorMap (cn ∘ Fin.cast hn.symm)) <|
       (𝓣.mapIso (Fin.castOrderIso hn).toEquiv rfl T : 𝓣.Tensor (cn ∘ Fin.cast hn.symm))
 
 /-!
@@ -83,7 +96,41 @@ def contr (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where
       T.index.contr_colorMap <|
       𝓣.contr (T.index.splitContr).symm T.index.splitContr_map T.tensor
 
-/-! TODO: Show that contracting twice is the same as contracting once. -/
+/-- Applying contr to a tensor whose indices has no contracts does not do anything. -/
+@[simp]
+lemma contr_of_hasNoContr (T : 𝓣.TensorIndex) (h : T.index.1.HasNoContr) :
+    T.contr = T := by
+  refine ext _ _ ?_ ?_
+  exact Subtype.eq (T.index.1.contrIndexList_of_hasNoContr h)
+  simp only [contr]
+  have h1 : IsEmpty T.index.1.contrPairSet := T.index.1.contrPairSet_isEmpty_of_hasNoContr h
+  cases T
+  rename_i i T
+  simp only
+  refine PiTensorProduct.induction_on' T ?_ (by
+    intro a b hx hy
+    simp [map_add, add_mul, hx, hy])
+  intro r f
+  simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, LinearMapClass.map_smul, mapIso_tprod, id_eq,
+    eq_mpr_eq_cast, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv]
+  apply congrArg
+  erw [TensorStructure.contr_tprod_isEmpty]
+  erw [mapIso_tprod]
+  apply congrArg
+  funext l
+  rw [← LinearEquiv.symm_apply_eq]
+  simp only [colorModuleCast, Equiv.cast_symm, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv,
+    Function.comp_apply, LinearEquiv.coe_mk, Equiv.cast_apply, LinearEquiv.coe_symm_mk, cast_cast]
+  apply cast_eq_iff_heq.mpr
+  rw [splitContr_symm_apply_of_hasNoContr _ h]
+  rfl
+
+@[simp]
+lemma contr_contr (T : 𝓣.TensorIndex) : T.contr.contr = T.contr :=
+  T.contr.contr_of_hasNoContr T.index.1.contrIndexList_hasNoContr
+
+@[simp]
+lemma contr_index (T : 𝓣.TensorIndex) : T.contr.index = T.index.contr := rfl
 
 /-!
 
@@ -187,7 +234,7 @@ lemma trans {T₁ T₂ T₃ : 𝓣.TensorIndex} (h1 : Rel T₁ T₂) (h2 : Rel T
   exact h2.2 h2.1
 
 /-- Rel forms an equivalence relation. -/
-lemma equivalence : Equivalence (@Rel _ _ 𝓣 _) where
+lemma isEquivalence : Equivalence (@Rel _ _ 𝓣 _) where
   refl := Rel.refl
   symm := Rel.symm
   trans := Rel.trans
@@ -198,6 +245,29 @@ lemma to_eq {T₁ T₂ : 𝓣.TensorIndex} (h : Rel T₁ T₂) :
 
 end Rel
 
+/-- The structure of a Setoid on `𝓣.TensorIndex` induced by `Rel`. -/
+instance asSetoid : Setoid 𝓣.TensorIndex := ⟨Rel, Rel.isEquivalence⟩
+
+/-- A tensor index is equivalent to its contraction. -/
+lemma self_equiv_contr (T : 𝓣.TensorIndex) : T ≈ T.contr := by
+  apply And.intro
+  simp only [PermContr, contr_index, IndexListColor.contr_contr, List.Perm.refl, true_and]
+  rw [IndexListColor.contr_contr]
+  exact T.index.contr.1.hasNoContr_color_eq_of_id_eq T.index.1.contrIndexList_hasNoContr
+  intro h
+  rw [tensor_eq_of_eq T.contr_contr]
+  simp only [contr_index, mapIso_mapIso]
+  trans 𝓣.mapIso (Equiv.refl _) (by rfl) T.contr.tensor
+  simp only [contr_index, mapIso_refl, LinearEquiv.refl_apply]
+  congr
+  apply Equiv.ext
+  intro x
+  rw [PermContr.toEquiv_contr_eq T.index.contr_contr.symm]
+  rfl
+
+/-! TODO: Show that the product is well defined with respect to Rel. -/
+/-! TODO : Show that addition is well defined with respect to Rel. -/
+
 end TensorIndex
 end
 end TensorStructure
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
index 7482ecd..78eeeb1 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
@@ -77,13 +77,13 @@ noncomputable def fromIndexStringColor {cn : Fin n → realTensorColor.Color}
     (hs : listCharIndexStringBool realTensorColor.Color s.toList = true)
     (hn : n = (IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)).length)
     (hc : IndexListColor.colorPropBool  (IndexString.toIndexList ⟨s, hs⟩))
-    (hd : TensorColor.DualMap.boolFin
+    (hd : TensorColor.ColorMap.DualMap.boolFin
     (IndexString.toIndexList ⟨s, hs⟩).colorMap (cn ∘ Fin.cast hn.symm)) :
     (realLorentzTensor d).TensorIndex :=
   TensorStructure.TensorIndex.mkDualMap T
     ⟨(IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)),
       IndexListColor.colorPropBool_indexListColorProp hc⟩ hn
-      (TensorColor.DualMap.boolFin_DualMap hd)
+      (TensorColor.ColorMap.DualMap.boolFin_DualMap hd)
 
 /-- A tactics used to prove `colorPropBool` for real Lorentz tensors. -/
 macro "prodTactic" : tactic =>
diff --git a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
index d26748a..d663923 100644
--- a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
+++ b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
@@ -19,6 +19,105 @@ noncomputable section
 
 open TensorProduct
 
+
+namespace TensorColor
+
+variable {𝓒 : TensorColor} [DecidableEq 𝓒.Color] [Fintype 𝓒.Color]
+
+variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
+  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
+  [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P]
+
+/-!
+
+## Dual maps
+
+-/
+
+namespace ColorMap
+
+variable (cX : 𝓒.ColorMap X)
+
+def partDual (e : C ⊕ P ≃ X) : 𝓒.ColorMap X :=
+  (Sum.elim (𝓒.τ ∘ cX ∘ e ∘ Sum.inl) (cX ∘ e ∘ Sum.inr) ∘ e.symm)
+
+/-- Two color maps are said to be dual if their quotents are dual. -/
+def DualMap (c₁ c₂ : 𝓒.ColorMap X) : Prop :=
+  𝓒.colorQuot ∘ c₁ = 𝓒.colorQuot ∘ c₂
+
+namespace DualMap
+
+variable {c₁ c₂ c₃ : 𝓒.ColorMap X}
+variable {n : ℕ}
+
+/-- The bool which if `𝓒.colorQuot (c₁ i) = 𝓒.colorQuot (c₂ i)` is true for all `i`. -/
+def boolFin (c₁ c₂ : 𝓒.ColorMap (Fin n)) : Bool :=
+  (Fin.list n).all fun i => if 𝓒.colorQuot (c₁ i) = 𝓒.colorQuot (c₂ i) then true else false
+
+lemma boolFin_DualMap {c₁ c₂ : 𝓒.ColorMap (Fin n)} (h : boolFin c₁ c₂ = true) :
+    DualMap c₁ c₂ := by
+  simp [boolFin] at h
+  simp [DualMap]
+  funext x
+  have h2 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by
+    have h1' : (Fin.list n)[m] = m := by
+      erw [Fin.getElem_list]
+      rfl
+    rw [← h1']
+    apply List.getElem_mem
+  exact h x (h2 _)
+
+lemma refl : DualMap c₁ c₁ := by
+  simp [DualMap]
+
+lemma symm (h : DualMap c₁ c₂) : DualMap c₂ c₁ := by
+  rw [DualMap] at h ⊢
+  exact h.symm
+
+lemma trans (h : DualMap c₁ c₂) (h' : DualMap c₂ c₃) : DualMap c₁ c₃ := by
+  rw [DualMap] at h h' ⊢
+  exact h.trans h'
+
+/-- The splitting of `X` given two color maps based on the equality of the color. -/
+def split (c₁ c₂ : 𝓒.ColorMap X) : { x // c₁ x ≠ c₂ x} ⊕ { x // c₁ x = c₂ x} ≃ X :=
+  ((Equiv.Set.sumCompl {x | c₁ x = c₂ x}).symm.trans (Equiv.sumComm _ _)).symm
+
+lemma dual_eq_of_neq (h : DualMap c₁ c₂) {x : X} (h' : c₁ x ≠ c₂ x) :
+    𝓒.τ (c₁ x) = c₂ x := by
+  rw [DualMap] at h
+  have h1 := congrFun h x
+  simp [colorQuot, HasEquiv.Equiv, Setoid.r, colorRel] at h1
+  simp_all only [ne_eq, false_or]
+  exact 𝓒.τ_involutive (c₂ x)
+
+@[simp]
+lemma split_dual (h : DualMap c₁ c₂) : c₁.partDual (split c₁ c₂) = c₂ := by
+  rw [partDual, Equiv.comp_symm_eq]
+  funext x
+  match x with
+  | Sum.inl x =>
+    exact h.dual_eq_of_neq x.2
+  | Sum.inr x =>
+    exact x.2
+
+@[simp]
+lemma split_dual' (h : DualMap c₁ c₂) : c₂.partDual (split c₁ c₂) = c₁ := by
+  rw [partDual, Equiv.comp_symm_eq]
+  funext x
+  match x with
+  | Sum.inl x =>
+    change 𝓒.τ (c₂ x) = c₁ x
+    rw [← h.dual_eq_of_neq x.2]
+    exact (𝓒.τ_involutive (c₁ x))
+  | Sum.inr x =>
+    exact x.2.symm
+
+end DualMap
+
+end ColorMap
+end TensorColor
+
+
 variable {R : Type} [CommSemiring R]
 
 namespace TensorStructure
@@ -28,8 +127,8 @@ variable (𝓣 : TensorStructure R)
 variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
   [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
   [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P]
-  {cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color}
-  {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
+  {cX cX2 : 𝓣.ColorMap X} {cY : 𝓣.ColorMap Y} {cZ : 𝓣.ColorMap Z}
+  {cW : 𝓣.ColorMap W} {cY' : 𝓣.ColorMap Y'} {μ ν: 𝓣.Color}
 
 variable {G H : Type} [Group G] [Group H] [MulActionTensor G 𝓣]
 local infixl:101 " • " => 𝓣.rep
@@ -199,12 +298,9 @@ lemma dualize_cond' (e : C ⊕ P ≃ X) :
   | Sum.inl x => simp
   | Sum.inr x => simp
 
-/-! TODO: Show that `dualize` is equivariant with respect to the group action. -/
-
 /-- Given an equivalence `C ⊕ P ≃ X` dualizes those indices of a tensor which correspond to
   `C` whilst leaving the indices `P` invariant. -/
-def dualize (e : C ⊕ P ≃ X) : 𝓣.Tensor cX ≃ₗ[R]
-    𝓣.Tensor (Sum.elim (𝓣.τ ∘ cX ∘ e ∘ Sum.inl) (cX ∘ e ∘ Sum.inr) ∘ e.symm) :=
+def dualize (e : C ⊕ P ≃ X) : 𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (cX.partDual e) :=
   𝓣.mapIso e.symm (𝓣.dualize_cond e) ≪≫ₗ
   (𝓣.tensoratorEquiv _ _).symm ≪≫ₗ
   TensorProduct.congr 𝓣.dualizeAll (LinearEquiv.refl _ _) ≪≫ₗ
@@ -232,95 +328,3 @@ lemma dualize_equivariant_apply (e : C ⊕ P ≃ X) (g : G) (x : 𝓣.Tensor cX)
 end TensorStructure
 
 end
-namespace TensorColor
-
-variable {𝓒 : TensorColor} [DecidableEq 𝓒.Color] [Fintype 𝓒.Color]
-
-variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
-  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
-  [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P]
-
-/-!
-
-## Dual maps
-
--/
-
-/-- Two color maps are said to be dual if their quotents are dual. -/
-def DualMap (c₁ : X → 𝓒.Color) (c₂ : X → 𝓒.Color) : Prop :=
-  𝓒.colorQuot ∘ c₁ = 𝓒.colorQuot ∘ c₂
-
-namespace DualMap
-
-variable {c₁ c₂ c₃ : X → 𝓒.Color}
-variable {n : ℕ}
-
-/-- The bool which if `𝓒.colorQuot (c₁ i) = 𝓒.colorQuot (c₂ i)` is true for all `i`. -/
-def boolFin (c₁ c₂ : Fin n → 𝓒.Color) : Bool :=
-  (Fin.list n).all fun i => if 𝓒.colorQuot (c₁ i) = 𝓒.colorQuot (c₂ i) then true else false
-
-lemma boolFin_DualMap {c₁ c₂ : Fin n → 𝓒.Color} (h : boolFin c₁ c₂ = true) :
-    DualMap c₁ c₂ := by
-  simp [boolFin] at h
-  simp [DualMap]
-  funext x
-  have h2 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by
-    have h1' : (Fin.list n)[m] = m := by
-      erw [Fin.getElem_list]
-      rfl
-    rw [← h1']
-    apply List.getElem_mem
-  exact h x (h2 _)
-
-lemma refl : DualMap c₁ c₁ := by
-  simp [DualMap]
-
-lemma symm (h : DualMap c₁ c₂) : DualMap c₂ c₁ := by
-  rw [DualMap] at h ⊢
-  exact h.symm
-
-lemma trans (h : DualMap c₁ c₂) (h' : DualMap c₂ c₃) : DualMap c₁ c₃ := by
-  rw [DualMap] at h h' ⊢
-  exact h.trans h'
-
-/-- The splitting of `X` given two color maps based on the equality of the color. -/
-def split (c₁ c₂ : X → 𝓒.Color) : { x // c₁ x ≠ c₂ x} ⊕ { x // c₁ x = c₂ x} ≃ X :=
-  ((Equiv.Set.sumCompl {x | c₁ x = c₂ x}).symm.trans (Equiv.sumComm _ _)).symm
-
-lemma dual_eq_of_neq (h : DualMap c₁ c₂) {x : X} (h' : c₁ x ≠ c₂ x) :
-    𝓒.τ (c₁ x) = c₂ x := by
-  rw [DualMap] at h
-  have h1 := congrFun h x
-  simp [colorQuot, HasEquiv.Equiv, Setoid.r, colorRel] at h1
-  simp_all only [ne_eq, false_or]
-  exact 𝓒.τ_involutive (c₂ x)
-
-@[simp]
-lemma split_dual (h : DualMap c₁ c₂) :
-    Sum.elim (𝓒.τ ∘ c₁ ∘ (split c₁ c₂) ∘ Sum.inl) (c₁ ∘ (split c₁ c₂) ∘ Sum.inr)
-    ∘ (split c₁ c₂).symm = c₂ := by
-  rw [Equiv.comp_symm_eq]
-  funext x
-  match x with
-  | Sum.inl x =>
-    exact h.dual_eq_of_neq x.2
-  | Sum.inr x =>
-    exact x.2
-
-@[simp]
-lemma split_dual' (h : DualMap c₁ c₂) :
-    Sum.elim (𝓒.τ ∘ c₂ ∘ (split c₁ c₂) ∘ Sum.inl) (c₂ ∘ (split c₁ c₂) ∘ Sum.inr) ∘
-    (split c₁ c₂).symm = c₁ := by
-  rw [Equiv.comp_symm_eq]
-  funext x
-  match x with
-  | Sum.inl x =>
-    change 𝓒.τ (c₂ x) = c₁ x
-    rw [← h.dual_eq_of_neq x.2]
-    exact (𝓒.τ_involutive (c₁ x))
-  | Sum.inr x =>
-    exact x.2.symm
-
-end DualMap
-
-end TensorColor