# 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.

class CategoryTheory.NoetherianObject {C : Type u_1} [] (X : C) :
• subobject_gt_wellFounded' : WellFounded fun x x_1 => x > x_1

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

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

Instances
theorem CategoryTheory.NoetherianObject.subobject_gt_wellFounded {C : Type u_1} [] (X : C) :
WellFounded fun x x_1 => x > x_1
class CategoryTheory.ArtinianObject {C : Type u_1} [] (X : C) :
• subobject_lt_wellFounded' : WellFounded fun x x_1 => x < x_1

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

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

Instances
theorem CategoryTheory.ArtinianObject.subobject_lt_wellFounded {C : Type u_1} [] (X : C) :
WellFounded fun x x_1 => x < x_1
class CategoryTheory.Noetherian (C : Type u_1) [] extends :
• equiv_smallCategory : S x, Nonempty (C S)
• noetherianObject : ∀ (X : C),

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

Instances
class CategoryTheory.Artinian (C : Type u_1) [] extends :
• equiv_smallCategory : S x, Nonempty (C S)
• artinianObject : ∀ (X : C),

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

Instances
theorem CategoryTheory.exists_simple_subobject {C : Type u_1} [] {X : C} :
Y, CategoryTheory.Simple (CategoryTheory.Subobject.underlying.obj Y)
noncomputable def CategoryTheory.simpleSubobject {C : Type u_1} [] {X : C} :
C

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

Instances For
noncomputable def CategoryTheory.simpleSubobjectArrow {C : Type u_1} [] {X : C} :

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

Instances For