The unit step of the dévissage

When every symmetric power of the remainder survives, the Key Lemma splits a unit factor off it: the splitting algebra becomes the new base, the complement becomes the new remainder, and the mixed free part gains one unit summand.

theorem RS.devissageStepA {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) : DevissageStepA (CategoryTheory.Ind C) L X

The unit step of the dévissage: when every symmetric power of the remainder survives, the Key Lemma splits a unit factor off it.