Bounded length for objects of an abelian category

A lightweight, bound-shaped notion of composition length (LengthLE, defined with the subquotient relation IsSubquotientOf in RS/Definitions.lean): an object Y satisfies LengthLE Y k when its subobject order admits no strictly increasing chain of k + 2 terms — exactly the predicate needed to state growth hypotheses, without committing to a composition-series formalism.

The elementary API, proved here: the bound is monotone, the predicate transfers along isomorphisms of the ambient object, zero objects have length at most 0, simple objects have length at most 1, and the bound is subadditive over binary biproducts.

theorem RS.LengthLE.mono {C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} {k k' : ℕ} (h : LengthLE Y k) (hk : k ≤ k') : LengthLE Y k'

The length bound is monotone: a bound at k is a bound at any k' ≥ k.

theorem RS.LengthLE.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {Y Z : C} (e : Y ≅ Z) {k : ℕ} (h : LengthLE Y k) : LengthLE Z k

The length bound transfers along an isomorphism of the ambient object, via the induced order isomorphism of subobject lattices.

theorem RS.lengthLE_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} (hY : CategoryTheory.Limits.IsZero Y) : LengthLE Y 0

A zero object has length at most 0: its subobject order is a singleton, so it carries no strictly increasing pair.

theorem RS.lengthLE_of_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} [CategoryTheory.Simple Y] : LengthLE Y 1

A simple object has length at most 1: its subobjects are only ⊥ and ⊤, so no chain has three distinct terms.

Splitting strict chains in a product order

Subadditivity over a binary biproduct

theorem RS.LengthLE.biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} {j k : ℕ} (hY : LengthLE Y j) (hZ : LengthLE Z k) : LengthLE (Y ⊞ Z) (j + k)

Subadditivity of the length bound over a binary biproduct: a strict chain of subobjects of Y ⊞ Z is traced by its parts over Y and its images in Z, and each strict step moves at least one of the two.