Jordan--Hölder filtrations from local finiteness #
The local-finiteness axiom controls intrinsic admissible subobjects in a normalized thin interval. In such an interval, admissible subobjects are exactly owner strict subobjects. Strict-Noetherian induction therefore finds a stable quotient of every nonzero same-phase object, and strict-Artinian induction iterates these quotients into an owner extension filtration.
No ordinary subobject is treated as admissible: every subobject constructed
below carries an explicit IsStrictMono witness, and all recursive steps use
the order on StrictSubobject.
theorem
CategoryTheory.Triangulated.Slicing.IsLocallyFinite.hasJordanHolderFiltrations
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
(hlocal : IsLocallyFinite C s)
:
Local finiteness supplies the same-phase Jordan--Hölder filtrations used by stable-object mass--Hom reduction.