The universal algebra of Deligne 2.11

Choosing, for every object, an algebra over which it becomes a mixed sum, and for every short exact sequence an algebra over which it splits, and taking the tensor product of all of them, gives a single nonzero algebra over which every object is a mixed sum and every short exact sequence splits.

theorem RS.exists_universal_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)) {J K : Type v} (X : J → CategoryTheory.Ind C) (V W : K → CategoryTheory.Ind C) (g : (k : K) → V k ⟶ W k) (hmix : ∀ (j : J), L.LocallyMixed (X j)) (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 ∧ (∀ (j : J), ∃ (p : ℕ) (q : ℕ), Nonempty (freeMod 𝔸 (X j) ≅ freeMod 𝔸 (L.mix p q))) ∧ ∀ (k : K), ∃ (s : freeMod 𝔸 (W k) ⟶ freeMod 𝔸 (V k)), CategoryTheory.CategoryStruct.comp s (freeModMap 𝔸 (g k)) = CategoryTheory.CategoryStruct.id (freeMod 𝔸 (W k))

The universal algebra: one nonzero algebra over which every object of the family becomes a mixed sum and every chosen morphism acquires a section.