Artinian and noetherian categories

An artinian category is a category in which objects do not have infinite decreasing sequences of subobjects.

A noetherian category is a category in which objects do not have infinite increasing sequences of subobjects.

Note: In the file, CategoryTheory.Subobject.ArtinianObject, it is shown that any nonzero Artinian object has a simple subobject.

Future work

The Jordan-Hölder theorem, following https://stacks.math.columbia.edu/tag/0FCK.

@[deprecated CategoryTheory.IsNoetherianObject (since := "2025-07-11")]

def CategoryTheory.NoetherianObject {C : Type u} [Category.{v, u} C] (X : C) : Prop

Alias of CategoryTheory.IsNoetherianObject.

---

An object X in a category C is Noetherian if Subobject X satisfies the ascending chain condition.

Stacks Tag 0FCG

@[deprecated CategoryTheory.IsArtinianObject (since := "2025-07-11")]

def CategoryTheory.ArtinianObject {C : Type u} [Category.{v, u} C] (X : C) : Prop

Alias of CategoryTheory.IsArtinianObject.

---

An object X in a category C is Artinian if Subobject X satisfies the descending chain condition.

Stacks Tag 0FCF

class CategoryTheory.Noetherian (C : Type u_1) [Category.{u_2, u_1} C] extends CategoryTheory.EssentiallySmall.{u_3, u_2, u_1} C : Prop

A category is noetherian if it is essentially small and all objects are noetherian.

• equiv_smallCategory : ∃ (S : Type u_3) (x : SmallCategory S), Nonempty (C ≌ S)
• isNoetherianObject (X : C) : IsNoetherianObject X

class CategoryTheory.Artinian (C : Type u_1) [Category.{u_2, u_1} C] extends CategoryTheory.EssentiallySmall.{u_3, u_2, u_1} C : Prop

A category is artinian if it is essentially small and all objects are artinian.

• equiv_smallCategory : ∃ (S : Type u_3) (x : SmallCategory S), Nonempty (C ≌ S)
• isArtinianObject (X : C) : IsArtinianObject X