Nonvanishing of the chain algebra unit

The unit of the splitting-chain algebra over the ind-category is nonzero: the finite-stage detection reduces vanishing to a chain unit stage, and the power zigzag induction keeps every stage alive.

theorem RS.chainBUnit_ne_zero {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (B : CategoryTheory.Ind C) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (N N' : CategoryTheory.Mod (CategoryTheory.Ind C) B) (d : ModDualityDatum B N N') (hz : ModZigzagDatum B d) (hS : ∀ (n : ℕ), ¬CategoryTheory.Limits.IsZero (symPow B N.X (n + 1))) : chainBUnit B N N' d ≠ 0

The unit of the splitting-chain algebra is nonzero: for a zigzag datum over the ind-category whose symmetric powers all survive, the unit of the algebra does not vanish.