The skein-side adjacent braiding and the transport intertwining

The adjacent braiding of strands in the skein category, mirroring powBraid's recursion, and the key intertwining: the model transport stdToOmega conjugates the skein braiding into the model braiding. The top square is proved abstractly for any braided monoidal functor — where every rewrite fires — and the strictness of the skein associator enters only through a small concrete collapse.

theorem RS.braid_top_intertwine {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory C] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.Functor C D) [F.LaxBraided] {PA PX : D} {A X : C} (tA : PA ⟶ F.obj A) (tx : PX ⟶ F.obj X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom tA tx) (CategoryTheory.Functor.LaxMonoidal.μ F A X)) tx) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj A X) X) (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (β_ X X).hom) (CategoryTheory.MonoidalCategoryStruct.associator A X X).inv)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator PA PX PX).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft PA (β_ PX PX).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator PA PX PX).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom tA tx) (CategoryTheory.Functor.LaxMonoidal.μ F A X)) tx) (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj A X) X))))

The abstract top braiding square: for a braided monoidal functor, transporting two point identifications through the structure maps intertwines the associator-conjugated braiding of the last two factors.

noncomputable def RS.skeinPowBraid {R : ℕ} (f : EdgeRankParameter R) (n i : ℕ) : i + 2 ≤ n → ({ arity := n } ⟶ { arity := n })

The skein-side adjacent braiding at position i.

Equations

• One or more equations did not get rendered due to their size.
• RS.skeinPowBraid f 0 x✝¹ x✝ = absurd x✝ ⋯
• RS.skeinPowBraid f 1 x✝¹ x✝ = absurd x✝ ⋯

theorem RS.skein_associator_collapse {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : (CategoryTheory.MonoidalCategoryStruct.associator { arity := n } { arity := 1 } { arity := 1 }).hom = CategoryTheory.CategoryStruct.id { arity := n + 2 }

The skein associator at concrete arities collapses to the identity.

theorem RS.skein_associator_inv_collapse {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : (CategoryTheory.MonoidalCategoryStruct.associator { arity := n } { arity := 1 } { arity := 1 }).inv = CategoryTheory.CategoryStruct.id { arity := n + 2 }

The inverse skein associator at concrete arities collapses to the identity.

theorem RS.stdToOmega_powBraid {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (n i : ℕ) (h : i + 2 ≤ n) : CategoryTheory.CategoryStruct.comp (stdToOmega f P e n) (P.ω.map (skeinPowBraid f n i h)) = CategoryTheory.CategoryStruct.comp (powBraid (stdSuperPair k ℓ) n i h) (stdToOmega f P e n)

The transport intertwining: the model transport carries the skein-side adjacent braiding to the model-side adjacent braiding.