Bundle-map permutations through the model transport

Composing the adjacent-swap collapse with the transport intertwining along an adjacent-transposition word: the image of any permutation bundle map conjugates through stdToOmega into the corresponding word of model braidings.

theorem RS.adjTrans_eq_adjSwap {n : ℕ} (i : Fin n) : adjTrans i = adjSwapEquiv (n + 1) ↑i ⋯

The adjacent transposition is the adjacent swap.

noncomputable def RS.powBraidWord (V : SuperVect) {n : ℕ} : List (Fin n) → (superPow V (n + 1) ⟶ superPow V (n + 1))

The model-side braiding word.

Equations

• RS.powBraidWord V [] = CategoryTheory.CategoryStruct.id (RS.superPow V (n + 1))
• RS.powBraidWord V (i :: w) = CategoryTheory.CategoryStruct.comp (RS.powBraidWord V w) (RS.powBraid V (n + 1) ↑i ⋯)

theorem RS.stdToOmega_bmc_word {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) {n : ℕ} (w : List (Fin n)) : CategoryTheory.CategoryStruct.comp (stdToOmega f P e (n + 1)) (P.ω.map (bundleMapClass f (List.map adjTrans w).prod)) = CategoryTheory.CategoryStruct.comp (powBraidWord (stdSuperPair k ℓ) w) (stdToOmega f P e (n + 1))

The word intertwining: the image of the word's product bundle map conjugates into the model braiding word.

theorem RS.stdToOmega_bmc_perm {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) {n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) : CategoryTheory.CategoryStruct.comp (stdToOmega f P e (n + 1)) (P.ω.map (bundleMapClass f σ)) = CategoryTheory.CategoryStruct.comp (powBraidWord (stdSuperPair k ℓ) (adjWord σ)) (stdToOmega f P e (n + 1))

The permutation intertwining: any permutation bundle map conjugates into the model braiding word of its adjacent-transposition word.