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.
Note: In the file, Mathlib/CategoryTheory/Subobject/ArtinianObject.lean,
it is shown 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.Noetherian
(C : Type u_1)
[Category.{v_1, u_1} C]
extends CategoryTheory.EssentiallySmall.{u_2, v_1, u_1} C :
A category is Noetherian if it is essentially small and all objects are Noetherian.
- equiv_smallCategory : ∃ (S : Type u_2) (x : SmallCategory S), Nonempty (C ≌ S)
- isNoetherianObject (X : C) : IsNoetherianObject X
Instances
class
CategoryTheory.Artinian
(C : Type u_1)
[Category.{v_1, u_1} C]
extends CategoryTheory.EssentiallySmall.{u_2, v_1, u_1} C :
A category is Artinian if it is essentially small and all objects are Artinian.
- equiv_smallCategory : ∃ (S : Type u_2) (x : SmallCategory S), Nonempty (C ≌ S)
- isArtinianObject (X : C) : IsArtinianObject X