Documentation

Mathlib.CategoryTheory.Noetherian

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.

source
@[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

Equations
Instances For
    source
    @[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

    Equations
    Instances For
      source
      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.

      Instances
        source
        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.

        Instances