The splitting algebra of the embedded category

The universal algebra of RS.exists_universal_algebra, taken over the family of all objects of the small category, splits the image of the Ind-embedding in the sense of RS.SplitsOn, and simultaneously splits every chosen epimorphism. These are exactly the two hypotheses under which the fibre functor over that algebra is strong monoidal and exact.

theorem RS.exists_splitting_algebra {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] [CategoryTheory.Limits.HasCoequalizers (CategoryTheory.Ind C)] [∀ (Z : CategoryTheory.Ind C), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Ind C)] (hu : HasScalarUnit C) (L : OddLine (CategoryTheory.Ind C)) {K : Type v} (V W : K → CategoryTheory.Ind C) (g : (k : K) → V k ⟶ W k) (hmix : ∀ (X : C), L.LocallyMixed (indOf.obj X)) (hsplit : ∀ (k : K), ∃ (A : CategoryTheory.Ind C) (x : CategoryTheory.MonObj A) (_ : CategoryTheory.IsCommMonObj A), CategoryTheory.MonObj.one ≠ 0 ∧ ∃ (s : freeMod A (W k) ⟶ freeMod A (V k)), CategoryTheory.CategoryStruct.comp s (freeModMap A (g k)) = CategoryTheory.CategoryStruct.id (freeMod A (W k))) : ∃ (𝔸 : CategoryTheory.Ind C) (x : CategoryTheory.MonObj 𝔸) (_ : CategoryTheory.IsCommMonObj 𝔸), CategoryTheory.MonObj.one ≠ 0 ∧ SplitsOn L 𝔸 indOf ∧ ∀ (k : K), ∃ (s : freeMod 𝔸 (W k) ⟶ freeMod 𝔸 (V k)), CategoryTheory.CategoryStruct.comp s (freeModMap 𝔸 (g k)) = CategoryTheory.CategoryStruct.id (freeMod 𝔸 (W k))

The splitting algebra: one nonzero commutative algebra that splits every embedded object into a mixed sum and splits every chosen epimorphism.