Merge pull request #238 from HEPLean/LightLikeComplex

feat: Def of general metric tensor and unit tensor

HepLean.lean

@@ -124,6 +124,11 @@ import HepLean.Tensors.OverColor.Discrete
 import HepLean.Tensors.OverColor.Functors
 import HepLean.Tensors.OverColor.Iso
 import HepLean.Tensors.OverColor.Lift
+import HepLean.Tensors.TensorSpecies.Basic
+import HepLean.Tensors.TensorSpecies.ContractLemmas
+import HepLean.Tensors.TensorSpecies.MetricTensor
+import HepLean.Tensors.TensorSpecies.RepIso
+import HepLean.Tensors.TensorSpecies.UnitTensor
 import HepLean.Tensors.Tree.Basic
 import HepLean.Tensors.Tree.Dot
 import HepLean.Tensors.Tree.Elab

HepLean/Mathematics/Fin.lean

@@ -279,6 +279,16 @@ def finExtractOnePerm (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ
   right_inv x := by
     simpa using congrFun (finExtractOnPermHom_inv (σ i) σ.symm) x
 
+@[simp]
+lemma finExtractOnePerm_apply (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ)
+    (x : Fin n.succ) : finExtractOnePerm i σ x = predAboveI (σ i)
+    (σ ((finExtractOne i).symm (Sum.inr x))) := rfl
+
+@[simp]
+lemma finExtractOnePerm_symm_apply (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ)
+    (x : Fin n.succ) : (finExtractOnePerm i σ).symm x = predAboveI (σ.symm (σ i))
+    (σ.symm ((finExtractOne (σ i)).symm (Sum.inr x))) := 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) :
@@ -322,4 +332,28 @@ lemma finExtractTwo_apply_snd {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
   rw [← Equiv.eq_symm_apply]
   simp
 
+/-- Takes two maps `Fin n → Fin n` and returns the equivelance they form. -/
+def finMapToEquiv (f1 : Fin n → Fin m) (f2 : Fin m → Fin n)
+    (h : ∀ x, f1 (f2 x) = x := by decide)
+    (h' : ∀ x, f2 (f1 x) = x := by decide) : Fin n ≃ Fin m where
+  toFun := f1
+  invFun := f2
+  left_inv := h'
+  right_inv := h
+
+@[simp]
+lemma finMapToEquiv_apply {f1 : Fin n → Fin m} {f2 : Fin m → Fin n}
+    {h : ∀ x, f1 (f2 x) = x} {h' : ∀ x, f2 (f1 x) = x} (x : Fin n) :
+    finMapToEquiv f1 f2 h h' x = f1 x := rfl
+
+@[simp]
+lemma finMapToEquiv_symm_apply {f1 : Fin n → Fin m} {f2 : Fin m → Fin n}
+    {h : ∀ x, f1 (f2 x) = x} {h' : ∀ x, f2 (f1 x) = x} (x : Fin m) :
+    (finMapToEquiv f1 f2 h h').symm x = f2 x := rfl
+
+lemma finMapToEquiv_symm_eq {f1 : Fin n → Fin m} {f2 : Fin m → Fin n}
+    {h : ∀ x, f1 (f2 x) = x} {h' : ∀ x, f2 (f1 x) = x} :
+    (finMapToEquiv f1 f2 h h').symm = finMapToEquiv f2 f1 h' h := by
+  rfl
+
 end HepLean.Fin

HepLean/Tensors/OverColor/Basic.lean

@@ -100,6 +100,9 @@ def toIso (m : f ⟶ g) : f ≅ g := {
     simp only [CategoryStruct.comp, Iso.symm_self_id, Iso.refl_hom, Over.id_left, types_id_apply]
     rfl}
 
+@[simp]
+lemma hom_comp (m : f ⟶ g) (n : g ⟶ h) : (m ≫ n).hom = m.hom ≫ n.hom := by rfl
+
 end Hom
 
 section monoidal
@@ -273,12 +276,39 @@ def mk (f : X → C) : OverColor C := Over.mk f
 lemma mk_hom (f : X → C) : (mk f).hom = f := rfl
 open MonoidalCategory
 
+@[simp]
+lemma mk_left (f : X → C) : (mk f).left = X := rfl
+
 lemma Hom.fin_ext {n : ℕ} {f g : Fin n → C} (σ σ' : OverColor.mk f ⟶ OverColor.mk g)
     (h : ∀ (i : Fin n), σ.hom.left i = σ'.hom.left i) : σ = σ' := by
   apply Hom.ext
   ext i
   apply h
 
+@[simp]
+lemma β_hom_toEquiv (f : X → C) (g : Y → C) :
+    Hom.toEquiv (β_ (OverColor.mk f) (OverColor.mk g)).hom = Equiv.sumComm X Y := by
+  rfl
+
+@[simp]
+lemma β_inv_toEquiv (f : X → C) (g : Y → C) :
+    Hom.toEquiv (β_ (OverColor.mk f) (OverColor.mk g)).inv = Equiv.sumComm Y X := by
+  rfl
+
+@[simp]
+lemma whiskeringLeft_toEquiv (f : X → C) (g : Y → C) (h : Z → C)
+    (σ : OverColor.mk f ⟶ OverColor.mk g) :
+    Hom.toEquiv (OverColor.mk h ◁ σ) = (Equiv.refl Z).sumCongr (Hom.toEquiv σ) := by
+  simp [MonoidalCategory.whiskerLeft]
+  rfl
+
+@[simp]
+lemma whiskeringRight_toEquiv (f : X → C) (g : Y → C) (h : Z → C)
+    (σ : OverColor.mk f ⟶ OverColor.mk g) :
+    Hom.toEquiv (σ ▷ OverColor.mk h) = (Hom.toEquiv σ).sumCongr (Equiv.refl Z) := by
+  simp [MonoidalCategory.whiskerLeft]
+  rfl
+
 end OverColor
 
 end IndexNotation

HepLean/Tensors/OverColor/Discrete.lean

@@ -111,6 +111,89 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
       HepLean.PiTensorProduct.elimPureTensor]
     exact (LinearEquiv.eq_symm_apply _).mp rfl
 
+lemma pairIsoSep_inv_tprod {c1 c2 : C} (fx : (i : (𝟭 Type).obj (OverColor.mk ![c1, c2]).left) →
+    CoeSort.coe (F.obj { as := (OverColor.mk ![c1, c2]).hom i })) :
+    (pairIsoSep F).inv.hom (PiTensorProduct.tprod k fx) = fx (0 : Fin 2) ⊗ₜ fx (1 : Fin 2) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, Nat.succ_eq_add_one, Nat.reduceAdd,
+    pairIsoSep, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
+    Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_assoc, Iso.trans_inv, Iso.symm_inv,
+    Functor.mapIso_hom, tensorIso_hom, Iso.trans_hom, Iso.symm_hom, Functor.mapIso_inv, tensor_comp,
+    Category.assoc, Action.comp_hom, Action.instMonoidalCategory_tensorHom_hom, mk_left,
+    Functor.id_obj, mk_hom, ModuleCat.coe_comp, Function.comp_apply, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj]
+  erw [lift.map_tprod]
+  erw [lift.μIso_inv_tprod]
+  change (((forgetLiftApp F c1).hom.hom (((lift.obj F).map (mkIso _).inv).hom
+    ((PiTensorProduct.tprod k) fun i =>
+    (lift.discreteFunctorMapEqIso F _) (fx ((Hom.toEquiv fin2Iso.hom).symm (Sum.inl i)))))) ⊗ₜ[k]
+    (forgetLiftApp F c2).hom.hom (((lift.obj F).map (mkIso _).inv).hom ((PiTensorProduct.tprod k)
+    fun i =>
+    (lift.discreteFunctorMapEqIso F _) (fx ((Hom.toEquiv fin2Iso.hom).symm (Sum.inr i)))))) = _
+  congr 1
+  · rw [lift.map_tprod]
+    rw [forgetLiftApp_hom_hom_apply_eq]
+    apply congrArg
+    funext x
+    match x with
+    | (0 : Fin 1) =>
+      simp only [mk_hom, Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Matrix.cons_val_zero,
+        equivToIso_mkIso_inv, Equiv.refl_symm, lift.discreteFunctorMapEqIso, eqToIso_refl,
+        Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv, Matrix.cons_val_one,
+        Matrix.head_cons, instMonoidalCategoryStruct_tensorObj_left, Functor.id_obj,
+        LinearEquiv.ofLinear_apply]
+      rfl
+  · rw [lift.map_tprod]
+    rw [forgetLiftApp_hom_hom_apply_eq]
+    apply congrArg
+    funext x
+    match x with
+    | (0 : Fin 1) =>
+      simp only [mk_hom, Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Matrix.cons_val_one,
+        Matrix.head_cons, equivToIso_mkIso_inv, Equiv.refl_symm, lift.discreteFunctorMapEqIso,
+        eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv,
+        Matrix.cons_val_zero, instMonoidalCategoryStruct_tensorObj_left, Functor.id_obj,
+        LinearEquiv.ofLinear_apply]
+      rfl
+
+open HepLean.Fin
+
+/-! TODO: Find a better place for this. -/
+lemma pairIsoSep_β_perm_cond (c1 c2 : C) : ∀ (x : Fin (Nat.succ 0).succ), ![c2, c1] x =
+    (![c1, c2] ∘ ⇑(finMapToEquiv ![1, 0] ![1, 0]).symm) x:= by
+  intro x
+  fin_cases x
+  · rfl
+  · rfl
+
+lemma pairIsoSep_β {c1 c2 : C} (x : ↑(F.obj { as := c1 } ⊗ F.obj { as := c2 }).V) :
+    (Discrete.pairIsoSep F).hom.hom ((β_ (F.obj (Discrete.mk c1)) _).hom.hom x) =
+    ((lift.obj F).map ((OverColor.equivToHomEq (finMapToEquiv ![1, 0] ![1, 0])
+    (pairIsoSep_β_perm_cond c1 c2)))).hom
+    ((Discrete.pairIsoSep F).hom.hom x) := by
+  have h1 : (Discrete.pairIsoSep F).hom.hom ∘ₗ
+      (β_ (F.obj (Discrete.mk c1)) (F.obj (Discrete.mk c2))).hom.hom
+      = ((lift.obj F).map ((OverColor.equivToHomEq
+      (finMapToEquiv ![1, 0] ![1, 0]) (pairIsoSep_β_perm_cond c1 c2)))).hom ∘ₗ
+      (Discrete.pairIsoSep F).hom.hom := by
+    apply TensorProduct.ext'
+    intro x y
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Equivalence.symm_inverse,
+      Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+      Action.instMonoidalCategory_tensorObj_V, LinearMap.coe_comp, Function.comp_apply, Fin.isValue]
+    change (Discrete.pairIsoSep F).hom.hom (y ⊗ₜ x) = ((lift.obj F).map
+      ((OverColor.equivToHomEq _ (pairIsoSep_β_perm_cond c1 c2)))).hom
+      ((Discrete.pairIsoSep F).hom.hom (x ⊗ₜ y))
+    rw [Discrete.pairIsoSep_tmul, Discrete.pairIsoSep_tmul]
+    erw [OverColor.lift.map_tprod]
+    apply congrArg
+    funext i
+    fin_cases i
+    · simp [lift.discreteFunctorMapEqIso]
+      rfl
+    · simp [lift.discreteFunctorMapEqIso]
+      rfl
+  exact congrFun (congrArg (fun f => f.toFun) h1) _
+
 /-- The isomorphism between
   `F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ⊗ F.obj (Discrete.mk c3)` and
   `(lift.obj F).obj (OverColor.mk ![c1,c2])` formed by the tensorate. -/
@@ -175,6 +258,24 @@ lemma pairτ_tmul {c : C} (x : F.obj (Discrete.mk c))
 def τPair (τ : C → C) : Discrete C ⥤ Rep k G :=
   ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F) ⊗ F
 
+/-!
+
+## A need lemma about rep
+
+-/
+
+@[simp]
+lemma rep_iso_inv_hom_apply (x y : Rep k G) (f : x ≅ y) (i : x) :
+    f.inv.hom (f.hom.hom i) = i := by
+  change (f.hom ≫ f.inv).hom i = i
+  simp
+
+@[simp]
+lemma rep_iso_hom_inv_apply (x y : Rep k G) (f : x ≅ y) (i : y) :
+    f.hom.hom (f.inv.hom i) = i := by
+  change (f.inv ≫ f.hom).hom i = i
+  simp
+
 end
 end Discrete
 end OverColor

HepLean/Tensors/OverColor/Iso.lean

@@ -32,6 +32,11 @@ lemma equivToIso_homToEquiv {c : X → C} (e : X ≃ Y) :
     Hom.toEquiv (equivToIso (c := c) e).hom = e := by
   rfl
 
+@[simp]
+lemma equivToIso_inv_homToEquiv {c : X → C} (e : X ≃ Y) :
+    Hom.toEquiv (equivToIso (c := c) e).inv = e.symm := by
+  rfl
+
 /-- The homomorphism between `c : X → C` and `c ∘ e.symm` as objects in `OverColor C` for an
   equivalence `e`. -/
 def equivToHom {c : X → C} (e : X ≃ Y) : mk c ⟶ mk (c ∘ e.symm) :=
@@ -65,6 +70,17 @@ lemma mkIso_refl_hom {c : X → C} : (mkIso (by rfl : c =c)).hom = 𝟙 _ := by
   rw [mkIso]
   rfl
 
+lemma mkIso_hom_hom_left {c1 c2 : X → C} (h : c1 = c2) : (mkIso h).hom.hom.left =
+    (Equiv.refl X).toFun := by
+  rw [mkIso]
+  rfl
+
+@[simp]
+lemma mkIso_hom_hom_left_apply {c1 c2 : X → C} (h : c1 = c2) (x : X) :
+    (mkIso h).hom.hom.left x = x := by
+  rw [mkIso_hom_hom_left]
+  rfl
+
 @[simp]
 lemma equivToIso_mkIso_hom {c1 c2 : X → C} (h : c1 = c2) :
     Hom.toEquiv (mkIso h).hom = Equiv.refl _ := by
@@ -81,6 +97,17 @@ def equivToHomEq {c : X → C} {c1 : Y → C} (e : X ≃ Y)
     (h : ∀ x, c1 x = (c ∘ e.symm) x := by decide) : mk c ⟶ mk c1 :=
   (equivToHom e).trans (mkIso (funext fun x => (h x).symm)).hom
 
+@[simp]
+lemma equivToHomEq_hom_left {c : X → C} {c1 : Y → C} (e : X ≃ Y)
+    (h : ∀ x, c1 x = (c ∘ e.symm) x := by decide) : (equivToHomEq e h).hom.left =
+    e.toFun := by
+  rfl
+
+@[simp]
+lemma equivToHomEq_toEquiv {c : X → C} {c1 : Y → C} (e : X ≃ Y)
+    (h : ∀ x, c1 x = (c ∘ e.symm) x := by decide) : Hom.toEquiv (equivToHomEq e h) = e := by
+    rfl
+
 /-- The isomorphism splitting a `mk c` for `Fin 2 → C` into the tensor product of
   the `Fin 1 → C` maps defined by `c 0` and `c 1`. -/
 def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by
@@ -163,6 +190,15 @@ def extractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
     equivToHomEq (Equiv.refl _) (by simp) ≫ extractOne j (extractOne i σ) ≫
     equivToHomEq (Equiv.refl _) (by simp)
 
+@[simp]
+lemma extractTwo_hom_left_apply {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ)
+    {c1 c2 : Fin n.succ.succ.succ → C} (σ : mk c1 ⟶ mk c2) (x : Fin n.succ) :
+    (extractTwo i j σ).hom.left x =
+      (finExtractOnePerm ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
+      (finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))) x := by
+  simp only [extractTwo, extractOne]
+  rfl
+
 /-- Removes a given `i : Fin n.succ.succ` and `j : Fin n.succ` from a morphism in `OverColor C`.
   This is from and to different (by equivalent) objects to `extractTwo`. -/
 def extractTwoAux {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
@@ -231,7 +267,7 @@ lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fi
   simp only [Nat.succ_eq_add_one, Equiv.apply_symm_apply]
   match k with
   | Sum.inl (Sum.inl 0) =>
-    simp
+    simp [-OverColor.mk_left]
   | Sum.inl (Sum.inr 0) =>
     simp only [Fin.isValue, finExtractTwo_symm_inl_inr_apply, Sum.map_inl, id_eq]
     have h1 : ((Hom.toEquiv σ) (Fin.succAbove

HepLean/Tensors/TensorSpecies/Basic.lean

@@ -0,0 +1,543 @@
+/-
+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.Iso
+import HepLean.Tensors.OverColor.Discrete
+import HepLean.Tensors.OverColor.Lift
+import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
+/-!
+
+# Tensor species
+
+- A tensor species is a structure including all of the ingredients needed to define a type of
+  tensor.
+- Examples of tensor species will include real Lorentz tensors, complex Lorentz tensors, and
+  Einstien tensors.
+- Tensor species are built upon symmetric monoidal categories.
+
+-/
+
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+
+/-- The structure of a type of tensors e.g. Lorentz tensors, ordinary tensors
+  (vectors and matrices), complex Lorentz tensors. -/
+structure TensorSpecies where
+  /-- The commutative ring over which we want to consider the tensors to live in,
+    usually `ℝ` or `ℂ`. -/
+  k : Type
+  /-- An instance of `k` as a commutative ring. -/
+  k_commRing : CommRing k
+  /-- The symmetry group acting on these tensor e.g. the Lorentz group or SL(2,ℂ). -/
+  G : Type
+  /-- An instance of `G` as a group. -/
+  G_group : Group G
+  /-- The colors of indices e.g. up or down. -/
+  C : Type
+  /-- A functor from `C` to `Rep k G` giving our building block representations.
+    Equivalently a function `C → Re k G`. -/
+  FD : Discrete C ⥤ Rep k G
+  /-- A specification of the dimension of each color in C. This will be used for explicit
+    evaluation of tensors. -/
+  repDim : C → ℕ
+  /-- repDim is not zero for any color. This allows casting of `ℕ` to `Fin (S.repDim c)`. -/
+  repDim_neZero (c : C) : NeZero (repDim c)
+  /-- A basis for each Module, determined by the evaluation map. -/
+  basis : (c : C) → Basis (Fin (repDim c)) k (FD.obj (Discrete.mk c)).V
+  /-- A map from `C` to `C`. An involution. -/
+  τ : C → C
+  /-- The condition that `τ` is an involution. -/
+  τ_involution : Function.Involutive τ
+  /-- The natural transformation describing contraction. -/
+  contr : OverColor.Discrete.pairτ FD τ ⟶ 𝟙_ (Discrete C ⥤ Rep k G)
+  /-- Contraction is symmetric with respect to duals. -/
+  contr_tmul_symm (c : C) (x : FD.obj (Discrete.mk c))
+      (y : FD.obj (Discrete.mk (τ c))) :
+    (contr.app (Discrete.mk c)).hom (x ⊗ₜ[k] y) = (contr.app (Discrete.mk (τ c))).hom
+    (y ⊗ₜ (FD.map (Discrete.eqToHom (τ_involution c).symm)).hom x)
+  /-- The natural transformation describing the unit. -/
+  unit : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.τPair FD τ
+  /-- The unit is symmetric. -/
+  unit_symm (c : C) :
+    ((unit.app (Discrete.mk c)).hom (1 : k)) =
+    ((FD.obj (Discrete.mk (τ (c)))) ◁
+      (FD.map (Discrete.eqToHom (τ_involution c)))).hom
+    ((β_ (FD.obj (Discrete.mk (τ (τ c)))) (FD.obj (Discrete.mk (τ (c))))).hom.hom
+    ((unit.app (Discrete.mk (τ c))).hom (1 : k)))
+  /-- Contraction with unit leaves invariant. -/
+  contr_unit (c : C) (x : FD.obj (Discrete.mk (c))) :
+    (λ_ (FD.obj (Discrete.mk (c)))).hom.hom
+    (((contr.app (Discrete.mk c)) ▷ (FD.obj (Discrete.mk (c)))).hom
+    ((α_ _ _ (FD.obj (Discrete.mk (c)))).inv.hom
+    (x ⊗ₜ[k] (unit.app (Discrete.mk c)).hom (1 : k)))) = x
+  /-- The natural transformation describing the metric. -/
+  metric : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.pair FD
+  /-- On contracting metrics we get back the unit. -/
+  contr_metric (c : C) :
+    (β_ (FD.obj (Discrete.mk c)) (FD.obj (Discrete.mk (τ c)))).hom.hom
+    (((FD.obj (Discrete.mk c)) ◁ (λ_ (FD.obj (Discrete.mk (τ c)))).hom).hom
+    (((FD.obj (Discrete.mk c)) ◁ ((contr.app (Discrete.mk c)) ▷
+    (FD.obj (Discrete.mk (τ c))))).hom
+    (((FD.obj (Discrete.mk c)) ◁ (α_ (FD.obj (Discrete.mk (c)))
+      (FD.obj (Discrete.mk (τ c))) (FD.obj (Discrete.mk (τ c)))).inv).hom
+    ((α_ (FD.obj (Discrete.mk (c))) (FD.obj (Discrete.mk (c)))
+      (FD.obj (Discrete.mk (τ c)) ⊗ FD.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
+
+namespace TensorSpecies
+open OverColor
+
+variable (S : TensorSpecies)
+
+/-- The field `k` of a TensorSpecies has the instance of a commuative ring. -/
+instance : CommRing S.k := S.k_commRing
+
+/-- The field `G` of a TensorSpecies has the instance of a group. -/
+instance : Group S.G := S.G_group
+
+/-- The field `repDim` of a TensorSpecies is non-zero for all colors. -/
+instance (c : S.C) : NeZero (S.repDim c) := S.repDim_neZero c
+
+/-- The lift of the functor `S.F` to a monoidal functor. -/
+def F : BraidedFunctor (OverColor S.C) (Rep S.k S.G) := (OverColor.lift).obj S.FD
+
+/- The definition of `F` as a lemma. -/
+lemma F_def : F S = (OverColor.lift).obj S.FD := rfl
+
+lemma perm_contr_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ → S.C}
+    {i : Fin n.succ.succ} {j : Fin n.succ}
+    (h : c1 (i.succAbove j) = S.τ (c1 i)) (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
+    c (Fin.succAbove ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)) =
+    S.τ (c ((Hom.toEquiv σ).symm i)) := by
+  have h1 := Hom.toEquiv_comp_apply σ
+  simp only [Nat.succ_eq_add_one, Functor.const_obj_obj, mk_hom] at h1
+  rw [h1, h1]
+  simp only [Nat.succ_eq_add_one, extractOne_homToEquiv, Equiv.apply_symm_apply]
+  rw [← h]
+  congr
+  simp only [Nat.succ_eq_add_one, HepLean.Fin.finExtractOnePerm, HepLean.Fin.finExtractOnPermHom,
+    HepLean.Fin.finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk]
+  erw [Equiv.apply_symm_apply]
+  rw [HepLean.Fin.succsAbove_predAboveI]
+  erw [Equiv.apply_symm_apply]
+  simp only [Nat.succ_eq_add_one, ne_eq]
+  erw [Equiv.apply_eq_iff_eq]
+  exact (Fin.succAbove_ne i j).symm
+
+/-- The isomorphism between the image of a map `Fin 1 ⊕ Fin 1 → S.C` contructed by `finExtractTwo`
+  under `S.F.obj`, and an object in the image of `OverColor.Discrete.pairτ S.FD`. -/
+def contrFin1Fin1 {n : ℕ} (c : Fin n.succ.succ → S.C)
+    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) :
+    S.F.obj (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) ≅
+    (OverColor.Discrete.pairτ S.FD S.τ).obj { as := c i } := by
+  apply (S.F.mapIso
+    (OverColor.mkSum (((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)))).trans
+  apply (S.F.μIso _ _).symm.trans
+  apply tensorIso ?_ ?_
+  · symm
+    apply (OverColor.forgetLiftApp S.FD (c i)).symm.trans
+    apply S.F.mapIso
+    apply OverColor.mkIso
+    funext x
+    fin_cases x
+    rfl
+  · symm
+    apply (OverColor.forgetLiftApp S.FD (S.τ (c i))).symm.trans
+    apply S.F.mapIso
+    apply OverColor.mkIso
+    funext x
+    fin_cases x
+    simp [h]
+
+lemma contrFin1Fin1_inv_tmul {n : ℕ} (c : Fin n.succ.succ → S.C)
+    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i))
+    (x : S.FD.obj { as := c i })
+    (y : S.FD.obj { as := S.τ (c i) }) :
+    (S.contrFin1Fin1 c i j h).inv.hom (x ⊗ₜ[S.k] y) =
+    PiTensorProduct.tprod S.k (fun k =>
+    match k with | Sum.inl 0 => x | Sum.inr 0 => (S.FD.map
+    (eqToHom (by simp [h]))).hom y) := by
+  simp only [Nat.succ_eq_add_one, contrFin1Fin1, Functor.comp_obj, Discrete.functor_obj_eq_as,
+    Function.comp_apply, Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_inv, tensorIso_inv,
+    Iso.symm_inv, Functor.mapIso_hom, tensor_comp, MonoidalFunctor.μIso_hom, Category.assoc,
+    LaxMonoidalFunctor.μ_natural, Functor.mapIso_inv, Action.comp_hom,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorHom_hom,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Functor.id_obj, mk_hom,
+    Fin.isValue]
+  change (S.F.map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
+    ((S.F.map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
+      ((S.F.μ (OverColor.mk fun _ => c i) (OverColor.mk fun _ => S.τ (c i))).hom
+        ((((OverColor.forgetLiftApp S.FD (c i)).inv.hom x) ⊗ₜ[S.k]
+        ((OverColor.forgetLiftApp S.FD (S.τ (c i))).inv.hom y))))) = _
+  simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    forgetLiftApp, Action.mkIso_inv_hom, LinearEquiv.toModuleIso_inv, Fin.isValue]
+  erw [OverColor.forgetLiftAppV_symm_apply,
+    OverColor.forgetLiftAppV_symm_apply S.FD (S.τ (c i))]
+  change ((OverColor.lift.obj S.FD).map (OverColor.mkSum
+    ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
+    (((OverColor.lift.obj S.FD).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
+    (((OverColor.lift.obj S.FD).μ (OverColor.mk fun _ => c i)
+    (OverColor.mk fun _ => S.τ (c i))).hom
+    (((PiTensorProduct.tprod S.k) fun _ => x) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun _ => y))) = _
+  rw [OverColor.lift.obj_μ_tprod_tmul S.FD]
+  change ((OverColor.lift.obj S.FD).map
+    (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
+    (((OverColor.lift.obj S.FD).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
+    ((PiTensorProduct.tprod S.k) _)) = _
+  rw [OverColor.lift.map_tprod S.FD]
+  change ((OverColor.lift.obj S.FD).map
+    (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
+    ((PiTensorProduct.tprod S.k _)) = _
+  rw [OverColor.lift.map_tprod S.FD]
+  apply congrArg
+  funext r
+  match r with
+  | Sum.inl 0 =>
+    simp only [Nat.succ_eq_add_one, mk_hom, Fin.isValue, Function.comp_apply,
+      instMonoidalCategoryStruct_tensorObj_left, mkSum_inv_homToEquiv, Equiv.refl_symm,
+      instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, lift.discreteSumEquiv, Sum.elim_inl,
+      Sum.elim_inr, HepLean.PiTensorProduct.elimPureTensor]
+    simp only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
+      Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
+    rfl
+  | Sum.inr 0 =>
+    simp only [Nat.succ_eq_add_one, mk_hom, Fin.isValue, Function.comp_apply,
+      instMonoidalCategoryStruct_tensorObj_left, mkSum_inv_homToEquiv, Equiv.refl_symm,
+      instMonoidalCategoryStruct_tensorObj_hom, lift.discreteFunctorMapEqIso, eqToIso_refl,
+      Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv, Functor.mapIso_hom,
+      eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, Functor.id_obj, lift.discreteSumEquiv,
+      Sum.elim_inl, Sum.elim_inr, HepLean.PiTensorProduct.elimPureTensor,
+      LinearEquiv.ofLinear_apply]
+    rfl
+
+lemma contrFin1Fin1_hom_hom_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
+    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i))
+    (x : (k : Fin 1 ⊕ Fin 1) → (S.FD.obj
+      { as := (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).hom k })) :
+    (S.contrFin1Fin1 c i j h).hom.hom (PiTensorProduct.tprod S.k x) =
+    x (Sum.inl 0) ⊗ₜ[S.k] ((S.FD.map (eqToHom (by simp [h]))).hom (x (Sum.inr 0))) := by
+  change ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).hom _ = _
+  trans ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).toLinearEquiv
+    (PiTensorProduct.tprod S.k x)
+  · rfl
+  erw [← LinearEquiv.eq_symm_apply]
+  erw [contrFin1Fin1_inv_tmul]
+  congr
+  funext i
+  match i with
+  | Sum.inl 0 =>
+    rfl
+  | Sum.inr 0 =>
+    simp only [Nat.succ_eq_add_one, Fin.isValue, mk_hom, Function.comp_apply,
+      Discrete.functor_obj_eq_as]
+    change _ = ((S.FD.map (eqToHom _)) ≫ (S.FD.map (eqToHom _))).hom (x (Sum.inr 0))
+    rw [← Functor.map_comp]
+    simp
+  exact h
+
+/-- The isomorphism of objects in `Rep S.k S.G` given an `i` in `Fin n.succ.succ` and
+  a `j` in `Fin n.succ` allowing us to undertake contraction. -/
+def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C)
+    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) :
+    S.F.obj (OverColor.mk c) ≅ ((OverColor.Discrete.pairτ S.FD S.τ).obj
+      (Discrete.mk (c i))) ⊗
+      (OverColor.lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
+  (S.F.mapIso (OverColor.equivToIso (HepLean.Fin.finExtractTwo i j))).trans <|
+  (S.F.mapIso (OverColor.mkSum (c ∘ (HepLean.Fin.finExtractTwo i j).symm))).trans <|
+  (S.F.μIso _ _).symm.trans <| by
+  refine tensorIso (S.contrFin1Fin1 c i j h) (S.F.mapIso (OverColor.mkIso (by ext x; simp)))
+
+lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C}
+    {i : Fin n.succ.succ} {j : Fin n.succ} {h : c1 (i.succAbove j) = S.τ (c1 i)} :
+    (S.contrIso c1 i j h).hom.hom =
+    (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom ≫
+    (S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom ≫
+    (S.F.μIso (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
+    (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom ≫
+    ((S.contrFin1Fin1 c1 i j h).hom.hom ⊗
+    (S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom) := by
+  rfl
+
+/-- `contrMap` is a function that takes a natural number `n`, a function `c` from
+`Fin n.succ.succ` to `S.C`, an index `i` of type `Fin n.succ.succ`, an index `j` of type
+`Fin n.succ`, and a proof `h` that `c (i.succAbove j) = S.τ (c i)`. It returns a morphism
+corresponding to the contraction of the `i`th index with the `i.succAbove j` index.
+--/
+def contrMap {n : ℕ} (c : Fin n.succ.succ → S.C)
+    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) :
+    S.F.obj (OverColor.mk c) ⟶
+    S.F.obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
+  (S.contrIso c i j h).hom ≫
+  (tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫
+  (MonoidalCategory.leftUnitor _).hom
+
+/-- Casts an element of the monoidal unit of `Rep S.k S.G` to the field `S.k`. -/
+def castToField (v : (↑((𝟙_ (Discrete S.C ⥤ Rep S.k S.G)).obj { as := c }).V)) : S.k := v
+
+/-- Casts an element of `(S.F.obj (OverColor.mk c)).V` for `c` a map from `Fin 0` to an
+  element of the field. -/
+def castFin0ToField {c : Fin 0 → S.C} : (S.F.obj (OverColor.mk c)).V →ₗ[S.k] S.k :=
+  (PiTensorProduct.isEmptyEquiv (Fin 0)).toLinearMap
+
+lemma castFin0ToField_tprod {c : Fin 0 → S.C}
+    (x : (i : Fin 0) → S.FD.obj (Discrete.mk (c i))) :
+    castFin0ToField S (PiTensorProduct.tprod S.k x) = 1 := by
+  simp only [castFin0ToField, mk_hom, Functor.id_obj, LinearEquiv.coe_coe]
+  erw [PiTensorProduct.isEmptyEquiv_apply_tprod]
+
+lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
+    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i))
+    (x : (i : Fin n.succ.succ) → S.FD.obj (Discrete.mk (c i))) :
+    (S.contrMap c i j h).hom (PiTensorProduct.tprod S.k x) =
+    (S.castToField ((S.contr.app (Discrete.mk (c i))).hom ((x i) ⊗ₜ[S.k]
+    (S.FD.map (Discrete.eqToHom h)).hom (x (i.succAbove j)))) : S.k)
+    • (PiTensorProduct.tprod S.k (fun k => x (i.succAbove (j.succAbove k))) :
+    S.F.obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))) := by
+  rw [contrMap, contrIso]
+  simp only [Nat.succ_eq_add_one, S.F_def, Iso.trans_hom, Functor.mapIso_hom, Iso.symm_hom,
+    tensorIso_hom, Monoidal.tensorUnit_obj, tensorHom_id,
+    Category.assoc, Action.comp_hom, Action.instMonoidalCategory_tensorObj_V,
+    Action.instMonoidalCategory_tensorHom_hom, Action.instMonoidalCategory_tensorUnit_V,
+    Action.instMonoidalCategory_whiskerRight_hom, Functor.id_obj, mk_hom, ModuleCat.coe_comp,
+    Function.comp_apply, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj, Discrete.functor_obj_eq_as]
+  change (λ_ ((lift.obj S.FD).obj _)).hom.hom
+    (((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
+    (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
+    (((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
+    (((lift.obj S.FD).μIso (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)
+    ∘ Sum.inl))
+    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
+    (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
+    (((lift.obj S.FD).map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom
+    ((PiTensorProduct.tprod S.k) x)))))) = _
+  rw [lift.map_tprod]
+  change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
+    (((S.contr.app { as := c i }).hom ▷
+    ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
+    (((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
+    (((lift.obj S.FD).μIso (OverColor.mk
+    ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
+    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
+    (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
+    ((PiTensorProduct.tprod S.k) fun i_1 =>
+    (lift.discreteFunctorMapEqIso S.FD _)
+    (x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm i_1))))))) = _
+  rw [lift.map_tprod]
+  change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
+    (((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
+    (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
+    (((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
+    (((lift.obj S.FD).μIso
+    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
+    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
+    ((PiTensorProduct.tprod S.k) fun i_1 =>
+    (lift.discreteFunctorMapEqIso S.FD _)
+    ((lift.discreteFunctorMapEqIso S.FD _)
+    (x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
+    ((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm i_1)))))))) = _
+  rw [lift.μIso_inv_tprod]
+  change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
+    (((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
+    (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
+    ((TensorProduct.map (S.contrFin1Fin1 c i j h).hom.hom
+    ((lift.obj S.FD).map (mkIso _).hom).hom)
+    (((PiTensorProduct.tprod S.k) fun i_1 =>
+    (lift.discreteFunctorMapEqIso S.FD _)
+    ((lift.discreteFunctorMapEqIso S.FD _) (x
+    ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
+    ((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm
+    (Sum.inl i_1)))))) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun i_1 =>
+    (lift.discreteFunctorMapEqIso S.FD _) ((lift.discreteFunctorMapEqIso S.FD _)
+    (x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
+    ((Hom.toEquiv
+    (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm (Sum.inr i_1)))))))) = _
+  rw [TensorProduct.map_tmul]
+  rw [contrFin1Fin1_hom_hom_tprod]
+  simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V,
+    Action.instMonoidalCategory_tensorUnit_V, Fin.isValue, mk_hom, Function.comp_apply,
+    Discrete.functor_obj_eq_as, instMonoidalCategoryStruct_tensorObj_left, mkSum_homToEquiv,
+    Equiv.refl_symm, Functor.id_obj, ModuleCat.MonoidalCategory.whiskerRight_apply]
+  rw [Action.instMonoidalCategory_leftUnitor_hom_hom]
+  simp only [Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue,
+    ModuleCat.MonoidalCategory.leftUnitor_hom_apply]
+  congr 1
+  /- The contraction. -/
+  · simp only [Fin.isValue, castToField]
+    congr 2
+    · simp only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
+      Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
+      rfl
+    · simp only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
+      Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
+      change (S.FD.map (eqToHom _)).hom
+        (x (((HepLean.Fin.finExtractTwo i j)).symm ((Sum.inl (Sum.inr 0))))) = _
+      simp only [Nat.succ_eq_add_one, Fin.isValue]
+      have h1' {a b d: Fin n.succ.succ} (hbd : b =d) (h : c d = S.τ (c a)) (h' : c b = S.τ (c a)) :
+          (S.FD.map (Discrete.eqToHom (h))).hom (x d) =
+          (S.FD.map (Discrete.eqToHom h')).hom (x b) := by
+        subst hbd
+        rfl
+      refine h1' ?_ ?_ ?_
+      simp only [Nat.succ_eq_add_one, Fin.isValue, HepLean.Fin.finExtractTwo_symm_inl_inr_apply]
+      simp [h]
+  /- The tensor. -/
+  · erw [lift.map_tprod]
+    apply congrArg
+    funext d
+    simp only [mk_hom, Function.comp_apply, lift.discreteFunctorMapEqIso, Functor.mapIso_hom,
+      eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom,
+      Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
+    change (S.FD.map (eqToHom _)).hom
+        ((x ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr (d))))) = _
+    simp only [Nat.succ_eq_add_one]
+    have h1 : ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr d))
+      = (i.succAbove (j.succAbove d)) := HepLean.Fin.finExtractTwo_symm_inr_apply i j d
+    have h1' {a b : Fin n.succ.succ} (h : a = b) :
+      (S.FD.map (eqToHom (by rw [h]))).hom (x a) = x b := by
+      subst h
+      simp
+    exact h1' h1
+
+/-!
+
+## Evalutation of indices.
+
+-/
+
+/-- The isomorphism of objects in `Rep S.k S.G` given an `i` in `Fin n.succ`
+  allowing us to undertake evaluation. -/
+def evalIso {n : ℕ} (c : Fin n.succ → S.C)
+    (i : Fin n.succ) : S.F.obj (OverColor.mk c) ≅ (S.FD.obj (Discrete.mk (c i))) ⊗
+      (OverColor.lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove)) :=
+  (S.F.mapIso (OverColor.equivToIso (HepLean.Fin.finExtractOne i))).trans <|
+  (S.F.mapIso (OverColor.mkSum (c ∘ (HepLean.Fin.finExtractOne i).symm))).trans <|
+  (S.F.μIso _ _).symm.trans <|
+  tensorIso
+    ((S.F.mapIso (OverColor.mkIso (by ext x; fin_cases x; rfl))).trans
+    (OverColor.forgetLiftApp S.FD (c i))) (S.F.mapIso (OverColor.mkIso (by ext x; simp)))
+
+lemma evalIso_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ)
+    (x : (i : Fin n.succ) → S.FD.obj (Discrete.mk (c i))) :
+    (S.evalIso c i).hom.hom (PiTensorProduct.tprod S.k x) =
+    x i ⊗ₜ[S.k] (PiTensorProduct.tprod S.k (fun k => x (i.succAbove k))) := by
+  simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, F_def, evalIso,
+    Iso.trans_hom, Functor.mapIso_hom, Iso.symm_hom, tensorIso_hom, Action.comp_hom,
+    Action.instMonoidalCategory_tensorHom_hom, Functor.id_obj, mk_hom, ModuleCat.coe_comp,
+    Function.comp_apply]
+  change (((lift.obj S.FD).map (mkIso _).hom).hom ≫
+    (forgetLiftApp S.FD (c i)).hom.hom ⊗
+    ((lift.obj S.FD).map (mkIso _).hom).hom)
+    (((lift.obj S.FD).μIso
+    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inl))
+    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inr))).inv.hom
+    (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractOne i).symm)).hom).hom
+    (((lift.obj S.FD).map (equivToIso (HepLean.Fin.finExtractOne i)).hom).hom
+    ((PiTensorProduct.tprod S.k) _)))) =_
+  rw [lift.map_tprod]
+  change (((lift.obj S.FD).map (mkIso _).hom).hom ≫
+    (forgetLiftApp S.FD (c i)).hom.hom ⊗
+    ((lift.obj S.FD).map (mkIso _).hom).hom)
+    (((lift.obj S.FD).μIso
+    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inl))
+    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inr))).inv.hom
+    (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractOne i).symm)).hom).hom
+    (((PiTensorProduct.tprod S.k) _)))) =_
+  rw [lift.map_tprod]
+  change ((TensorProduct.map (((lift.obj S.FD).map (mkIso _).hom).hom ≫
+    (forgetLiftApp S.FD (c i)).hom.hom)
+    ((lift.obj S.FD).map (mkIso _).hom).hom))
+    (((lift.obj S.FD).μIso
+    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inl))
+    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inr))).inv.hom
+    ((((PiTensorProduct.tprod S.k) _)))) =_
+  rw [lift.μIso_inv_tprod]
+  rw [TensorProduct.map_tmul]
+  erw [lift.map_tprod]
+  simp only [Nat.succ_eq_add_one, CategoryStruct.comp, Functor.id_obj,
+    instMonoidalCategoryStruct_tensorObj_hom, mk_hom, Sum.elim_inl, Function.comp_apply,
+    instMonoidalCategoryStruct_tensorObj_left, mkSum_homToEquiv, Equiv.refl_symm,
+    LinearMap.coe_comp, Sum.elim_inr]
+  congr 1
+  · change (forgetLiftApp S.FD (c i)).hom.hom
+      (((lift.obj S.FD).map (mkIso _).hom).hom
+      ((PiTensorProduct.tprod S.k) _)) = _
+    rw [lift.map_tprod]
+    rw [forgetLiftApp_hom_hom_apply_eq]
+    apply congrArg
+    funext i
+    match i with
+    | (0 : Fin 1) =>
+      simp only [mk_hom, Fin.isValue, Function.comp_apply, lift.discreteFunctorMapEqIso,
+        eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv,
+        LinearEquiv.ofLinear_apply]
+      rfl
+  · apply congrArg
+    funext k
+    simp only [lift.discreteFunctorMapEqIso, Functor.mapIso_hom, eqToIso.hom, Functor.mapIso_inv,
+      eqToIso.inv, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv,
+      LinearEquiv.ofLinear_apply]
+    change (S.FD.map (eqToHom _)).hom
+      (x ((HepLean.Fin.finExtractOne i).symm ((Sum.inr k)))) = _
+    have h1' {a b : Fin n.succ} (h : a = b) :
+      (S.FD.map (eqToHom (by rw [h]))).hom (x a) = x b := by
+      subst h
+      simp
+    refine h1' ?_
+    exact HepLean.Fin.finExtractOne_symm_inr_apply i k
+
+/-- The linear map giving the coordinate of a vector with respect to the given basis.
+  Important Note: This is not a morphism in the category of representations. In general,
+  it cannot be lifted thereto. -/
+def evalLinearMap {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (S.repDim (c i))) :
+    S.FD.obj { as := c i } →ₗ[S.k] S.k where
+  toFun := fun v => (S.basis (c i)).repr v e
+  map_add' := by simp
+  map_smul' := by simp
+
+/-- The evaluation map, used to evaluate indices of tensors.
+  Important Note: The evaluation map is in general, not equivariant with respect to
+  group actions. It is a morphism in the underlying module category, not the category
+  of representations. -/
+def evalMap {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (S.repDim (c i))) :
+    (S.F.obj (OverColor.mk c)).V ⟶ (S.F.obj (OverColor.mk (c ∘ i.succAbove))).V :=
+  (S.evalIso c i).hom.hom ≫ ((Action.forgetMonoidal _ _).μIso _ _).inv
+  ≫ ModuleCat.asHom (TensorProduct.map (S.evalLinearMap i e) LinearMap.id) ≫
+  ModuleCat.asHom (TensorProduct.lid S.k _).toLinearMap
+
+lemma evalMap_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (S.repDim (c i)))
+    (x : (i : Fin n.succ) → S.FD.obj (Discrete.mk (c i))) :
+    (S.evalMap i e) (PiTensorProduct.tprod S.k x) =
+    (((S.basis (c i)).repr (x i) e) : S.k) •
+    (PiTensorProduct.tprod S.k
+    (fun k => x (i.succAbove k)) : S.F.obj (OverColor.mk (c ∘ i.succAbove))) := by
+  rw [evalMap]
+  simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V,
+    Action.forgetMonoidal_toLaxMonoidalFunctor_toFunctor, Action.forget_obj, Functor.id_obj, mk_hom,
+    Function.comp_apply, ModuleCat.coe_comp]
+  erw [evalIso_tprod]
+  change ((TensorProduct.lid S.k ↑((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove))).V))
+    (((TensorProduct.map (S.evalLinearMap i e) LinearMap.id))
+    (((Action.forgetMonoidal (ModuleCat S.k) (MonCat.of S.G)).μIso (S.FD.obj { as := c i })
+    ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove)))).inv
+    (x i ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun k => x (i.succAbove k)))) = _
+  simp only [Nat.succ_eq_add_one, Action.forgetMonoidal_toLaxMonoidalFunctor_toFunctor,
+    Action.forget_obj, Action.instMonoidalCategory_tensorObj_V, MonoidalFunctor.μIso,
+    Action.forgetMonoidal_toLaxMonoidalFunctor_μ, asIso_inv, IsIso.inv_id, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    Functor.id_obj, mk_hom, Function.comp_apply, ModuleCat.id_apply, TensorProduct.map_tmul,
+    LinearMap.id_coe, id_eq, TensorProduct.lid_tmul]
+  rfl
+
+end TensorSpecies
+
+end

HepLean/Tensors/TensorSpecies/ContractLemmas.lean

@@ -0,0 +1,140 @@
+/-
+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.TensorSpecies.UnitTensor
+/-!
+
+## Contraction of specific tensor types
+
+-/
+
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+open OverColor
+open HepLean.Fin
+open TensorProduct
+noncomputable section
+
+namespace TensorSpecies
+open TensorTree
+
+variable {S : TensorSpecies}
+
+/-- Expands the inner contraction of two 2-tensors which are
+  tprods in terms of basic categorical
+  constructions and fields of the tensor species. -/
+lemma contr_two_two_inner_tprod (c : S.C) (x : S.F.obj (OverColor.mk ![c, c]))
+    (fx : (i : (𝟭 Type).obj (OverColor.mk ![c, c]).left) →
+      CoeSort.coe (S.FD.obj { as := (OverColor.mk ![c, c]).hom i }))
+    (y : S.F.obj (OverColor.mk ![(S.τ c), (S.τ c)]))
+    (fy : (i : (𝟭 Type).obj (OverColor.mk ![S.τ c, S.τ c]).left) →
+      CoeSort.coe (S.FD.obj { as := (OverColor.mk ![S.τ c, S.τ c]).hom i }))
+    (hx : x = PiTensorProduct.tprod S.k fx)
+    (hy : y = PiTensorProduct.tprod S.k fy) :
+    {x | μ ν ⊗ y| ν ρ}ᵀ.tensor = (S.F.map (OverColor.mkIso (by
+      funext x
+      fin_cases x <;> rfl)).hom).hom ((OverColor.Discrete.pairIsoSep S.FD).hom.hom
+    (((S.FD.obj (Discrete.mk c)) ◁ (λ_ (S.FD.obj (Discrete.mk (S.τ c)))).hom).hom
+    (((S.FD.obj (Discrete.mk c)) ◁ ((S.contr.app (Discrete.mk c)) ▷
+    (S.FD.obj (Discrete.mk (S.τ c))))).hom
+    (((S.FD.obj (Discrete.mk c)) ◁ (α_ (S.FD.obj (Discrete.mk (c)))
+      (S.FD.obj (Discrete.mk (S.τ c))) (S.FD.obj (Discrete.mk (S.τ c)))).inv).hom
+    ((α_ (S.FD.obj (Discrete.mk (c))) (S.FD.obj (Discrete.mk (c)))
+      (S.FD.obj (Discrete.mk (S.τ c)) ⊗ S.FD.obj (Discrete.mk (S.τ c)))).hom.hom
+    (((OverColor.Discrete.pairIsoSep S.FD).inv.hom x ⊗ₜ
+    (OverColor.Discrete.pairIsoSep S.FD).inv.hom y))))))) := by
+  subst hx
+  subst hy
+  rw [Discrete.pairIsoSep_inv_tprod S.FD fx, Discrete.pairIsoSep_inv_tprod S.FD fy]
+  change _ = (S.F.map (OverColor.mkIso _).hom).hom ((OverColor.Discrete.pairIsoSep S.FD).hom.hom
+    ((fx (0 : Fin 2) ⊗ₜ[S.k] (λ_ (S.FD.obj { as := S.τ c }).V).hom
+      ((S.contr.app { as := c }).hom (fx (1 : Fin 2)
+      ⊗ₜ[S.k] fy (0 : Fin 2)) ⊗ₜ[S.k] fy (1 : Fin 2)))))
+  simp only [F_def, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, Monoidal.tensorUnit_obj,
+    Action.instMonoidalCategory_tensorUnit_V, Functor.comp_obj, Discrete.functor_obj_eq_as,
+    Function.comp_apply, ModuleCat.MonoidalCategory.leftUnitor_hom_apply, tmul_smul, map_smul]
+  conv_lhs =>
+    simp only [Nat.reduceAdd, Fin.isValue, contr_tensor, prod_tensor, Functor.id_obj, mk_hom,
+    Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    tensorNode_tensor, Action.instMonoidalCategory_tensorUnit_V,
+    Action.instMonoidalCategory_whiskerLeft_hom, Action.instMonoidalCategory_leftUnitor_hom_hom,
+    Monoidal.tensorUnit_obj, Action.instMonoidalCategory_whiskerRight_hom,
+    Action.instMonoidalCategory_associator_inv_hom, Action.instMonoidalCategory_associator_hom_hom,
+    F_def]
+    erw [OverColor.lift.μ_tmul_tprod S.FD]
+    rw (config := { transparency := .instances }) [OverColor.lift.map_tprod]
+    rw (config := { transparency := .instances }) [contrMap_tprod]
+  congr 1
+  /- The contraction. -/
+  · congr
+    · simp only [Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Fin.isValue,
+      Function.comp_apply, Action.FunctorCategoryEquivalence.functor_obj_obj, mk_hom,
+      equivToIso_homToEquiv, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
+      Iso.refl_hom, Action.id_hom, Iso.refl_inv, Functor.id_obj,
+      instMonoidalCategoryStruct_tensorObj_hom, LinearEquiv.ofLinear_apply]
+      rfl
+    · simp only [Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Fin.isValue,
+      Function.comp_apply, Functor.comp_obj, Discrete.functor_obj_eq_as,
+      Action.FunctorCategoryEquivalence.functor_obj_obj, Nat.reduceAdd, eqToHom_refl,
+      Discrete.functor_map_id, Action.id_hom, mk_hom, equivToIso_homToEquiv,
+      lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, Iso.refl_inv,
+      Functor.id_obj, instMonoidalCategoryStruct_tensorObj_hom, LinearEquiv.ofLinear_apply]
+      rfl
+  /- The tensor. -/
+  · rw (config := { transparency := .instances }) [Discrete.pairIsoSep_tmul,
+      OverColor.lift.map_tprod]
+    apply congrArg
+    funext k
+    match k with
+    | (0 : Fin 2) => rfl
+    | (1 : Fin 2) => rfl
+
+/-- Expands the inner contraction of two 2-tensors in terms of basic categorical
+  constructions and fields of the tensor species. -/
+lemma contr_two_two_inner (c : S.C) (x : S.F.obj (OverColor.mk ![c, c]))
+    (y : S.F.obj (OverColor.mk ![(S.τ c), (S.τ c)])) :
+    {x | μ ν ⊗ y| ν ρ}ᵀ.tensor = (S.F.map (OverColor.mkIso (by
+      funext x
+      fin_cases x <;> rfl)).hom).hom ((OverColor.Discrete.pairIsoSep S.FD).hom.hom
+    (((S.FD.obj (Discrete.mk c)) ◁ (λ_ (S.FD.obj (Discrete.mk (S.τ c)))).hom).hom
+    (((S.FD.obj (Discrete.mk c)) ◁ ((S.contr.app (Discrete.mk c)) ▷
+    (S.FD.obj (Discrete.mk (S.τ c))))).hom
+    (((S.FD.obj (Discrete.mk c)) ◁ (α_ (S.FD.obj (Discrete.mk (c)))
+      (S.FD.obj (Discrete.mk (S.τ c))) (S.FD.obj (Discrete.mk (S.τ c)))).inv).hom
+    ((α_ (S.FD.obj (Discrete.mk (c))) (S.FD.obj (Discrete.mk (c)))
+      (S.FD.obj (Discrete.mk (S.τ c)) ⊗ S.FD.obj (Discrete.mk (S.τ c)))).hom.hom
+    (((OverColor.Discrete.pairIsoSep S.FD).inv.hom x ⊗ₜ
+    (OverColor.Discrete.pairIsoSep S.FD).inv.hom y))))))) := by
+  simp only [Nat.reduceAdd, Fin.isValue, contr_tensor, prod_tensor, Functor.id_obj, mk_hom,
+    Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    tensorNode_tensor, Action.instMonoidalCategory_tensorUnit_V,
+    Action.instMonoidalCategory_whiskerLeft_hom, Action.instMonoidalCategory_leftUnitor_hom_hom,
+    Monoidal.tensorUnit_obj, Action.instMonoidalCategory_whiskerRight_hom,
+    Action.instMonoidalCategory_associator_inv_hom, Action.instMonoidalCategory_associator_hom_hom]
+  refine PiTensorProduct.induction_on' x ?_ (by
+    intro a b hx hy
+    simp only [Fin.isValue, Nat.reduceAdd, Functor.id_obj, mk_hom, add_tmul,
+      map_add, hx, hy])
+  intro rx fx
+  refine PiTensorProduct.induction_on' y ?_ (by
+      intro a b hx hy
+      simp_all only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Functor.id_obj, mk_hom,
+        PiTensorProduct.tprodCoeff_eq_smul_tprod, map_smul, map_add, tmul_add])
+  intro ry fy
+  simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, tmul_smul, LinearMapClass.map_smul]
+  apply congrArg
+  simp only [smul_tmul, tmul_smul, LinearMapClass.map_smul]
+  apply congrArg
+  simpa using contr_two_two_inner_tprod c (PiTensorProduct.tprod S.k fx) fx
+    (PiTensorProduct.tprod S.k fy) fy
+
+end TensorSpecies
+
+end

