A simple algebra splitting the tensor generator

Composing the two halves: the splitting algebra of a single object is countably presented, and every nonzero algebra object has a simple quotient. Base change carries the splitting down, so a single simple algebra splits the chosen object.

Over a simple algebra the regular module is a simple object of the module category, and so is its twist by the odd line, so a free mixed module is semisimple of finite length. That is what will carry the splitting from the tensor generator to every subquotient, and with it to the whole category.

theorem RS.exists_simple_generator_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)) (X₀ : C) (lam : YoungDiagram) (hkill : SchurKilled P X₀ lam) (hlen : ∀ (Z : C), ∃ (N : ℕ), LengthLE Z N) : ∃ (p : ℕ) (q : ℕ) (𝔸 : CategoryTheory.Ind C) (𝔹 : CategoryTheory.Ind C) (x : CategoryTheory.MonObj 𝔸) (_ : CategoryTheory.IsCommMonObj 𝔸) (x_2 : CategoryTheory.MonObj 𝔹) (_ : CategoryTheory.IsCommMonObj 𝔹) (π : 𝔸 ⟶ 𝔹), CategoryTheory.MonObj.one ≠ 0 ∧ CountablyPresented 𝔸 ∧ CategoryTheory.Epi π ∧ CategoryTheory.IsMonHom π ∧ (∀ (I : CategoryTheory.Subobject 𝔹), IsIdeal 𝔹 I → I = ⊥ ∨ I = ⊤) ∧ Nonempty (freeMod 𝔹 (indOf.obj X₀) ≅ freeMod 𝔹 (L.mix p q))

A simple algebra splitting a chosen object, obtained from a countably presented splitting algebra by passing to the quotient by a maximal ideal. The countably presented algebra above is kept, together with the projection, because the dimension count for the scalars of the quotient runs through it.