The power descent, unconditionally

Over a zigzag datum the sandwich retract exists, so vanishing of a relative tensor power descends to the module itself.

theorem RS.isZero_of_isZero_modPow {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.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) (k : ℕ) (h : CategoryTheory.Limits.IsZero (modPow A M.X (k + 2))) : CategoryTheory.Limits.IsZero M.X

Power vanishing descends to the module (Deligne 2.9, case (c), object half): over a duality datum with the zigzag laws, a module whose (k + 2)-nd relative power vanishes is zero.

theorem RS.devissageTrichotomy {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.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (P : SchurPackage) (L : OddLine D) (X : D) : DevissageTrichotomy D L X

The dévissage trichotomy (Deligne 2.9, the case analysis): over any state, either every symmetric power of the remainder survives, or every alternating power survives, or the remainder is zero.