HepLean/Tensors/TensorSpecies/MetricTensor.lean

@@ -0,0 +1,128 @@
+/-
+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.TensorSpecies.UnitTensor
+import HepLean.Tensors.TensorSpecies.ContractLemmas
+import HepLean.Tensors.Tree.NodeIdentities.ProdComm
+import HepLean.Tensors.Tree.NodeIdentities.PermProd
+import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
+import HepLean.Tensors.Tree.NodeIdentities.PermContr
+/-!
+
+## Metrics in tensor trees
+
+-/
+
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+open OverColor
+open HepLean.Fin
+open TensorProduct
+noncomputable section
+
+namespace TensorSpecies
+open TensorTree
+
+/-- The metric of a tensor species in a `PiTensorProduct`. -/
+def metricTensor (S : TensorSpecies) (c : S.C) : S.F.obj (OverColor.mk ![c, c]) :=
+  (OverColor.Discrete.pairIsoSep S.FD).hom.hom ((S.metric.app (Discrete.mk c)).hom (1 : S.k))
+
+variable {S : TensorSpecies}
+
+lemma metricTensor_congr {c c' : S.C} (h : c = c') : {S.metricTensor c | μ ν}ᵀ.tensor =
+    (perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by subst h; fin_cases x <;> rfl))
+    {S.metricTensor c' | μ ν}ᵀ).tensor := by
+  subst h
+  change _ = (S.F.map (𝟙 _)).hom (S.metricTensor c)
+  simp
+
+lemma pairIsoSep_inv_metricTensor (c : S.C) :
+    (Discrete.pairIsoSep S.FD).inv.hom (S.metricTensor c) =
+    (S.metric.app (Discrete.mk c)).hom (1 : S.k) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, Nat.succ_eq_add_one, Nat.reduceAdd,
+    metricTensor, Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V]
+  erw [Discrete.rep_iso_inv_hom_apply]
+
+/-- Contraction of a metric tensor with a metric tensor gives the unit.
+  Like `S.contr_metric` but with the braiding appearing on the side of the unit. -/
+lemma contr_metric_braid_unit (c : S.C) : (((S.FD.obj (Discrete.mk c)) ◁
+    (λ_ (S.FD.obj (Discrete.mk (S.τ c)))).hom).hom
+    (((S.FD.obj (Discrete.mk c)) ◁ ((S.contr.app (Discrete.mk c)) ▷
+    (S.FD.obj (Discrete.mk (S.τ c))))).hom
+    (((S.FD.obj (Discrete.mk c)) ◁ (α_ (S.FD.obj (Discrete.mk (c)))
+      (S.FD.obj (Discrete.mk (S.τ c))) (S.FD.obj (Discrete.mk (S.τ c)))).inv).hom
+    ((α_ (S.FD.obj (Discrete.mk (c))) (S.FD.obj (Discrete.mk (c)))
+      (S.FD.obj (Discrete.mk (S.τ c)) ⊗ S.FD.obj (Discrete.mk (S.τ c)))).hom.hom
+    (((OverColor.Discrete.pairIsoSep S.FD).inv.hom (S.metricTensor c) ⊗ₜ
+    (OverColor.Discrete.pairIsoSep S.FD).inv.hom (S.metricTensor (S.τ c)))))))) =
+    (β_ (S.FD.obj (Discrete.mk (S.τ c))) (S.FD.obj (Discrete.mk c))).hom.hom
+      ((S.unit.app (Discrete.mk c)).hom (1 : S.k)) := by
+  apply (β_ _ _).toLinearEquiv.toEquiv.injective
+  rw [pairIsoSep_inv_metricTensor, pairIsoSep_inv_metricTensor]
+  erw [S.contr_metric c]
+  change _ = (β_ (S.FD.obj { as := S.τ c }) (S.FD.obj { as := c })).inv.hom
+    ((β_ (S.FD.obj { as := S.τ c }) (S.FD.obj { as := c })).hom.hom _)
+  rw [Discrete.rep_iso_inv_hom_apply]
+
+lemma metricTensor_contr_dual_metricTensor_perm_cond (c : S.C) : ∀ (x : Fin (Nat.succ 0).succ),
+    ((Sum.elim ![c, c] ![S.τ c, S.τ c] ∘ ⇑finSumFinEquiv.symm) ∘
+    Fin.succAbove 1 ∘ Fin.succAbove 1) x =
+    (![S.τ c, c] ∘ ⇑(finMapToEquiv ![1, 0] ![1, 0]).symm) x := by
+  intro x
+  fin_cases x
+  · rfl
+  · rfl
+
+/-- The contraction of a metric tensor with its dual via the inner indices gives the unit. -/
+lemma metricTensor_contr_dual_metricTensor_eq_unit (c : S.C) :
+    {S.metricTensor c | μ ν ⊗ S.metricTensor (S.τ c) | ν ρ}ᵀ.tensor = ({S.unitTensor c | μ ρ}ᵀ |>
+    perm (OverColor.equivToHomEq (finMapToEquiv ![1, 0] ![1, 0])
+      (metricTensor_contr_dual_metricTensor_perm_cond c))).tensor := by
+  rw [contr_two_two_inner, contr_metric_braid_unit, Discrete.pairIsoSep_β]
+  change (S.F.map _ ≫ S.F.map _).hom _ = _
+  rw [← S.F.map_comp]
+  rfl
+
+/-- The contraction of a metric tensor with its dual via the outer indices gives the unit. -/
+lemma metricTensor_contr_dual_metricTensor_outer_eq_unit (c : S.C) :
+    {S.metricTensor c | ν μ ⊗ S.metricTensor (S.τ c) | ρ ν}ᵀ.tensor = ({S.unitTensor c | μ ρ}ᵀ |>
+    perm (OverColor.equivToHomEq
+      (finMapToEquiv ![1, 0] ![1, 0]) (fun x => by fin_cases x <;> rfl))).tensor := by
+  conv_lhs =>
+    rw [contr_tensor_eq <| prod_tensor_eq_fst <| metricTensor_congr (S.τ_involution c).symm]
+    rw [contr_tensor_eq <| prod_comm _ _ _ _]
+    rw [perm_contr_congr 2 1 (by rfl) (by rfl)]
+    rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_right _ _ _ _]
+    rw [perm_tensor_eq <| perm_contr_congr 2 1 (by rfl) (by rfl)]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_swap _ _]
+    rw [perm_perm]
+    erw [perm_tensor_eq <| metricTensor_contr_dual_metricTensor_eq_unit _]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| dual_unitTensor_eq_perm _]
+    rw [perm_perm]
+  apply perm_congr _ rfl
+  apply OverColor.Hom.fin_ext
+  intro i
+  simp only [Functor.id_obj, mk_hom, Function.comp_apply, Equiv.refl_symm, Equiv.coe_refl, id_eq,
+    Fin.zero_eta, Matrix.cons_val_zero, List.pmap.eq_1, ContrPair.contrSwapHom,
+    extractOne_homToEquiv, Category.assoc, Hom.hom_comp, Over.comp_left, equivToHomEq_hom_left,
+    Equiv.toFun_as_coe, types_comp_apply, finMapToEquiv_apply, mkIso_hom_hom_left_apply]
+  rw [extractTwo_hom_left_apply]
+  simp only [mk_left, braidPerm_toEquiv, Equiv.symm_trans_apply, Equiv.symm_symm,
+    Equiv.sumComm_symm, Equiv.sumComm_apply, finExtractOnePerm_symm_apply, Equiv.trans_apply,
+    Equiv.symm_apply_apply, Sum.swap_swap, Equiv.apply_symm_apply, finExtractOne_symm_inr_apply,
+    Fin.zero_succAbove, List.pmap.eq_2, Fin.mk_one, List.pmap.eq_1, Matrix.cons_val_one,
+    Matrix.head_cons, extractTwo_hom_left_apply, permProdRight_toEquiv, equivToHomEq_toEquiv,
+    Equiv.sumCongr_refl, Equiv.refl_trans, Equiv.symm_trans_self, Equiv.refl_symm, Equiv.refl_apply,
+    predAboveI_succAbove, finExtractOnePerm_apply]
+  fin_cases i
+  · decide
+  · decide
+
+end TensorSpecies
+
+end

