The collapse against the group-algebra action

Permutation equivariance of the free collapse extends linearly to the whole symmetric-group algebra: the action on a word of free letters becomes, after collapsing the heads, the action on the ambient word under the head.

theorem RS.freeCollapse_permAlg {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) (n : ℕ) (z : SymGroupAlgebra n) : CategoryTheory.CategoryStruct.comp ((permAlg (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) n) z) (freeCollapse A V n) = CategoryTheory.CategoryStruct.comp (freeCollapse A V n) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A ((permAlg V n) z))

Equivariance of the collapse for the group algebra.