The commutativity of Permutations and contractions.

There is very likely a better way to do this using TensorSpecies.contrMap_tprod.

theorem TensorSpecies.contrFin1Fin1_naturality (S : TensorSpecies) {n : ℕ} {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)) (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.extractTwoAux' i j σ)).hom (S.contrFin1Fin1 c1 i j h).hom.hom = CategoryTheory.CategoryStruct.comp (S.contrFin1Fin1 c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ((PhysLean.Fin.finExtractOnePerm ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) (IndexNotation.OverColor.Hom.toEquiv σ)).symm j) ⋯).hom.hom ((IndexNotation.OverColor.Discrete.pairτ S.FD S.τ).map (CategoryTheory.Discrete.eqToHom ⋯)).hom

theorem TensorSpecies.contrIso_comm_aux_1 (S : TensorSpecies) {n : ℕ} {c c1 : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (S.F.map σ).hom (S.F.map (IndexNotation.OverColor.equivToIso (PhysLean.Fin.finExtractTwo i j)).hom).hom) (S.F.map (IndexNotation.OverColor.mkSum (c1 ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm)).hom).hom = CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.equivToIso (PhysLean.Fin.finExtractTwo ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ((PhysLean.Fin.finExtractOnePerm ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) (IndexNotation.OverColor.Hom.toEquiv σ)).symm j))).hom).hom (CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.mkSum (c ∘ ⇑(PhysLean.Fin.finExtractTwo ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ((PhysLean.Fin.finExtractOnePerm ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) (IndexNotation.OverColor.Hom.toEquiv σ)).symm j)).symm)).hom).hom (S.F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (IndexNotation.OverColor.extractTwoAux' i j σ) (IndexNotation.OverColor.extractTwoAux i j σ))).hom)

theorem TensorSpecies.contrIso_comm_aux_2 (S : TensorSpecies) {n : ℕ} {c c1 : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : CategoryTheory.CategoryStruct.comp (S.F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (IndexNotation.OverColor.extractTwoAux' i j σ) (IndexNotation.OverColor.extractTwoAux i j σ))).hom (CategoryTheory.Functor.Monoidal.μIso S.F (IndexNotation.OverColor.mk ((c1 ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) (IndexNotation.OverColor.mk ((c1 ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Monoidal.μIso S.F (IndexNotation.OverColor.mk ((c ∘ ⇑(PhysLean.Fin.finExtractTwo ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j)).symm) ∘ Sum.inl)) (IndexNotation.OverColor.mk ((c ∘ ⇑(PhysLean.Fin.finExtractTwo ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j)).symm) ∘ Sum.inr))).inv.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (S.F.map (IndexNotation.OverColor.extractTwoAux' i j σ)) (S.F.map (IndexNotation.OverColor.extractTwoAux i j σ))).hom

theorem TensorSpecies.contrIso_comm_aux_3 (S : TensorSpecies) {n : ℕ} {c c1 : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : CategoryTheory.CategoryStruct.comp (((Action.functorCategoryEquivalence (ModuleCat S.k) ↑(MonCat.of S.G)).symm.inverse.map (S.F.map (IndexNotation.OverColor.extractTwoAux i j σ))).app PUnit.unit) (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom = CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom (S.F.map (IndexNotation.OverColor.extractTwo i j σ)).hom

def TensorSpecies.contrIsoComm (S : TensorSpecies) {n : ℕ} {c c1 : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((IndexNotation.OverColor.Discrete.pairτ S.FD S.τ).obj { as := c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) }) (S.F.obj (IndexNotation.OverColor.mk (c ∘ Fin.succAbove ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ∘ Fin.succAbove ((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j)))) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj ((IndexNotation.OverColor.Discrete.pairτ S.FD S.τ).obj { as := c1 i }) (S.F.obj (IndexNotation.OverColor.mk (c1 ∘ i.succAbove ∘ j.succAbove)))

A helper function used to proof the relation between perm and contr.

Equations

• One or more equations did not get rendered due to their size.

theorem TensorSpecies.contrIso_comm_aux_5 (S : TensorSpecies) {n : ℕ} {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)) (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (S.F.map (IndexNotation.OverColor.extractTwoAux' i j σ)) (S.F.map (IndexNotation.OverColor.extractTwoAux i j σ))).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (S.contrFin1Fin1 c1 i j h).hom.hom (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (S.contrFin1Fin1 c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ((PhysLean.Fin.finExtractOnePerm ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) (IndexNotation.OverColor.Hom.toEquiv σ)).symm j) ⋯).hom.hom (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom) (S.contrIsoComm σ).hom

theorem TensorSpecies.contrIso_comm_map (S : TensorSpecies) {n : ℕ} {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)} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : CategoryTheory.CategoryStruct.comp (S.F.map σ) (S.contrIso c1 i j h).hom = CategoryTheory.CategoryStruct.comp (S.contrIso c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j) ⋯).hom (S.contrIsoComm σ)

theorem TensorSpecies.contrMap_naturality (S : TensorSpecies) {n : ℕ} {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)} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : CategoryTheory.CategoryStruct.comp (S.F.map σ) (S.contrMap c1 i j h) = CategoryTheory.CategoryStruct.comp (S.contrMap c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j) ⋯) (S.F.map (IndexNotation.OverColor.extractTwo i j σ))

Contraction commutes with S.F.map σ on removing corresponding indices from σ.

theorem TensorTree.perm_contr {S : TensorSpecies} {n : ℕ} {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)} (t : TensorTree S c) (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : (contr i j h (perm σ t)).tensor = (perm (IndexNotation.OverColor.extractTwo i j σ) (contr ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j) ⋯ t)).tensor

Permuting indices, and then contracting is equivalent to contracting and then permuting, once care is taking about ensuring one is contracting the same indices.

theorem TensorTree.perm_contr_congr_mkIso_cond {S : TensorSpecies} {n : ℕ} {c c1 : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} {σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1} {i' : Fin n.succ.succ} {j' : Fin n.succ} (hi : i' = (IndexNotation.OverColor.Hom.toEquiv σ).symm i) (hj : j' = (IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j) : c ∘ i'.succAbove ∘ j'.succAbove = c ∘ Fin.succAbove ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ∘ Fin.succAbove ((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j)

theorem TensorTree.perm_contr_congr_contr_cond {S : TensorSpecies} {n : ℕ} {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)) {σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1} {i' : Fin n.succ.succ} {j' : Fin n.succ} (hi : i' = (IndexNotation.OverColor.Hom.toEquiv σ).symm i) (hj : j' = (IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j) : c (i'.succAbove j') = S.τ (c i')

theorem TensorTree.perm_contr_congr {S : TensorSpecies} {n : ℕ} {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)} {t : TensorTree S c} {σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1} (i' : Fin n.succ.succ) (j' : Fin n.succ) (hi : i' = (IndexNotation.OverColor.Hom.toEquiv σ).symm i := by decide) (hj : j' = (IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j := by decide) : (contr i j h (perm σ t)).tensor = (perm (CategoryTheory.CategoryStruct.comp (IndexNotation.OverColor.mkIso ⋯).hom (IndexNotation.OverColor.extractTwo i j σ)) (contr i' j' ⋯ t)).tensor