HepLean/Tensors/TensorSpecies/RepIso.lean

@@ -0,0 +1,45 @@
+/-
+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.TensorSpecies.Basic
+/-!
+
+# Isomorphism between rep of color `c` and rep of dual color.
+
+-/
+
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+
+noncomputable section
+
+namespace TensorSpecies
+variable (S : TensorSpecies)
+
+/-- The morphism from `S.FD.obj (Discrete.mk c)` to `S.FD.obj (Discrete.mk (S.τ c))`
+  defined by contracting with the metric. -/
+def toDualRep (c : S.C) : S.FD.obj (Discrete.mk c) ⟶ S.FD.obj (Discrete.mk (S.τ c)) :=
+  (ρ_ (S.FD.obj (Discrete.mk c))).inv
+  ≫ (S.FD.obj { as := c } ◁ (S.metric.app (Discrete.mk (S.τ c))))
+  ≫ (α_ (S.FD.obj (Discrete.mk c)) (S.FD.obj (Discrete.mk (S.τ c)))
+    (S.FD.obj (Discrete.mk (S.τ c)))).inv
+  ≫ (S.contr.app (Discrete.mk c) ▷ S.FD.obj { as := S.τ c })
+  ≫ (λ_ (S.FD.obj (Discrete.mk (S.τ c)))).hom
+
+/-- The `toDualRep` for equal colors is the same, up-to conjugation by a trivial equivalence. -/
+lemma toDualRep_congr {c c' : S.C} (h : c = c') : S.toDualRep c = S.FD.map (Discrete.eqToHom h) ≫
+    S.toDualRep c' ≫ S.FD.map (Discrete.eqToHom (congrArg S.τ h.symm)) := by
+  subst h
+  simp only [eqToHom_refl, Discrete.functor_map_id, Category.comp_id, Category.id_comp]
+
+/-- The morphism from `S.FD.obj (Discrete.mk (S.τ c))` to `S.FD.obj (Discrete.mk c)`
+  defined by contracting with the metric. -/
+def fromDualRep (c : S.C) : S.FD.obj (Discrete.mk (S.τ c)) ⟶ S.FD.obj (Discrete.mk c) :=
+  S.toDualRep (S.τ c) ≫ S.FD.map (Discrete.eqToHom (S.τ_involution c))
+
+end TensorSpecies
+
+end

