The trichotomy, closed over a descent

The case analysis of the dévissage trichotomy: over any state, classically either all symmetric powers of the remainder survive, or all alternating powers survive, or some power of each dies — and then the Schur collapse and the power descent kill the remainder. The descent is a parameter, discharged by the sandwich retract.

theorem RS.antisymmetriser_one : antisymmetriser 1 = 1

The antisymmetriser at arity one is the identity.

theorem RS.antisymmetriser_zero : antisymmetriser 0 = 1

The antisymmetriser at arity zero is the identity.

theorem RS.isZero_of_isZero_symPowOne {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] [CategoryTheory.Linear ℂ D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (h : CategoryTheory.Limits.IsZero (symPow A X 1)) : CategoryTheory.Limits.IsZero X

A dead arity-one symmetric power kills the module.

theorem RS.isZero_of_isZero_altPow_one {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] [CategoryTheory.Linear ℂ D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (h : CategoryTheory.Limits.IsZero (altPow A X 1)) : CategoryTheory.Limits.IsZero X

A dead arity-one alternating power kills the module.

theorem RS.isZero_of_isZero_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (X : D) (h : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) : CategoryTheory.Limits.IsZero X

A dead tensor unit kills every object.

theorem RS.isZero_of_isZero_symPowZero {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] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (h : CategoryTheory.Limits.IsZero (symPow A X 0)) : CategoryTheory.Limits.IsZero X

A dead arity-zero symmetric power kills the module.

theorem RS.isZero_of_isZero_altPow_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] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (h : CategoryTheory.Limits.IsZero (altPow A X 0)) : CategoryTheory.Limits.IsZero X

A dead arity-zero alternating power kills the module.

theorem RS.devissageTrichotomy_of_descent {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.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (P : SchurPackage) (L : OddLine D) (X : D) (hdesc : ∀ (B : D) (x : CategoryTheory.MonObj B) (x_1 : CategoryTheory.IsCommMonObj B) (R R' : CategoryTheory.Mod D B) (d : ModDualityDatum B R R'), ModZigzagDatum B d → ∀ (k : ℕ), CategoryTheory.Limits.IsZero (modPow B R.X (k + 2)) → CategoryTheory.Limits.IsZero R.X) : DevissageTrichotomy D L X

The trichotomy holds over a power descent: classically, either all symmetric powers of the remainder survive, or all alternating powers survive, or the Schur collapse and the descent kill the remainder.