The top braiding through the merge

The braiding of the last two strands commutes with the block merge: whiskering the two-strand braid inside the last block and merging equals merging and braiding on top. Abstract braided coherence first, instantiated to the powers.

theorem RS.powMerge_topBraid (V : SuperVect) (a : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (superPow V a) (topBraid V 0)) (powMerge V a 2) = CategoryTheory.CategoryStruct.comp (powMerge V a 2) (topBraid V a)

The merge-braid exchange on powers: braiding inside the last two-strand block and merging equals merging and braiding on top.

theorem RS.powMerge_isIso (V : SuperVect) (a b : ℕ) : CategoryTheory.IsIso (powMerge V a b)

The block merge is an isomorphism.

theorem RS.powMerge_evenMap_surjective (V : SuperVect) (a b : ℕ) : Function.Surjective ⇑(powMerge V a b).evenMap

Every power element is a merge image.

theorem RS.powMerge_oddMap_surjective (V : SuperVect) (a b : ℕ) : Function.Surjective ⇑(powMerge V a b).oddMap

Every odd power element is a merge image.