HepLean/Tensors/TensorSpecies/UnitTensor.lean

@@ -0,0 +1,110 @@
+/-
+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.Elab
+import HepLean.Tensors.Tree.NodeIdentities.Basic
+import HepLean.Tensors.Tree.NodeIdentities.Congr
+/-!
+
+## Units as tensors
+
+-/
+
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+open OverColor
+open HepLean.Fin
+open TensorProduct
+noncomputable section
+
+namespace TensorSpecies
+
+/-- The unit of a tensor species in a `PiTensorProduct`. -/
+def unitTensor (S : TensorSpecies) (c : S.C) : S.F.obj (OverColor.mk ![S.τ c, c]) :=
+  (OverColor.Discrete.pairIsoSep S.FD).hom.hom ((S.unit.app (Discrete.mk c)).hom (1 : S.k))
+
+variable {S : TensorSpecies}
+open TensorTree
+
+/-- The relation between two units of colors which are equal. -/
+lemma unitTensor_congr {c c' : S.C} (h : c = c') : {S.unitTensor c | μ ν}ᵀ.tensor =
+    (perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by subst h; fin_cases x <;> rfl))
+    {S.unitTensor c' | μ ν}ᵀ).tensor := by
+  subst h
+  change _ = (S.F.map (𝟙 _)).hom (S.unitTensor c)
+  simp
+
+lemma unitTensor_eq_dual_perm_eq (c : S.C) : ∀ (x : Fin (Nat.succ 0).succ),
+    ![S.τ c, c] x = (![S.τ (S.τ c), S.τ c] ∘ ⇑(finMapToEquiv ![1, 0] ![1, 0]).symm) x := fun x => by
+  fin_cases x
+  · rfl
+  · exact (S.τ_involution c).symm
+
+/-- The unit tensor is equal to a permutation of indices of the dual tensor. -/
+lemma unitTensor_eq_dual_perm (c : S.C) : {S.unitTensor c | μ ν}ᵀ.tensor =
+    (perm (OverColor.equivToHomEq (finMapToEquiv ![1,0] ![1, 0]) (unitTensor_eq_dual_perm_eq c))
+    {S.unitTensor (S.τ c) | ν μ }ᵀ).tensor := by
+  simp [unitTensor, tensorNode_tensor, perm_tensor]
+  have h1 := S.unit_symm c
+  erw [h1]
+  have hg : (Discrete.pairIsoSep S.FD).hom.hom ∘ₗ (S.FD.obj { as := S.τ c } ◁
+      S.FD.map (Discrete.eqToHom (S.τ_involution c))).hom ∘ₗ
+      (β_ (S.FD.obj { as := S.τ (S.τ c) }) (S.FD.obj { as := S.τ c })).hom.hom =
+      (S.F.map (equivToHomEq (finMapToEquiv ![1, 0] ![1, 0]) (unitTensor_eq_dual_perm_eq c))).hom
+      ∘ₗ (Discrete.pairIsoSep S.FD).hom.hom := by
+    apply TensorProduct.ext'
+    intro x y
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Equivalence.symm_inverse,
+      Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+      Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_whiskerLeft_hom,
+      LinearMap.coe_comp, Function.comp_apply, Fin.isValue]
+    change (Discrete.pairIsoSep S.FD).hom.hom
+      (((y ⊗ₜ[S.k] ((S.FD.map (Discrete.eqToHom _)).hom x)))) =
+      ((S.F.map (equivToHomEq (finMapToEquiv ![1, 0] ![1, 0]) _)).hom ∘ₗ
+      (Discrete.pairIsoSep S.FD).hom.hom) (x ⊗ₜ[S.k] y)
+    rw [Discrete.pairIsoSep_tmul]
+    conv_rhs =>
+      simp [Discrete.pairIsoSep_tmul]
+    change _ =
+      (S.F.map (equivToHomEq (finMapToEquiv ![1, 0] ![1, 0]) _)).hom
+      ((Discrete.pairIsoSep S.FD).hom.hom (x ⊗ₜ[S.k] y))
+    rw [Discrete.pairIsoSep_tmul]
+    simp only [F_def, Nat.succ_eq_add_one, Nat.reduceAdd, mk_hom, Functor.id_obj, Fin.isValue]
+    erw [OverColor.lift.map_tprod]
+    apply congrArg
+    funext i
+    fin_cases i
+    · simp only [Fin.zero_eta, Fin.isValue, Matrix.cons_val_zero, Fin.cases_zero, mk_hom,
+      Nat.succ_eq_add_one, Nat.reduceAdd, lift.discreteFunctorMapEqIso, eqToIso_refl,
+      Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
+      rfl
+    · simp only [Fin.mk_one, Fin.isValue, Matrix.cons_val_one, Matrix.head_cons, mk_hom,
+      Nat.succ_eq_add_one, Nat.reduceAdd, lift.discreteFunctorMapEqIso, Functor.mapIso_hom,
+      eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, LinearEquiv.ofLinear_apply]
+      rfl
+  exact congrFun (congrArg (fun f => f.toFun) hg) _
+
+lemma dual_unitTensor_eq_perm_eq (c : S.C) : ∀ (x : Fin (Nat.succ 0).succ),
+    ![S.τ (S.τ c), S.τ c] x = (![S.τ c, c] ∘ ⇑(finMapToEquiv ![1, 0] ![1, 0]).symm) x := fun x => by
+  fin_cases x
+  · exact (S.τ_involution c)
+  · rfl
+
+lemma dual_unitTensor_eq_perm (c : S.C) : {S.unitTensor (S.τ c) | ν μ}ᵀ.tensor =
+    (perm (OverColor.equivToHomEq (finMapToEquiv ![1, 0] ![1, 0]) (dual_unitTensor_eq_perm_eq c))
+    {S.unitTensor c | μ ν}ᵀ).tensor := by
+  rw [unitTensor_eq_dual_perm]
+  conv =>
+    lhs
+    rw [perm_tensor_eq <| unitTensor_congr (S.τ_involution c)]
+    rw [perm_perm]
+  refine perm_congr ?_ rfl
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue]
+  rfl
+
+end TensorSpecies
+
+end

