The line step of the dévissage

When every alternating power of the remainder survives, twisting by the odd line turns them into surviving symmetric powers, so the unit step applies to the twisted state and splits a unit factor off it. Twisting back turns that unit factor into a line factor of the original state.

theorem RS.devissageStepB {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)] (L : OddLine (CategoryTheory.Ind C)) (X : CategoryTheory.Ind C) : DevissageStepB (CategoryTheory.Ind C) L X

The line step of the dévissage: when every alternating power of the remainder survives, a further line factor splits off it.