The skein braiding as a bundle map

The skein-side adjacent braiding collapses to the bundle-map class of the adjacent transposition: the whiskers are block sums of label equivalences and the one-strand braiding is the transpose, so the whole recursion lives in the bundle-map calculus.

def RS.adjSwapEquiv (n i : ℕ) (h : i + 2 ≤ n) : Fin n ≃ Fin n

The adjacent swap as a label equivalence.

Equations

• RS.adjSwapEquiv n i h = Equiv.swap ⟨i, ⋯⟩ ⟨i + 1, ⋯⟩

theorem RS.swap_val {m : ℕ} (a b x : Fin m) : ↑((Equiv.swap a b) x) = if ↑x = ↑a then ↑b else if ↑x = ↑b then ↑a else ↑x

The value of a swap, on underlying values.

theorem RS.adjSwapEquiv_val (n i : ℕ) (h : i + 2 ≤ n) (x : Fin n) : ↑((adjSwapEquiv n i h) x) = if ↑x = i then i + 1 else if ↑x = i + 1 then i else ↑x

The value of the adjacent swap.

theorem RS.tensorMapEquiv_top (n : ℕ) : tensorMapEquiv (Equiv.refl (Fin n)) (transposeEquiv 1 1) = adjSwapEquiv (n + 2) n ⋯

The top block sum is the adjacent swap.

theorem RS.tensorMapEquiv_whisker (n i : ℕ) (h : i + 2 ≤ n + 1) : tensorMapEquiv (adjSwapEquiv (n + 1) i h) (Equiv.refl (Fin 1)) = adjSwapEquiv (n + 2) i ⋯

The whiskered block sum is the shifted adjacent swap.

theorem RS.skeinPowBraid_bmc {R : ℕ} (f : EdgeRankParameter R) (n i : ℕ) (h : i + 2 ≤ n) : skeinPowBraid f n i h = bundleMapClass f (adjSwapEquiv n i h)

The skein adjacent braiding is the adjacent-swap bundle map.