feat: Start on braiding of products

HepLean.lean

@@ -122,3 +122,4 @@ import HepLean.Tensors.Tree.NodeIdentities.Basic
 import HepLean.Tensors.Tree.NodeIdentities.ContrContr
 import HepLean.Tensors.Tree.NodeIdentities.PermContr
 import HepLean.Tensors.Tree.NodeIdentities.PermProd
+import HepLean.Tensors.Tree.NodeIdentities.ProdComm

HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean

@@ -0,0 +1,35 @@
+/-
+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.Basic
+/-!
+
+# Commuting products
+
+The results here follow from the properties of Monoidal categories and monoidal functors.
+-/
+
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+open OverColor
+open HepLean.Fin
+
+namespace TensorTree
+
+variable {S : TensorStruct} {n n2 : ℕ}
+    (c : Fin n → S.C) (c2 : Fin n2 → S.C)
+
+def braidPerm : OverColor.mk (Sum.elim c2 c ∘ ⇑finSumFinEquiv.symm) ⟶
+    OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm) :=
+  (equivToIso finSumFinEquiv).inv ≫
+  (BraidedCategory.braiding (OverColor.mk c2) (OverColor.mk c)).hom
+  ≫ (equivToIso finSumFinEquiv).hom
+
+theorem prod_comm (t : TensorTree S c) (t2 : TensorTree S c2) :
+    (prod t t2).tensor = (perm (braidPerm c c2) (prod t2 t)).tensor := by
+
+  sorry
+end TensorTree