The normalisation step for a word of free letters

Gathering every head of a word of free letters A ⊗ V onto its last letter can be done one letter at a time: normalise all but the last letter, and then slide the head so gathered one place along. That is freeCollapse_freeInsert_succ.

Both sides of the identity begin by collapsing the first k + 1 letters, so the whole statement reduces to the last two letters: absorbing a fresh head and inserting on the top letter is inserting on the penultimate letter and sliding. What is left is braiding bookkeeping around a single multiplication, organised here by the head swap — carrying a head factor past a block and landing it on the tail of that block. The interchange is a head swap under a head (tensorμ_headSwap), a head swap past a two-block splits into two head swaps (headSwap_tensor_block), and the slide window is itself a head swap followed by the action (freeSlideWin_eq). The two products are formed in the same order on both sides, so no commutativity is needed for the step.

Carrying a head past a block

The two-letter step

The normalisation step

theorem RS.freeCollapse_freeInsert_succ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (k : ℕ) : CategoryTheory.CategoryStruct.comp (freeCollapse A V (k + 2)) (freeInsert A V (k + 1)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (freeCollapse A V (k + 1)) (freeInsert A V k)) (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)) (freeSlideTop A V k)

The normalisation step: gathering every head of a word of free letters onto the last letter is gathering the heads of all but the last onto the penultimate letter and then sliding that head one place along.