# 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) :

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

• subobject_gt_wellFounded' : WellFounded fun (x x_1 : ) => x > x_1
Instances
theorem CategoryTheory.NoetherianObject.subobject_gt_wellFounded' {C : Type u_1} [] {X : C} [self : ] :
WellFounded fun (x x_1 : ) => x > x_1
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) :

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

• subobject_lt_wellFounded' : WellFounded fun (x x_1 : ) => x < x_1
Instances
theorem CategoryTheory.ArtinianObject.subobject_lt_wellFounded' {C : Type u_1} [] {X : C} [self : ] :
WellFounded fun (x x_1 : ) => x < x_1
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 :

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

• equiv_smallCategory : ∃ (S : Type u_3) (x : ), Nonempty (C S)
• noetherianObject : ∀ (X : C),
Instances
theorem CategoryTheory.Noetherian.noetherianObject {C : Type u_1} [] [self : ] (X : C) :
class CategoryTheory.Artinian (C : Type u_1) [] extends :

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

• equiv_smallCategory : ∃ (S : Type u_3) (x : ), Nonempty (C S)
• artinianObject : ∀ (X : C),
Instances
theorem CategoryTheory.Artinian.artinianObject {C : Type u_1} [] [self : ] (X : C) :
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.

Equations
• = CategoryTheory.Subobject.underlying.obj .choose
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.

Equations
• = .choose.arrow
Instances For
Equations
• =
Equations
• =