Symmetric powers of an odd twist

Twisting a module by the odd line exchanges the two halves of the trichotomy: the symmetric powers of the twist survive exactly when the alternating powers of the module do. In arity zero both are the tensor unit, so the exchange holds there too.

theorem RS.not_isZero_symPow_twist {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)] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (L : OddLine D) (R : CategoryTheory.Mod D A) (hA : ∀ (n : ℕ), ¬CategoryTheory.Limits.IsZero (altPow A R.X n)) (n : ℕ) : ¬CategoryTheory.Limits.IsZero (symPow A (tensorLeftMod A L.obj R).X n)

Surviving alternating powers become surviving symmetric powers after the odd twist.