Length bounded by the endomorphism dimension

In a ℂ-linear semisimple category with finite-dimensional Hom-spaces, the categorical length of an object is bounded by the dimension of its endomorphism algebra. Writing Y ≅ ⨁ S with the S i simple over Fin n, the biproduct of n simple objects has length at most n; and the n composites of a projection with the matching inclusion form pairwise-orthogonal nonzero idempotents in End Y, hence a linearly independent family, so that n ≤ dim End Y. Monotonicity of the length bound combines the two halves.

Length of a biproduct of simple objects

theorem RS.lengthLE_biproduct_of_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (S : Fin n → C) (hS : ∀ (i : Fin n), CategoryTheory.Simple (S i)) : LengthLE (⨁ S) n

A biproduct of n simple objects has length at most n.

Counting orthogonal idempotents

Reconciling independently supplied structures

A category may carry its preadditive and its abelian structure as independent instances — the envelope of the development does. The two then disagree on which zero-morphism structure to use, and a hypothesis stated over one does not typecheck against a lemma stated over the other. Zero-morphism structures are unique, so the abelian structure can be rebuilt over a prescribed preadditive one: everything abelianness adds beyond preadditivity is Prop-valued data that transports along that uniqueness.

The bound

theorem RS.lengthLE_finrank_end {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.Limits.HasFiniteBiproducts C] (hab : CategoryTheory.Abelian C) (hss : IsSemisimple C) (hfd : HasFinDimHom C) (Y : C) : LengthLE Y (Module.finrank ℂ (CategoryTheory.End Y))

Length is bounded by the endomorphism dimension: in a ℂ-linear semisimple category with finite-dimensional Hom-spaces, every object Y satisfies the length bound at dim End Y. The semisimplicity and finiteness hypotheses are read over the preadditive structure, and the abelian structure is rebuilt over it so that the two halves compose.