Vanishing along the standard embeddings on module powers

The module-power mirror of Envelope/SymPermCast.lean: an element of the symmetric-group algebra whose descended action on the m-th module power vanishes keeps a vanishing action at every higher arity, along the standard embeddings S_m ↪ S_n.

The route is a descent reduction rather than a fresh induction. The projection modPowπ intertwines the ambient action permAlg with the descended action modPowAlg (modPowπ_permAlg), because the descended action is defined slot by slot through that very square; so vanishing of the descended action is exactly vanishing of the ambient action followed by the projection. The ambient compatibility permAlg_symCast rewrites the restricted action as a repeated whiskering, and one letter is attached to a module power by modPowAttach — the first concatenation stage of SymMul.lean taken at a single letter — whose defining square (modPowπ ▷ X) ≫ modPowAttach = modPowπ lets whiskered morphisms that die after the projection keep dying (whiskerRight_modPowπ_zero). The compatibility modPowAlg_compat follows.

Structural helpers

Attaching one letter to a module power

noncomputable def RS.modPowAttach {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (p : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modPow A X p) X ⟶ modPow A X (p + 1)

Attach one ambient letter on the right of a module power: the first concatenation stage of the multiplication of SymMul.lean, taken at a single letter.

Equations

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

theorem RS.modPowπ_attach {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (p : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X p) X) (modPowAttach A X p) = modPowπ A X (p + 1)

Defining square of the attachment: the projection at p + 1 factors through the right-whiskered projection at p.

theorem RS.whiskerRight_modPowπ_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] {p : ℕ} {f : tensorPow D X p ⟶ tensorPow D X p} (hf : CategoryTheory.CategoryStruct.comp f (modPowπ A X p) = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) (modPowπ A X (p + 1)) = 0

Whiskered vanishing: a morphism of the ambient power that dies after the projection keeps dying, one letter later, after whiskering on the right.

The compatibility

theorem RS.modPowπ_permAlg {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (n : ℕ) (x : SymGroupAlgebra n) : CategoryTheory.CategoryStruct.comp (modPowπ A X n) ((modPowAlg A X n) x) = CategoryTheory.CategoryStruct.comp ((permAlg X n) x) (modPowπ A X n)

The projection intertwines the two algebra actions: the ℂ-linear extension of the defining square of the descended permutation action.

theorem RS.whiskerPowAlg_modPowπ_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m k : ℕ) (f : tensorPow D X m ⟶ tensorPow D X m) (hf : CategoryTheory.CategoryStruct.comp f (modPowπ A X m) = 0) : CategoryTheory.CategoryStruct.comp ((whiskerPowAlg X m k) f) (modPowπ A X (m + k)) = 0

Iterated whiskered vanishing: an endomorphism of the ambient power that dies after the projection keeps dying after any number of letters is attached.

theorem RS.modPowAlg_compat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] {m n : ℕ} (h : m ≤ n) (x : SymGroupAlgebra m) (hx : (modPowAlg A X m) x = 0) : (modPowAlg A X n) ((symCast h) x) = 0

Vanishing propagates along the standard embeddings on module powers: an element of the group algebra killed by the descended action at arity m stays killed at every arity n ≥ m. This is the compat field of a tower, for the action on a module power.