Towards the matching cap

Left composition with a bundle-map class relabels the incoming boundary: the class-level mirror of bundleMapCompose. This is the absorption step for permuted caps — composing a braiding word into the strand-bundle cap yields the cap of the permuted matching.

theorem RS.bundleMapClass_comp_left {R : ℕ} (f : EdgeRankParameter R) {n m u : ℕ} (e : Fin n ≃ Fin m) (X : Fragment (Fin (m + u))) : ((HomSpace.comp f n m u) (bundleMapClass f e)) (HomSpace.ofFragment f.val X) = HomSpace.ofFragment f.val (X.relabel (finSumFinEquiv.symm.trans ((e.symm.sumCongr (Equiv.refl (Fin u))).trans finSumFinEquiv)))

Left composition with a bundle-map class relabels the fragment along the incoming transport.