The scalars of a simple countably presented algebra are complex

The even part of the Γ-algebra of a simple algebra is a field, and a quotient of a countably presented ind-object is countably presented, so that field has countable dimension over the complex numbers. A field extension of the complex numbers of countable dimension is the complex numbers, so every scalar is a complex multiple of the unit.

Together with the vanishing of the odd part this is exactly the pair of hypotheses that RS/Classical/Deligne/FreeSummand.lean consumes: the free-module functor is then full and faithful on the mixed objects, and idempotents split with free image.

theorem RS.exists_smul_one_of_simple_of_epi {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (hu : HasScalarUnit C) (hsmul : IndOfLinear C) (hlen : ∀ (Z : C), ∃ (N : ℕ), LengthLE Z N) (L : OddLine (CategoryTheory.Ind C)) {𝔸 𝔹 : CategoryTheory.Ind C} [CategoryTheory.MonObj 𝔹] [CategoryTheory.IsCommMonObj 𝔹] (π : 𝔸 ⟶ 𝔹) [CategoryTheory.Epi π] (hcp : CountablyPresented 𝔸) (hne : CategoryTheory.MonObj.one ≠ 0) (hsimple : ∀ (I : CategoryTheory.Subobject 𝔹), IsIdeal 𝔹 I → I = ⊥ ∨ I = ⊤) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ 𝔹) : ∃ (c : ℂ), g = c • CategoryTheory.MonObj.one

The scalars of a simple countably presented algebra are the complex numbers. The algebra is presented as a quotient of a countably presented one, which is how the countable descent delivers it.