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.

We show that any nonzero artinian object has a simple subobject.

Future work #

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

A noetherian object is an object which does not have infinite increasing sequences of subobjects.

See https://stacks.math.columbia.edu/tag/0FCG

Instances

    An artinian object is an object which does not have infinite decreasing sequences of subobjects.

    See https://stacks.math.columbia.edu/tag/0FCF

    Instances

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

      Instances

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

        Instances

          Choose an arbitrary simple subobject of a non-zero artinian object.

          Equations
          Instances For

            The monomorphism from the arbitrary simple subobject of a non-zero artinian object.

            Equations
            Instances For