Nonvanishing of the splitting-chain units

The assembly of the Key Lemma's nonvanishing half: the chain unit stage is the copair element of the symmetric-power duality datum, up to the braiding of the module tensor product; so once the symmetric-power datum satisfies the zigzag laws, a vanishing stage unit kills the symmetric power. This is Deligne's argument: δⁿ is the δ of a duality between the symmetric powers (1.15.1), and the δ of a duality vanishes only on the zero module.

theorem RS.chainUnitStage_eq_symCopair {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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (n : ℕ) : chainUnitStage A M M' d n = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp (symDualityDatum A M M' d n).copair (modTensorSwap A (symPowMod A M.X n) (symPowMod A M'.X n)))

The chain unit stage is the symmetric copair element, up to the braiding of the module tensor product: Deligne's 1.15.1 composite.

theorem RS.chainUnitStage_ne_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.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') (n : ℕ) (hz : ModZigzagDatum A (symDualityDatum A M M' d n)) (hS : ¬CategoryTheory.Limits.IsZero (symPow A M.X (n + 1))) : chainUnitStage A M M' d n ≠ 0

Nonvanishing of the chain unit stages: once the symmetric-power datum satisfies the zigzag laws, the stage unit detects the symmetric power.

theorem RS.chainUnitStage_ne_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.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') (n : ℕ) (hz : ModZigzagDatum A (powDualityDatum A M M' d n)) (hS : ¬CategoryTheory.Limits.IsZero (symPow A M.X (n + 1))) : chainUnitStage A M M' d n ≠ 0

Nonvanishing from the power-level zigzags: composing the detection with the symmetric-power inheritance.