The splitting algebra of the doubling

A tensor category need not contain an odd line; the ℤ/2-graded doubling always does. Every hypothesis passes to the doubling — scalar unit endomorphisms, moderate length growth, finite tensor generation, and finite length of every object — so the single simple algebra that splits the doubling is available, together with the complex point of its Γ-algebra.

theorem RS.exists_splitting_simple_algebra_doubled {A : Type v} [CategoryTheory.SmallCategory A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Abelian A] [CategoryTheory.RigidCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.Limits.HasFiniteBiproducts A] (P : SchurPackage) (P₀ : SchurPackage) (hu : HasScalarUnit A) (X : A) (hgen : TensorGeneratedBy A X) (hgrow : ModerateLengthGrowth A) : ∃ (𝔹 : CategoryTheory.Ind (Doubled A)) (x : CategoryTheory.MonObj 𝔹) (x_1 : CategoryTheory.IsCommMonObj 𝔹), CategoryTheory.MonObj.one ≠ 0 ∧ (∀ (I : CategoryTheory.Subobject 𝔹), IsIdeal 𝔹 I → I = ⊥ ∨ I = ⊤) ∧ SplitsOn doubledIndOddLine 𝔹 indOf ∧ Nonempty (SuperPoint (gammaAlgebra (CategoryTheory.Ind (Doubled A)) doubledIndOddLine 𝔹))

The splitting algebra of the doubling. Everything the argument needs passes to Doubled A, so one simple algebra splits every embedded object of the doubling and its Γ-algebra has a complex point.