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, Mathlib/CategoryTheory/Subobject/ArtinianObject.lean, 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.

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.

    Equations
    Instances For
      source
      class CategoryTheory.Noetherian (C : Type u_1) [Category.{v_1, u_1} C] extends CategoryTheory.EssentiallySmall.{u_2, v_1, 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.{v_1, u_1} C] extends CategoryTheory.EssentiallySmall.{u_2, v_1, u_1} C :
        Prop

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

        Instances