The power zigzag induction

The successor power datum is the transfer of the tensor of the stage datum and the bottom datum along the merge isomorphism, so the zigzag laws climb the powers: the base is the arity-one transfer and the step is the tensor inheritance transferred along the merge.

theorem RS.powDualityDatum_succ {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') (n : ℕ) : powDualityDatum A M M' d (n + 1) = ModDualityDatum.transfer A (tensorDatum A (powDualityDatum A M M' d n) (powDualityDatum A M M' d 0)) (powFrontModInv A M.X n) (powBackModInv A M'.X n) (powFrontMod A M.X n) (powBackMod A M'.X n)

The successor power datum is the transferred tensor datum: the merge isomorphism carries the tensor of the stage datum and the bottom datum to the successor datum.

theorem RS.powDualityDatum_zigzag_all {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) (n : ℕ) : ModZigzagDatum A (powDualityDatum A M M' d n)

The power data satisfy the zigzag laws at every arity: the base is the arity-one transfer; the step transfers the tensor inheritance along the merge isomorphism.

theorem RS.chainUnitStage_ne_zero_all {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) [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) (n : ℕ) (hS : ¬CategoryTheory.Limits.IsZero (symPow A M.X (n + 1))) : chainUnitStage A M M' d n ≠ 0

Unconditional nonvanishing of the chain unit stages: for a zigzag datum with nonvanishing symmetric powers, every chain unit stage is nonzero.