A section of the free collapse

The free collapse freeCollapse A V n of Deligne/FreePow.lean multiplies the heads of a word of free letters A ⊗ V to the front of the word. From arity one upwards it is a split epimorphism: the section carries the head of A ⊗ V ^ ⊗ n into the topmost letter and fills every other letter with the unit of A.

The bookkeeping is carried by two auxiliary constructions. The unit word is the empty product of units in a monoid power; folding it returns the unit, by the left unit law alone. The unit power inserts the unit into every letter of an ambient power; shuffling it separates the unit word from the ambient word. With those two in hand the composite of the insertion and the collapse is a symmetric-monoidal identity: the braiding introduced by the insertion cancels the braiding hidden inside the middle-four interchange, and the folded unit word contributes only a left unitor.

Unit words and unit-filled powers

noncomputable def RS.unitWord {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ tensorPow D A n

The unit word: the empty product of units in an ambient power.

Equations

• One or more equations did not get rendered due to their size.
• RS.unitWord A 0 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

@[simp]

theorem RS.unitWord_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] : unitWord A 0 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

noncomputable def RS.freeUnitPow {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (n : ℕ) : tensorPow D V n ⟶ tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) n

Insert the monoid unit into every letter of an ambient power.

Equations

• One or more equations did not get rendered due to their size.
• RS.freeUnitPow A V 0 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

@[simp]

theorem RS.unitPow_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) : freeUnitPow A V 0 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

theorem RS.unitWord_muFold {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (n : ℕ) : CategoryTheory.CategoryStruct.comp (unitWord A n) (muFold A n) = CategoryTheory.MonObj.one

Folding a word of units gives the unit.

The unit power through the shuffle

theorem RS.unitPow_plainShuffle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (n : ℕ) : CategoryTheory.CategoryStruct.comp (freeUnitPow A V n) (plainShuffle A V n).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (tensorPow D V n)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (unitWord A n) (tensorPow D V n))

Shuffling a word of unit-filled letters separates the unit word from the ambient word.

The free insertion

noncomputable def RS.freeInsert {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (tensorPow D V (n + 1)) ⟶ tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) (n + 1)

The free insertion: carry the head into the top letter of the word and fill every other letter with the unit.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.freeInsert_freeCollapse {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (n : ℕ) : CategoryTheory.CategoryStruct.comp (freeInsert A V n) (freeCollapse A V (n + 1)) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A (tensorPow D V (n + 1)))

The free insertion is a section of the free collapse.