HepLean/Tensors/Tree/Basic.lean

@@ -3,23 +3,10 @@ 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.Iso
-import HepLean.Tensors.OverColor.Discrete
-import HepLean.Tensors.OverColor.Lift
-import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
+import HepLean.Tensors.TensorSpecies.Basic
 /-!
 
-# Tensor species and trees
-
-## Tensor species
-
-- A tensor species is a structure including all of the ingredients needed to define a type of
-  tensor.
-- Examples of tensor species will include real Lorentz tensors, complex Lorentz tensors, and
-  Einstien tensors.
-- Tensor species are built upon symmetric monoidal categories.
-
-## Trees
+# Tensor trees
 
 - Tensor trees provide an abstract way to represent tensor expressions.
 - Their nodes are either tensors or operations between tensors.
@@ -37,523 +24,8 @@ open IndexNotation
 open CategoryTheory
 open MonoidalCategory
 
-/-- The structure of a type of tensors e.g. Lorentz tensors, ordinary tensors
-  (vectors and matrices), complex Lorentz tensors. -/
-structure TensorSpecies where
-  /-- The commutative ring over which we want to consider the tensors to live in,
-    usually `ℝ` or `ℂ`. -/
-  k : Type
-  /-- An instance of `k` as a commutative ring. -/
-  k_commRing : CommRing k
-  /-- The symmetry group acting on these tensor e.g. the Lorentz group or SL(2,ℂ). -/
-  G : Type
-  /-- An instance of `G` as a group. -/
-  G_group : Group G
-  /-- The colors of indices e.g. up or down. -/
-  C : Type
-  /-- A functor from `C` to `Rep k G` giving our building block representations.
-    Equivalently a function `C → Re k G`. -/
-  FD : Discrete C ⥤ Rep k G
-  /-- A specification of the dimension of each color in C. This will be used for explicit
-    evaluation of tensors. -/
-  repDim : C → ℕ
-  /-- repDim is not zero for any color. This allows casting of `ℕ` to `Fin (S.repDim c)`. -/
-  repDim_neZero (c : C) : NeZero (repDim c)
-  /-- A basis for each Module, determined by the evaluation map. -/
-  basis : (c : C) → Basis (Fin (repDim c)) k (FD.obj (Discrete.mk c)).V
-  /-- A map from `C` to `C`. An involution. -/
-  τ : C → C
-  /-- The condition that `τ` is an involution. -/
-  τ_involution : Function.Involutive τ
-  /-- The natural transformation describing contraction. -/
-  contr : OverColor.Discrete.pairτ FD τ ⟶ 𝟙_ (Discrete C ⥤ Rep k G)
-  /-- Contraction is symmetric with respect to duals. -/
-  contr_tmul_symm (c : C) (x : FD.obj (Discrete.mk c))
-      (y : FD.obj (Discrete.mk (τ c))) :
-    (contr.app (Discrete.mk c)).hom (x ⊗ₜ[k] y) = (contr.app (Discrete.mk (τ c))).hom
-    (y ⊗ₜ (FD.map (Discrete.eqToHom (τ_involution c).symm)).hom x)
-  /-- The natural transformation describing the unit. -/
-  unit : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.τPair FD τ
-  /-- The unit is symmetric. -/
-  unit_symm (c : C) :
-    ((unit.app (Discrete.mk c)).hom (1 : k)) =
-    ((FD.obj (Discrete.mk (τ (c)))) ◁
-      (FD.map (Discrete.eqToHom (τ_involution c)))).hom
-    ((β_ (FD.obj (Discrete.mk (τ (τ c)))) (FD.obj (Discrete.mk (τ (c))))).hom.hom
-    ((unit.app (Discrete.mk (τ c))).hom (1 : k)))
-  /-- Contraction with unit leaves invariant. -/
-  contr_unit (c : C) (x : FD.obj (Discrete.mk (c))) :
-    (λ_ (FD.obj (Discrete.mk (c)))).hom.hom
-    (((contr.app (Discrete.mk c)) ▷ (FD.obj (Discrete.mk (c)))).hom
-    ((α_ _ _ (FD.obj (Discrete.mk (c)))).inv.hom
-    (x ⊗ₜ[k] (unit.app (Discrete.mk c)).hom (1 : k)))) = x
-  /-- The natural transformation describing the metric. -/
-  metric : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.pair FD
-  /-- On contracting metrics we get back the unit. -/
-  contr_metric (c : C) :
-    (β_ (FD.obj (Discrete.mk c)) (FD.obj (Discrete.mk (τ c)))).hom.hom
-    (((FD.obj (Discrete.mk c)) ◁ (λ_ (FD.obj (Discrete.mk (τ c)))).hom).hom
-    (((FD.obj (Discrete.mk c)) ◁ ((contr.app (Discrete.mk c)) ▷
-    (FD.obj (Discrete.mk (τ c))))).hom
-    (((FD.obj (Discrete.mk c)) ◁ (α_ (FD.obj (Discrete.mk (c)))
-      (FD.obj (Discrete.mk (τ c))) (FD.obj (Discrete.mk (τ c)))).inv).hom
-    ((α_ (FD.obj (Discrete.mk (c))) (FD.obj (Discrete.mk (c)))
-      (FD.obj (Discrete.mk (τ c)) ⊗ FD.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
 
-namespace TensorSpecies
-open OverColor
-
-variable (S : TensorSpecies)
-
-/-- The field `k` of a TensorSpecies has the instance of a commuative ring. -/
-instance : CommRing S.k := S.k_commRing
-
-/-- The field `G` of a TensorSpecies has the instance of a group. -/
-instance : Group S.G := S.G_group
-
-/-- The field `repDim` of a TensorSpecies is non-zero for all colors. -/
-instance (c : S.C) : NeZero (S.repDim c) := S.repDim_neZero c
-
-/-- The lift of the functor `S.F` to a monoidal functor. -/
-def F : BraidedFunctor (OverColor S.C) (Rep S.k S.G) := (OverColor.lift).obj S.FD
-
-/- The definition of `F` as a lemma. -/
-lemma F_def : F S = (OverColor.lift).obj S.FD := rfl
-
-lemma perm_contr_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ → S.C}
-    {i : Fin n.succ.succ} {j : Fin n.succ}
-    (h : c1 (i.succAbove j) = S.τ (c1 i)) (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
-    c (Fin.succAbove ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)) =
-    S.τ (c ((Hom.toEquiv σ).symm i)) := by
-  have h1 := Hom.toEquiv_comp_apply σ
-  simp only [Nat.succ_eq_add_one, Functor.const_obj_obj, mk_hom] at h1
-  rw [h1, h1]
-  simp only [Nat.succ_eq_add_one, extractOne_homToEquiv, Equiv.apply_symm_apply]
-  rw [← h]
-  congr
-  simp only [Nat.succ_eq_add_one, HepLean.Fin.finExtractOnePerm, HepLean.Fin.finExtractOnPermHom,
-    HepLean.Fin.finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk]
-  erw [Equiv.apply_symm_apply]
-  rw [HepLean.Fin.succsAbove_predAboveI]
-  erw [Equiv.apply_symm_apply]
-  simp only [Nat.succ_eq_add_one, ne_eq]
-  erw [Equiv.apply_eq_iff_eq]
-  exact (Fin.succAbove_ne i j).symm
-
-/-- The isomorphism between the image of a map `Fin 1 ⊕ Fin 1 → S.C` contructed by `finExtractTwo`
-  under `S.F.obj`, and an object in the image of `OverColor.Discrete.pairτ S.FD`. -/
-def contrFin1Fin1 {n : ℕ} (c : Fin n.succ.succ → S.C)
-    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) :
-    S.F.obj (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) ≅
-    (OverColor.Discrete.pairτ S.FD S.τ).obj { as := c i } := by
-  apply (S.F.mapIso
-    (OverColor.mkSum (((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)))).trans
-  apply (S.F.μIso _ _).symm.trans
-  apply tensorIso ?_ ?_
-  · symm
-    apply (OverColor.forgetLiftApp S.FD (c i)).symm.trans
-    apply S.F.mapIso
-    apply OverColor.mkIso
-    funext x
-    fin_cases x
-    rfl
-  · symm
-    apply (OverColor.forgetLiftApp S.FD (S.τ (c i))).symm.trans
-    apply S.F.mapIso
-    apply OverColor.mkIso
-    funext x
-    fin_cases x
-    simp [h]
-
-lemma contrFin1Fin1_inv_tmul {n : ℕ} (c : Fin n.succ.succ → S.C)
-    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i))
-    (x : S.FD.obj { as := c i })
-    (y : S.FD.obj { as := S.τ (c i) }) :
-    (S.contrFin1Fin1 c i j h).inv.hom (x ⊗ₜ[S.k] y) =
-    PiTensorProduct.tprod S.k (fun k =>
-    match k with | Sum.inl 0 => x | Sum.inr 0 => (S.FD.map
-    (eqToHom (by simp [h]))).hom y) := by
-  simp only [Nat.succ_eq_add_one, contrFin1Fin1, Functor.comp_obj, Discrete.functor_obj_eq_as,
-    Function.comp_apply, Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_inv, tensorIso_inv,
-    Iso.symm_inv, Functor.mapIso_hom, tensor_comp, MonoidalFunctor.μIso_hom, Category.assoc,
-    LaxMonoidalFunctor.μ_natural, Functor.mapIso_inv, Action.comp_hom,
-    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorHom_hom,
-    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
-    Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Functor.id_obj, mk_hom,
-    Fin.isValue]
-  change (S.F.map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
-    ((S.F.map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
-      ((S.F.μ (OverColor.mk fun _ => c i) (OverColor.mk fun _ => S.τ (c i))).hom
-        ((((OverColor.forgetLiftApp S.FD (c i)).inv.hom x) ⊗ₜ[S.k]
-        ((OverColor.forgetLiftApp S.FD (S.τ (c i))).inv.hom y))))) = _
-  simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
-    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
-    forgetLiftApp, Action.mkIso_inv_hom, LinearEquiv.toModuleIso_inv, Fin.isValue]
-  erw [OverColor.forgetLiftAppV_symm_apply,
-    OverColor.forgetLiftAppV_symm_apply S.FD (S.τ (c i))]
-  change ((OverColor.lift.obj S.FD).map (OverColor.mkSum
-    ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
-    (((OverColor.lift.obj S.FD).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
-    (((OverColor.lift.obj S.FD).μ (OverColor.mk fun _ => c i)
-    (OverColor.mk fun _ => S.τ (c i))).hom
-    (((PiTensorProduct.tprod S.k) fun _ => x) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun _ => y))) = _
-  rw [OverColor.lift.obj_μ_tprod_tmul S.FD]
-  change ((OverColor.lift.obj S.FD).map
-    (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
-    (((OverColor.lift.obj S.FD).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
-    ((PiTensorProduct.tprod S.k) _)) = _
-  rw [OverColor.lift.map_tprod S.FD]
-  change ((OverColor.lift.obj S.FD).map
-    (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
-    ((PiTensorProduct.tprod S.k _)) = _
-  rw [OverColor.lift.map_tprod S.FD]
-  apply congrArg
-  funext r
-  match r with
-  | Sum.inl 0 =>
-    simp only [Nat.succ_eq_add_one, mk_hom, Fin.isValue, Function.comp_apply,
-      instMonoidalCategoryStruct_tensorObj_left, mkSum_inv_homToEquiv, Equiv.refl_symm,
-      instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, lift.discreteSumEquiv, Sum.elim_inl,
-      Sum.elim_inr, HepLean.PiTensorProduct.elimPureTensor]
-    simp only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
-      Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
-    rfl
-  | Sum.inr 0 =>
-    simp only [Nat.succ_eq_add_one, mk_hom, Fin.isValue, Function.comp_apply,
-      instMonoidalCategoryStruct_tensorObj_left, mkSum_inv_homToEquiv, Equiv.refl_symm,
-      instMonoidalCategoryStruct_tensorObj_hom, lift.discreteFunctorMapEqIso, eqToIso_refl,
-      Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv, Functor.mapIso_hom,
-      eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, Functor.id_obj, lift.discreteSumEquiv,
-      Sum.elim_inl, Sum.elim_inr, HepLean.PiTensorProduct.elimPureTensor,
-      LinearEquiv.ofLinear_apply]
-    rfl
-
-lemma contrFin1Fin1_hom_hom_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
-    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i))
-    (x : (k : Fin 1 ⊕ Fin 1) → (S.FD.obj
-      { as := (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).hom k })) :
-    (S.contrFin1Fin1 c i j h).hom.hom (PiTensorProduct.tprod S.k x) =
-    x (Sum.inl 0) ⊗ₜ[S.k] ((S.FD.map (eqToHom (by simp [h]))).hom (x (Sum.inr 0))) := by
-  change ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).hom _ = _
-  trans ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).toLinearEquiv
-    (PiTensorProduct.tprod S.k x)
-  · rfl
-  erw [← LinearEquiv.eq_symm_apply]
-  erw [contrFin1Fin1_inv_tmul]
-  congr
-  funext i
-  match i with
-  | Sum.inl 0 =>
-    rfl
-  | Sum.inr 0 =>
-    simp only [Nat.succ_eq_add_one, Fin.isValue, mk_hom, Function.comp_apply,
-      Discrete.functor_obj_eq_as]
-    change _ = ((S.FD.map (eqToHom _)) ≫ (S.FD.map (eqToHom _))).hom (x (Sum.inr 0))
-    rw [← Functor.map_comp]
-    simp
-  exact h
-
-/-- The isomorphism of objects in `Rep S.k S.G` given an `i` in `Fin n.succ.succ` and
-  a `j` in `Fin n.succ` allowing us to undertake contraction. -/
-def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C)
-    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) :
-    S.F.obj (OverColor.mk c) ≅ ((OverColor.Discrete.pairτ S.FD S.τ).obj
-      (Discrete.mk (c i))) ⊗
-      (OverColor.lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
-  (S.F.mapIso (OverColor.equivToIso (HepLean.Fin.finExtractTwo i j))).trans <|
-  (S.F.mapIso (OverColor.mkSum (c ∘ (HepLean.Fin.finExtractTwo i j).symm))).trans <|
-  (S.F.μIso _ _).symm.trans <| by
-  refine tensorIso (S.contrFin1Fin1 c i j h) (S.F.mapIso (OverColor.mkIso (by ext x; simp)))
-
-lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C}
-    {i : Fin n.succ.succ} {j : Fin n.succ} {h : c1 (i.succAbove j) = S.τ (c1 i)} :
-    (S.contrIso c1 i j h).hom.hom =
-    (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom ≫
-    (S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom ≫
-    (S.F.μIso (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
-    (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom ≫
-    ((S.contrFin1Fin1 c1 i j h).hom.hom ⊗
-    (S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom) := by
-  rfl
-
-/-- `contrMap` is a function that takes a natural number `n`, a function `c` from
-`Fin n.succ.succ` to `S.C`, an index `i` of type `Fin n.succ.succ`, an index `j` of type
-`Fin n.succ`, and a proof `h` that `c (i.succAbove j) = S.τ (c i)`. It returns a morphism
-corresponding to the contraction of the `i`th index with the `i.succAbove j` index.
---/
-def contrMap {n : ℕ} (c : Fin n.succ.succ → S.C)
-    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) :
-    S.F.obj (OverColor.mk c) ⟶
-    S.F.obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
-  (S.contrIso c i j h).hom ≫
-  (tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫
-  (MonoidalCategory.leftUnitor _).hom
-
-/-- Casts an element of the monoidal unit of `Rep S.k S.G` to the field `S.k`. -/
-def castToField (v : (↑((𝟙_ (Discrete S.C ⥤ Rep S.k S.G)).obj { as := c }).V)) : S.k := v
-
-/-- Casts an element of `(S.F.obj (OverColor.mk c)).V` for `c` a map from `Fin 0` to an
-  element of the field. -/
-def castFin0ToField {c : Fin 0 → S.C} : (S.F.obj (OverColor.mk c)).V →ₗ[S.k] S.k :=
-  (PiTensorProduct.isEmptyEquiv (Fin 0)).toLinearMap
-
-lemma castFin0ToField_tprod {c : Fin 0 → S.C}
-    (x : (i : Fin 0) → S.FD.obj (Discrete.mk (c i))) :
-    castFin0ToField S (PiTensorProduct.tprod S.k x) = 1 := by
-  simp only [castFin0ToField, mk_hom, Functor.id_obj, LinearEquiv.coe_coe]
-  erw [PiTensorProduct.isEmptyEquiv_apply_tprod]
-
-lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
-    (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i))
-    (x : (i : Fin n.succ.succ) → S.FD.obj (Discrete.mk (c i))) :
-    (S.contrMap c i j h).hom (PiTensorProduct.tprod S.k x) =
-    (S.castToField ((S.contr.app (Discrete.mk (c i))).hom ((x i) ⊗ₜ[S.k]
-    (S.FD.map (Discrete.eqToHom h)).hom (x (i.succAbove j)))) : S.k)
-    • (PiTensorProduct.tprod S.k (fun k => x (i.succAbove (j.succAbove k))) :
-    S.F.obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))) := by
-  rw [contrMap, contrIso]
-  simp only [Nat.succ_eq_add_one, S.F_def, Iso.trans_hom, Functor.mapIso_hom, Iso.symm_hom,
-    tensorIso_hom, Monoidal.tensorUnit_obj, tensorHom_id,
-    Category.assoc, Action.comp_hom, Action.instMonoidalCategory_tensorObj_V,
-    Action.instMonoidalCategory_tensorHom_hom, Action.instMonoidalCategory_tensorUnit_V,
-    Action.instMonoidalCategory_whiskerRight_hom, Functor.id_obj, mk_hom, ModuleCat.coe_comp,
-    Function.comp_apply, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
-    Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj, Discrete.functor_obj_eq_as]
-  change (λ_ ((lift.obj S.FD).obj _)).hom.hom
-    (((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
-    (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
-    (((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
-    (((lift.obj S.FD).μIso (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)
-    ∘ Sum.inl))
-    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
-    (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
-    (((lift.obj S.FD).map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom
-    ((PiTensorProduct.tprod S.k) x)))))) = _
-  rw [lift.map_tprod]
-  change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
-    (((S.contr.app { as := c i }).hom ▷
-    ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
-    (((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
-    (((lift.obj S.FD).μIso (OverColor.mk
-    ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
-    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
-    (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
-    ((PiTensorProduct.tprod S.k) fun i_1 =>
-    (lift.discreteFunctorMapEqIso S.FD _)
-    (x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm i_1))))))) = _
-  rw [lift.map_tprod]
-  change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
-    (((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
-    (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
-    (((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
-    (((lift.obj S.FD).μIso
-    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
-    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
-    ((PiTensorProduct.tprod S.k) fun i_1 =>
-    (lift.discreteFunctorMapEqIso S.FD _)
-    ((lift.discreteFunctorMapEqIso S.FD _)
-    (x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
-    ((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm i_1)))))))) = _
-  rw [lift.μIso_inv_tprod]
-  change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
-    (((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
-    (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
-    ((TensorProduct.map (S.contrFin1Fin1 c i j h).hom.hom
-    ((lift.obj S.FD).map (mkIso _).hom).hom)
-    (((PiTensorProduct.tprod S.k) fun i_1 =>
-    (lift.discreteFunctorMapEqIso S.FD _)
-    ((lift.discreteFunctorMapEqIso S.FD _) (x
-    ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
-    ((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm
-    (Sum.inl i_1)))))) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun i_1 =>
-    (lift.discreteFunctorMapEqIso S.FD _) ((lift.discreteFunctorMapEqIso S.FD _)
-    (x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
-    ((Hom.toEquiv
-    (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm (Sum.inr i_1)))))))) = _
-  rw [TensorProduct.map_tmul]
-  rw [contrFin1Fin1_hom_hom_tprod]
-  simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V,
-    Action.instMonoidalCategory_tensorUnit_V, Fin.isValue, mk_hom, Function.comp_apply,
-    Discrete.functor_obj_eq_as, instMonoidalCategoryStruct_tensorObj_left, mkSum_homToEquiv,
-    Equiv.refl_symm, Functor.id_obj, ModuleCat.MonoidalCategory.whiskerRight_apply]
-  rw [Action.instMonoidalCategory_leftUnitor_hom_hom]
-  simp only [Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue,
-    ModuleCat.MonoidalCategory.leftUnitor_hom_apply]
-  congr 1
-  /- The contraction. -/
-  · simp only [Fin.isValue, castToField]
-    congr 2
-    · simp only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
-      Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
-      rfl
-    · simp only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
-      Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
-      change (S.FD.map (eqToHom _)).hom
-        (x (((HepLean.Fin.finExtractTwo i j)).symm ((Sum.inl (Sum.inr 0))))) = _
-      simp only [Nat.succ_eq_add_one, Fin.isValue]
-      have h1' {a b d: Fin n.succ.succ} (hbd : b =d) (h : c d = S.τ (c a)) (h' : c b = S.τ (c a)) :
-          (S.FD.map (Discrete.eqToHom (h))).hom (x d) =
-          (S.FD.map (Discrete.eqToHom h')).hom (x b) := by
-        subst hbd
-        rfl
-      refine h1' ?_ ?_ ?_
-      simp only [Nat.succ_eq_add_one, Fin.isValue, HepLean.Fin.finExtractTwo_symm_inl_inr_apply]
-      simp [h]
-  /- The tensor. -/
-  · erw [lift.map_tprod]
-    apply congrArg
-    funext d
-    simp only [mk_hom, Function.comp_apply, lift.discreteFunctorMapEqIso, Functor.mapIso_hom,
-      eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom,
-      Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
-    change (S.FD.map (eqToHom _)).hom
-        ((x ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr (d))))) = _
-    simp only [Nat.succ_eq_add_one]
-    have h1 : ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr d))
-      = (i.succAbove (j.succAbove d)) := HepLean.Fin.finExtractTwo_symm_inr_apply i j d
-    have h1' {a b : Fin n.succ.succ} (h : a = b) :
-      (S.FD.map (eqToHom (by rw [h]))).hom (x a) = x b := by
-      subst h
-      simp
-    exact h1' h1
-
-/-!
-
-## Evalutation of indices.
-
--/
-
-/-- The isomorphism of objects in `Rep S.k S.G` given an `i` in `Fin n.succ`
-  allowing us to undertake evaluation. -/
-def evalIso {n : ℕ} (c : Fin n.succ → S.C)
-    (i : Fin n.succ) : S.F.obj (OverColor.mk c) ≅ (S.FD.obj (Discrete.mk (c i))) ⊗
-      (OverColor.lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove)) :=
-  (S.F.mapIso (OverColor.equivToIso (HepLean.Fin.finExtractOne i))).trans <|
-  (S.F.mapIso (OverColor.mkSum (c ∘ (HepLean.Fin.finExtractOne i).symm))).trans <|
-  (S.F.μIso _ _).symm.trans <|
-  tensorIso
-    ((S.F.mapIso (OverColor.mkIso (by ext x; fin_cases x; rfl))).trans
-    (OverColor.forgetLiftApp S.FD (c i))) (S.F.mapIso (OverColor.mkIso (by ext x; simp)))
-
-lemma evalIso_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ)
-    (x : (i : Fin n.succ) → S.FD.obj (Discrete.mk (c i))) :
-    (S.evalIso c i).hom.hom (PiTensorProduct.tprod S.k x) =
-    x i ⊗ₜ[S.k] (PiTensorProduct.tprod S.k (fun k => x (i.succAbove k))) := by
-  simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, F_def, evalIso,
-    Iso.trans_hom, Functor.mapIso_hom, Iso.symm_hom, tensorIso_hom, Action.comp_hom,
-    Action.instMonoidalCategory_tensorHom_hom, Functor.id_obj, mk_hom, ModuleCat.coe_comp,
-    Function.comp_apply]
-  change (((lift.obj S.FD).map (mkIso _).hom).hom ≫
-    (forgetLiftApp S.FD (c i)).hom.hom ⊗
-    ((lift.obj S.FD).map (mkIso _).hom).hom)
-    (((lift.obj S.FD).μIso
-    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inl))
-    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inr))).inv.hom
-    (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractOne i).symm)).hom).hom
-    (((lift.obj S.FD).map (equivToIso (HepLean.Fin.finExtractOne i)).hom).hom
-    ((PiTensorProduct.tprod S.k) _)))) =_
-  rw [lift.map_tprod]
-  change (((lift.obj S.FD).map (mkIso _).hom).hom ≫
-    (forgetLiftApp S.FD (c i)).hom.hom ⊗
-    ((lift.obj S.FD).map (mkIso _).hom).hom)
-    (((lift.obj S.FD).μIso
-    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inl))
-    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inr))).inv.hom
-    (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractOne i).symm)).hom).hom
-    (((PiTensorProduct.tprod S.k) _)))) =_
-  rw [lift.map_tprod]
-  change ((TensorProduct.map (((lift.obj S.FD).map (mkIso _).hom).hom ≫
-    (forgetLiftApp S.FD (c i)).hom.hom)
-    ((lift.obj S.FD).map (mkIso _).hom).hom))
-    (((lift.obj S.FD).μIso
-    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inl))
-    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inr))).inv.hom
-    ((((PiTensorProduct.tprod S.k) _)))) =_
-  rw [lift.μIso_inv_tprod]
-  rw [TensorProduct.map_tmul]
-  erw [lift.map_tprod]
-  simp only [Nat.succ_eq_add_one, CategoryStruct.comp, Functor.id_obj,
-    instMonoidalCategoryStruct_tensorObj_hom, mk_hom, Sum.elim_inl, Function.comp_apply,
-    instMonoidalCategoryStruct_tensorObj_left, mkSum_homToEquiv, Equiv.refl_symm,
-    LinearMap.coe_comp, Sum.elim_inr]
-  congr 1
-  · change (forgetLiftApp S.FD (c i)).hom.hom
-      (((lift.obj S.FD).map (mkIso _).hom).hom
-      ((PiTensorProduct.tprod S.k) _)) = _
-    rw [lift.map_tprod]
-    rw [forgetLiftApp_hom_hom_apply_eq]
-    apply congrArg
-    funext i
-    match i with
-    | (0 : Fin 1) =>
-      simp only [mk_hom, Fin.isValue, Function.comp_apply, lift.discreteFunctorMapEqIso,
-        eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv,
-        LinearEquiv.ofLinear_apply]
-      rfl
-  · apply congrArg
-    funext k
-    simp only [lift.discreteFunctorMapEqIso, Functor.mapIso_hom, eqToIso.hom, Functor.mapIso_inv,
-      eqToIso.inv, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv,
-      LinearEquiv.ofLinear_apply]
-    change (S.FD.map (eqToHom _)).hom
-      (x ((HepLean.Fin.finExtractOne i).symm ((Sum.inr k)))) = _
-    have h1' {a b : Fin n.succ} (h : a = b) :
-      (S.FD.map (eqToHom (by rw [h]))).hom (x a) = x b := by
-      subst h
-      simp
-    refine h1' ?_
-    exact HepLean.Fin.finExtractOne_symm_inr_apply i k
-
-/-- The linear map giving the coordinate of a vector with respect to the given basis.
-  Important Note: This is not a morphism in the category of representations. In general,
-  it cannot be lifted thereto. -/
-def evalLinearMap {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (S.repDim (c i))) :
-    S.FD.obj { as := c i } →ₗ[S.k] S.k where
-  toFun := fun v => (S.basis (c i)).repr v e
-  map_add' := by simp
-  map_smul' := by simp
-
-/-- The evaluation map, used to evaluate indices of tensors.
-  Important Note: The evaluation map is in general, not equivariant with respect to
-  group actions. It is a morphism in the underlying module category, not the category
-  of representations. -/
-def evalMap {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (S.repDim (c i))) :
-    (S.F.obj (OverColor.mk c)).V ⟶ (S.F.obj (OverColor.mk (c ∘ i.succAbove))).V :=
-  (S.evalIso c i).hom.hom ≫ ((Action.forgetMonoidal _ _).μIso _ _).inv
-  ≫ ModuleCat.asHom (TensorProduct.map (S.evalLinearMap i e) LinearMap.id) ≫
-  ModuleCat.asHom (TensorProduct.lid S.k _).toLinearMap
-
-lemma evalMap_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (S.repDim (c i)))
-    (x : (i : Fin n.succ) → S.FD.obj (Discrete.mk (c i))) :
-    (S.evalMap i e) (PiTensorProduct.tprod S.k x) =
-    (((S.basis (c i)).repr (x i) e) : S.k) •
-    (PiTensorProduct.tprod S.k
-    (fun k => x (i.succAbove k)) : S.F.obj (OverColor.mk (c ∘ i.succAbove))) := by
-  rw [evalMap]
-  simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V,
-    Action.forgetMonoidal_toLaxMonoidalFunctor_toFunctor, Action.forget_obj, Functor.id_obj, mk_hom,
-    Function.comp_apply, ModuleCat.coe_comp]
-  erw [evalIso_tprod]
-  change ((TensorProduct.lid S.k ↑((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove))).V))
-    (((TensorProduct.map (S.evalLinearMap i e) LinearMap.id))
-    (((Action.forgetMonoidal (ModuleCat S.k) (MonCat.of S.G)).μIso (S.FD.obj { as := c i })
-    ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove)))).inv
-    (x i ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun k => x (i.succAbove k)))) = _
-  simp only [Nat.succ_eq_add_one, Action.forgetMonoidal_toLaxMonoidalFunctor_toFunctor,
-    Action.forget_obj, Action.instMonoidalCategory_tensorObj_V, MonoidalFunctor.μIso,
-    Action.forgetMonoidal_toLaxMonoidalFunctor_μ, asIso_inv, IsIso.inv_id, Equivalence.symm_inverse,
-    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
-    Functor.id_obj, mk_hom, Function.comp_apply, ModuleCat.id_apply, TensorProduct.map_tmul,
-    LinearMap.id_coe, id_eq, TensorProduct.lid_tmul]
-  rfl
-
-end TensorSpecies
-
 /-- A syntax tree for tensor expressions. -/
 inductive TensorTree (S : TensorSpecies) : {n : ℕ} → (Fin n → S.C) → Type where
   /-- A general tensor node. -/

