The relative power of a free module

Gathering every head of a word of free letters onto the last letter is invisible in the module power: one letter at a time, it is a slide, and a slide is a slot relation. So the descended collapse is an isomorphism modPow A (A ⊗ V) (n + 1) ≅ A ⊗ tensorPow D V (n + 1), and under it the descended group-algebra action becomes the ambient action under the head.

theorem RS.freeNormalise {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] (V : D) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (freeCollapse A V (n + 1)) (freeInsert A V n)) (modPowπ A (freeMod A V).X (n + 1)) = modPowπ A (freeMod A V).X (n + 1)

Normalisation: gathering every head onto the last letter is invisible in the module power.

noncomputable def RS.freeCollapseSection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (V : D) (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (tensorPow D V (n + 1)) ⟶ modPow A (freeMod A V).X (n + 1)

The section of the descended collapse: insert the head on the last letter and project.

Equations

• RS.freeCollapseSection A V n = CategoryTheory.CategoryStruct.comp (RS.freeInsert A V n) (RS.modPowπ A (RS.freeMod A V).X (n + 1))

theorem RS.freeCollapseSection_desc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) (n : ℕ) : CategoryTheory.CategoryStruct.comp (freeCollapseSection A V n) (freeCollapseDesc A V (n + 1)) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A (tensorPow D V (n + 1)))

The section retracts the descended collapse.

theorem RS.freeCollapseDesc_section {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) (n : ℕ) : CategoryTheory.CategoryStruct.comp (freeCollapseDesc A V (n + 1)) (freeCollapseSection A V n) = CategoryTheory.CategoryStruct.id (modPow A (freeMod A V).X (n + 1))

The descended collapse retracts the section.

theorem RS.freeModPow_alg {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) (n : ℕ) (z : SymGroupAlgebra (n + 1)) : CategoryTheory.CategoryStruct.comp (freeCollapseSection A V n) (CategoryTheory.CategoryStruct.comp ((modPowAlg A (freeMod A V).X (n + 1)) z) (freeCollapseDesc A V (n + 1))) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft A ((permAlg V (n + 1)) z)

The identification intertwines the two group-algebra actions.

theorem RS.whisker_permAlg_eq_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) (n : ℕ) (hn : n ≠ 0) (z : SymGroupAlgebra n) (h : (modPowAlg A (freeMod A V).X n) z = 0) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft A ((permAlg V n) z) = 0

Module-level vanishing gives whiskered ambient vanishing.

theorem RS.modPowAlg_eq_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) (n : ℕ) (hn : n ≠ 0) (z : SymGroupAlgebra n) (h : CategoryTheory.MonoidalCategoryStruct.whiskerLeft A ((permAlg V n) z) = 0) : (modPowAlg A (freeMod A V).X n) z = 0

Whiskered ambient vanishing gives module-level vanishing.