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.