HepLean/Tensors/Tree/Elab.lean

@@ -425,14 +425,7 @@ def getPermutation (l1 l2 : List (TSyntax `indexExpr)) : TermElabM (List (ℕ))
     (fun x => l1enum.find? (fun y => Lean.TSyntax.getId y.2 = Lean.TSyntax.getId x))
   return l2''.map fun x => x.1
 
-/-- Takes two maps `Fin n → Fin n` and returns the equivelance they form. -/
-def finMapToEquiv (f1 : Fin n → Fin m) (f2 : Fin m → Fin n)
-    (h : ∀ x, f1 (f2 x) = x := by decide)
-    (h' : ∀ x, f2 (f1 x) = x := by decide) : Fin n ≃ Fin m where
-  toFun := f1
-  invFun := f2
-  left_inv := h'
-  right_inv := h
+open HepLean.Fin
 
 /-- Given two lists of indices returns the permutation between them based on `finMapToEquiv`. -/
 def getPermutationSyntax (l1 l2 : List (TSyntax `indexExpr)) : TermElabM Term := do

HepLean/Tensors/Tree/NodeIdentities/Basic.lean

@@ -140,7 +140,7 @@ lemma perm_eq_iff_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
       apply Hom.ext
       ext x
       change (Hom.toEquiv σ) ((Hom.toEquiv σ).symm x) = x
