mathlib

7c4c90f4 - feat(category_theory/noetherian): nonzero artinian objects have simple subobjects (#13972)

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>