Commit 2022-05-12 08:45 7c4c90f4
View on Github →feat(category_theory/noetherian): nonzero artinian objects have simple subobjects (#13972)
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.