Commuting products

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

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

The permutation that arises when moving a commuting terms in a 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.

@[simp]

theorem TensorTree.braidPerm_toEquiv {S : TensorSpecies} {n n2 : ℕ} (c : Fin n → S.C) (c2 : Fin n2 → S.C) : IndexNotation.OverColor.Hom.toEquiv (braidPerm c c2) = finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n2) (Fin n)).trans finSumFinEquiv)

theorem TensorTree.finSumFinEquiv_comp_braidPerm {S : TensorSpecies} {n n2 : ℕ} (c : Fin n → S.C) (c2 : Fin n2 → S.C) : CategoryTheory.CategoryStruct.comp (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom (braidPerm c c2) = CategoryTheory.CategoryStruct.comp (β_ (IndexNotation.OverColor.mk c2) (IndexNotation.OverColor.mk c)).hom (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom

theorem TensorTree.prod_comm {S : TensorSpecies} {n n2 : ℕ} (c : Fin n → S.C) (c2 : Fin n2 → S.C) (t : TensorTree S c) (t2 : TensorTree S c2) : (t.prod t2).tensor = (perm (braidPerm c c2) (t2.prod t)).tensor

The arguments of a prod node can be commuted using braiding.