Nonvanishing detection from the zigzag laws

The general engine behind every stage-unit nonvanishing argument in the Key Lemma: for a duality datum satisfying the zigzag laws, the copair element detects nonvanishing of the module. If the element η ≫ copair vanishes then the zig composite vanishes, yet the zigzag law says it is the identity of the single-factor multi-tensor, which is therefore zero — and so is the module.

This is the open-diagram detection: it consumes the triangle identity, never the loop composite, so it is uniform in the categorical dimension of the module. Applied to the power, symmetric-power and chain-stage data it yields the stage units' nonvanishing exactly from the nonvanishing of the corresponding power objects.

theorem RS.isZero_of_unit_copair_eq_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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) (h0 : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d.copair = 0) : CategoryTheory.Limits.IsZero M.X

If the copair element vanishes, so does the module: the zig composite factors through the copair element, and the zigzag law makes it the identity.

theorem RS.unit_copair_ne_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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) (hM : ¬CategoryTheory.Limits.IsZero M.X) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d.copair ≠ 0

The copair element detects nonvanishing: over a zigzag datum for a nonzero module, the copair element is nonzero. This is the open-diagram stage-unit detection of the Key Lemma.