feat: Prove commutivity of prod node.

HepLean/Tensors/OverColor/Lift.lean

@@ -453,7 +453,7 @@ lemma right_unitality (X : OverColor C) : (rightUnitor (objObj' F X)).hom =
     LinearEquiv.ofLinear_apply]
   rfl
 
-lemma braided' (X Y : OverColor C)  : (μ F X Y).hom ≫  (objMap' F) (β_ X Y).hom =
+lemma braided' (X Y : OverColor C) : (μ F X Y).hom ≫ (objMap' F) (β_ X Y).hom =
     (β_ (objObj' F X) (objObj' F Y)).hom ≫ (μ F Y X).hom := by
   ext1
   apply HepLean.PiTensorProduct.induction_tmul (fun p q => ?_)
@@ -529,7 +529,7 @@ def obj' : BraidedFunctor (OverColor C) (Rep k G) where
   left_unitality := left_unitality F
   right_unitality := right_unitality F
   braided X Y := by
-    change (objMap' F) (β_ X Y).hom  = _
+    change (objMap' F) (β_ X Y).hom = _
     rw [braided F X Y]
     congr
     simp_all only [IsIso.Iso.inv_hom]
@@ -684,6 +684,7 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ BraidedFunctor (OverColor
     rfl
 
 namespace lift
+variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F')
 
 lemma map_tprod (F : Discrete C ⥤ Rep k G) {X Y : OverColor C} (f : X ⟶ Y)
     (p : (i : X.left) → F.obj (Discrete.mk <| X.hom i)) :
@@ -719,6 +720,12 @@ lemma μIso_inv_tprod (F : Discrete C ⥤ Rep k G) (X Y : OverColor C)
   | Sum.inl i => rfl
   | Sum.inr i => rfl
 
+@[simp]
+lemma inv_μ (X Y : OverColor C) : inv ((lift.obj F).μ X Y) =
+    (lift.μ F X Y).inv := by
+  change inv (lift.μ F X Y).hom = _
+  exact IsIso.Iso.inv_hom (μ F X Y)
+
 end lift
 /-- The natural inclusion of `Discrete C` into `OverColor C`. -/
 def incl : Discrete C ⥤ OverColor C := Discrete.functor fun c =>

HepLean/Tensors/Tree/Basic.lean

@@ -59,7 +59,7 @@ instance : CommRing S.k := S.k_commRing
 instance : Group S.G := S.G_group
 
 /-- The lift of the functor `S.F` to a monoidal functor. -/
-def F : MonoidalFunctor (OverColor S.C) (Rep S.k S.G) := (OverColor.lift).obj S.FDiscrete
+def F : BraidedFunctor (OverColor S.C) (Rep S.k S.G) := (OverColor.lift).obj S.FDiscrete
 
 lemma F_def : F S = (OverColor.lift).obj S.FDiscrete := rfl
 

HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean

@@ -8,7 +8,7 @@ import HepLean.Tensors.Tree.Basic
 
 # Commuting products
 
-The results here follow from the properties of Monoidal categories and monoidal functors.
+The results here follow from the properties of braided categories and braided functors.
 -/
 
 open IndexNotation
@@ -22,14 +22,53 @@ namespace TensorTree
 variable {S : TensorStruct} {n n2 : ℕ}
     (c : Fin n → S.C) (c2 : Fin n2 → S.C)
 
+/-- 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. -/
 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
+  (β_ (OverColor.mk c2) (OverColor.mk c)).hom
   ≫ (equivToIso finSumFinEquiv).hom
 
+lemma finSumFinEquiv_comp_braidPerm :
+    (equivToIso finSumFinEquiv).hom ≫ braidPerm c c2 =
+    (β_ (OverColor.mk c2) (OverColor.mk c)).hom
+    ≫ (equivToIso finSumFinEquiv).hom := by
+  rw [braidPerm]
+  simp
+
+/-- The arguments of a `prod` node can be commuted using braiding. -/
 theorem prod_comm (t : TensorTree S c) (t2 : TensorTree S c2) :
     (prod t t2).tensor = (perm (braidPerm c c2) (prod t2 t)).tensor := by
+  rw [perm_tensor]
+  nth_rewrite 2 [prod_tensor]
+  change _ = (S.F.map (equivToIso finSumFinEquiv).hom ≫ S.F.map (braidPerm c c2)).hom
+    ((S.F.μ (OverColor.mk c2) (OverColor.mk c)).hom (t2.tensor ⊗ₜ[S.k] t.tensor))
+  rw [← S.F.map_comp]
+  rw [finSumFinEquiv_comp_braidPerm]
+  rw [S.F.map_comp]
+  simp only [BraidedFunctor.braided, Category.assoc, Action.comp_hom,
+    Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    ModuleCat.coe_comp, Function.comp_apply]
+  rw [prod_tensor]
+  apply congrArg
+  apply congrArg
+  change _ = (β_ (S.F.obj (OverColor.mk c2)) (S.F.obj (OverColor.mk c))).hom.hom
+    ((inv (lift.μ S.FDiscrete (OverColor.mk c2) (OverColor.mk c)).hom).hom
+    ((lift.μ S.FDiscrete (OverColor.mk c2) (OverColor.mk c)).hom.hom (t2.tensor ⊗ₜ[S.k] t.tensor)))
+  simp only [Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    lift.objObj'_V_carrier, instMonoidalCategoryStruct_tensorObj_left,
+    instMonoidalCategoryStruct_tensorObj_hom, mk_hom, IsIso.Iso.inv_hom]
+  change _ = (β_ (S.F.obj (OverColor.mk c2)) (S.F.obj (OverColor.mk c))).hom.hom
+    (((lift.μ S.FDiscrete (OverColor.mk c2) (OverColor.mk c)).hom ≫
+    (lift.μ S.FDiscrete (OverColor.mk c2) (OverColor.mk c)).inv).hom ((t2.tensor ⊗ₜ[S.k] t.tensor)))
+  simp only [Action.instMonoidalCategory_tensorObj_V, Iso.hom_inv_id, Action.id_hom,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, lift.objObj'_V_carrier, mk_hom,
+    ModuleCat.id_apply]
+  rfl
 
-  sorry
 end TensorTree