The peel rotation as a permutation and a cast

The peel rotation splits as a same-arity permutation followed by an arity cast; the permutation feeds the braiding-word transport and the cast transports as an equality of powers.

def RS.capPeelPerm (m : ℕ) : Equiv.Perm (Fin (m + 1 + (m + 1)))

The peel rotation as a permutation of the source arity.

Equations

• RS.capPeelPerm m = (RS.capPeelRotation m).trans (finCongr ⋯)

theorem RS.capPeelEquiv_split (m : ℕ) : capPeelRotation m = Equiv.trans (capPeelPerm m) (finCongr ⋯)

The peel rotation is its permutation followed by the arity cast.

theorem RS.bmc_capPeel_split {R : ℕ} (f : EdgeRankParameter R) (m : ℕ) : bundleMapClass f (capPeelRotation m) = ((HomSpace.comp f (m + 1 + (m + 1)) (m + 1 + (m + 1)) (m + m + 2)) (bundleMapClass f (capPeelPerm m))) (bundleMapClass f (finCongr ⋯))

The peel bundle map splits as permutation then cast.

theorem RS.stdToOmega_bmc_cast {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) {n₁ n₂ : ℕ} (h : n₁ = n₂) : CategoryTheory.CategoryStruct.comp (stdToOmega f P e n₁) (P.ω.map (bundleMapClass f (finCongr h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (stdToOmega f P e n₂)

The cast transport: an arity-cast bundle map conjugates through the model transport into the equality of powers.