Associativity of products

The results here follow from the properties of braided categories and braided functors.

def TensorTree.assocPerm {S : TensorSpecies} {n n2 n3 : ℕ} (c : Fin n → S.C) (c2 : Fin n2 → S.C) (c3 : Fin n3 → S.C) : IndexNotation.OverColor.mk (Sum.elim (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm) c3 ∘ ⇑finSumFinEquiv.symm) ≅ IndexNotation.OverColor.mk (Sum.elim c (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm) ∘ ⇑finSumFinEquiv.symm)

The permutation that arises from associativity of prod node. This permutation is defined using braiding and composition with finSumFinEquiv based-isomorphisms.

Equations

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

theorem TensorTree.finSumFinEquiv_comp_assocPerm {S : TensorSpecies} {n n2 n3 : ℕ} (c : Fin n → S.C) (c2 : Fin n2 → S.C) (c3 : Fin n3 → S.C) : CategoryTheory.CategoryStruct.comp (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom (assocPerm c c2 c3).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRightIso (IndexNotation.OverColor.equivToIso finSumFinEquiv).symm (IndexNotation.OverColor.mk c3)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (IndexNotation.OverColor.mk c) (IndexNotation.OverColor.mk c2) (IndexNotation.OverColor.mk c3)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeftIso (IndexNotation.OverColor.mk c) (IndexNotation.OverColor.equivToIso finSumFinEquiv)).hom (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom))

@[simp]

theorem TensorTree.assocPerm_toHomEquiv_hom {S : TensorSpecies} {n n2 n3 : ℕ} (c : Fin n → S.C) (c2 : Fin n2 → S.C) (c3 : Fin n3 → S.C) : IndexNotation.OverColor.Hom.toEquiv (assocPerm c c2 c3).hom = finSumFinEquiv.symm.trans ((finSumFinEquiv.symm.sumCongr (Equiv.refl (Fin n3))).trans ((Equiv.sumAssoc (Fin n) (Fin n2) (Fin n3)).trans (((Equiv.refl (Fin n)).sumCongr finSumFinEquiv).trans finSumFinEquiv)))

@[simp]

theorem TensorTree.assocPerm_toHomEquiv_inv {S : TensorSpecies} {n n2 n3 : ℕ} (c : Fin n → S.C) (c2 : Fin n2 → S.C) (c3 : Fin n3 → S.C) : IndexNotation.OverColor.Hom.toEquiv (assocPerm c c2 c3).inv = finSumFinEquiv.symm.trans (((Equiv.refl (Fin n)).sumCongr finSumFinEquiv.symm).trans ((Equiv.sumAssoc (Fin n) (Fin n2) (Fin n3)).symm.trans ((finSumFinEquiv.sumCongr (Equiv.refl (Fin n3))).trans finSumFinEquiv)))

theorem TensorTree.prod_assoc {S : TensorSpecies} {n n2 n3 : ℕ} (c : Fin n → S.C) (c2 : Fin n2 → S.C) (c3 : Fin n3 → S.C) (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree S c3) : (t.prod (t2.prod t3)).tensor = (perm (assocPerm c c2 c3).hom ((t.prod t2).prod t3)).tensor

The prod obeys associativity.

theorem TensorTree.prod_assoc' {S : TensorSpecies} {n n2 n3 : ℕ} (c : Fin n → S.C) (c2 : Fin n2 → S.C) (c3 : Fin n3 → S.C) (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree S c3) : ((t.prod t2).prod t3).tensor = (perm (assocPerm c c2 c3).inv (t.prod (t2.prod t3))).tensor

The alternative version of associativity for prod where the permutation is on the opposite side.