Length lower bounds from orthogonal idempotents

A family of pairwise-orthogonal nonzero idempotent endomorphisms of an object Y of an abelian category splits Y into as many nonzero pieces, so it bounds the composition length of Y from below. In the bound-shaped formulation of LengthLE (RS/Definitions.lean) this reads: k such endomorphisms together with LengthLE Y N force k ≤ N + 1.

The proof forms the partial sums E n = f 0 + ⋯ + f n, which are again idempotent by orthogonality, realises each as the subobject ker (𝟙 Y - E n), and shows the resulting chain is strictly increasing: a collapse of consecutive kernels would factor f (n + 1) through ker (𝟙 Y - E n), where it is annihilated by orthogonality, contradicting f (n + 1) ≠ 0.

theorem RS.le_of_orthogonal_idempotents {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {N k : ℕ} (hlen : LengthLE Y N) (f : Fin k → CategoryTheory.End Y) (hidem : ∀ (i : Fin k), f i * f i = f i) (horth : ∀ (i j : Fin k), i ≠ j → f i * f j = 0) (hne : ∀ (i : Fin k), f i ≠ 0) : k ≤ N + 1

Orthogonal idempotents bound length from below. In an abelian category, a family of k pairwise-orthogonal nonzero idempotent endomorphisms of Y forces the composition length of Y to be at least k; with the bound LengthLE Y N this reads k ≤ N + 1.