-      simp
+      simp [-OverColor.mk_left]
     rw [h1]
     simp
 
@@ -250,6 +250,7 @@ lemma prod_add_both {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
 
 -/
 
+/-- The action of a group element can be brought though a scalar multiplication. -/
 lemma smul_action {n : ℕ} {c : Fin n → S.C} (g : S.G) (a : S.k) (t : TensorTree S c) :
     (smul a (action g t)).tensor = (action g (smul a t)).tensor := by
   simp only [smul_tensor, action_tensor, map_smul]

HepLean/Tensors/Tree/NodeIdentities/PermProd.lean

@@ -29,12 +29,23 @@ variable {S : TensorSpecies} {n n' n2 : ℕ}
 def permProdLeft := (equivToIso finSumFinEquiv).inv ≫ σ ▷ OverColor.mk c2
   ≫ (equivToIso finSumFinEquiv).hom
 
+@[simp]
+lemma permProdLeft_toEquiv : Hom.toEquiv (permProdLeft c2 σ) =  finSumFinEquiv.symm.trans
+    (((Hom.toEquiv σ).sumCongr (Equiv.refl (Fin n2))).trans finSumFinEquiv)  := by
+  simp [permProdLeft]
+
+
 /-- The permutation that arises when moving a `perm` node in the right entry through a `prod` node.
   This permutation is defined using left-whiskering and composition with `finSumFinEquiv`
   based-isomorphisms. -/
 def permProdRight := (equivToIso finSumFinEquiv).inv ≫ OverColor.mk c2 ◁ σ
   ≫ (equivToIso finSumFinEquiv).hom
 
+@[simp]
+lemma permProdRight_toEquiv : Hom.toEquiv (permProdRight c2 σ) = finSumFinEquiv.symm.trans
+    (((Equiv.refl (Fin n2)).sumCongr (Hom.toEquiv σ)).trans finSumFinEquiv) := by
+  simp [permProdRight]
+
 /-- When a `prod` acts on a `perm` node in the left entry, the `perm` node can be moved through
   the `prod` node via right-whiskering. -/
 theorem prod_perm_left (t : TensorTree S c) (t2 : TensorTree S c2) :

HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean

@@ -31,6 +31,11 @@ def braidPerm : OverColor.mk (Sum.elim c2 c ∘ ⇑finSumFinEquiv.symm) ⟶
   (β_ (OverColor.mk c2) (OverColor.mk c)).hom
   ≫ (equivToIso finSumFinEquiv).hom
 
+@[simp]
+lemma braidPerm_toEquiv : Hom.toEquiv (braidPerm c c2) = finSumFinEquiv.symm.trans
+    ((Equiv.sumComm (Fin n2) (Fin n)).trans finSumFinEquiv) := by
+  simp [braidPerm]
+
 lemma finSumFinEquiv_comp_braidPerm :
     (equivToIso finSumFinEquiv).hom ≫ braidPerm c c2 =
     (β_ (OverColor.mk c2) (OverColor.mk c)).hom