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.
- 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
- 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
- noetherianObject : ∀ (X : C), CategoryTheory.NoetherianObject X
A category is noetherian if it is essentially small and all objects are noetherian.
Instances
- artinianObject : ∀ (X : C), CategoryTheory.ArtinianObject X
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.
Instances For
The monomorphism from the arbitrary simple subobject of a non-zero artinian object.