The splitting algebra of a Schur-killed category

Every object of a category all of whose objects are killed by some Schur functor is locally mixed after the Ind-embedding, and every short exact sequence splits after base change; so the universal algebra of RS.exists_splitting_algebra splits every embedded object and every embedded short exact sequence at once.

theorem RS.exists_fibre_algebra {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (P : SchurPackage) (P₀ : SchurPackage) (L : OddLine (CategoryTheory.Ind C)) (hkill : ∀ (Z : C), ∃ (lam : YoungDiagram), SchurKilled P Z lam) : ∃ (𝔸 : CategoryTheory.Ind C) (x : CategoryTheory.MonObj 𝔸) (_ : CategoryTheory.IsCommMonObj 𝔸), CategoryTheory.MonObj.one ≠ 0 ∧ SplitsOn L 𝔸 indOf ∧ ∀ (T : CategoryTheory.ShortComplex C), T.ShortExact → ∃ (s : freeMod 𝔸 (T.map indOf).X₃ ⟶ freeMod 𝔸 (T.map indOf).X₂), CategoryTheory.CategoryStruct.comp s (freeModMap 𝔸 (T.map indOf).g) = CategoryTheory.CategoryStruct.id (freeMod 𝔸 (T.map indOf).X₃)

The fibre algebra of a Schur-killed category.