opaque CategoryTheory.loewyLength {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) : ℕ

The Loewy length of an object X in an abelian category: the length of the shortest filtration of X by semisimple subquotients, declared opaque here as an abstract handle.

def CategoryTheory.IsInCoradicalLayer {C : Type u} [Category.{v, u} C] [Abelian C] (i : ℕ) (X : C) : Prop

An object X lies in the i-th coradical layer of the socle/Loewy filtration when its Loewy length is at most i + 1.