The sort as a permutation and a cast

The inverse sort of the star factorization splits as a same-arity permutation followed by the degree-sum cast, feeding the braiding-word transport and the cast transport respectively.

noncomputable def RS.sortSplitPerm (W : ClosedFragment) : Equiv.Perm (Fin (degList (starAssignEnum W)).sum)

The inverse sort as a permutation of the degree-sum arity.

Equations

• RS.sortSplitPerm W = (RS.sortEquiv (RS.starAssignEnum W)).symm.trans (finCongr ⋯)

theorem RS.sortEquiv_symm_split (W : ClosedFragment) : (sortEquiv (starAssignEnum W)).symm = Equiv.trans (sortSplitPerm W) (finCongr ⋯)

The inverse sort is its permutation followed by the arity cast.

theorem RS.bmc_sort_split {R : ℕ} (f : EdgeRankParameter R) (W : ClosedFragment) : bundleMapClass f (sortEquiv (starAssignEnum W)).symm = ((HomSpace.comp f (degList (starAssignEnum W)).sum (degList (starAssignEnum W)).sum (edgeCount W + edgeCount W)) (bundleMapClass f (sortSplitPerm W))) (bundleMapClass f (finCongr ⋯))

The sort bundle map splits as permutation then cast.