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.

class CategoryTheory.NoetherianObject {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) : Prop

• 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

theorem CategoryTheory.NoetherianObject.subobject_gt_wellFounded {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) [CategoryTheory.NoetherianObject X] : WellFounded fun x x_1 => x > x_1

class CategoryTheory.ArtinianObject {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) : Prop

• 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

theorem CategoryTheory.ArtinianObject.subobject_lt_wellFounded {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) [CategoryTheory.ArtinianObject X] : WellFounded fun x x_1 => x < x_1

class CategoryTheory.Noetherian (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] extends CategoryTheory.EssentiallySmall : Prop

• equiv_smallCategory : ∃ S x, Nonempty (C ≌ S)
• noetherianObject : ∀ (X : C), CategoryTheory.NoetherianObject X

A category is noetherian if it is essentially small and all objects are noetherian.

class CategoryTheory.Artinian (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] extends CategoryTheory.EssentiallySmall : Prop

• equiv_smallCategory : ∃ S x, Nonempty (C ≌ S)
• artinianObject : ∀ (X : C), CategoryTheory.ArtinianObject X

A category is artinian if it is essentially small and all objects are artinian.

theorem CategoryTheory.exists_simple_subobject {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X : C} [CategoryTheory.ArtinianObject X] (h : ¬CategoryTheory.Limits.IsZero X) : ∃ Y, CategoryTheory.Simple (CategoryTheory.Subobject.underlying.obj Y)

noncomputable def CategoryTheory.simpleSubobject {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X : C} [CategoryTheory.ArtinianObject X] (h : ¬CategoryTheory.Limits.IsZero X) : C

Choose an arbitrary simple subobject of a non-zero artinian object.

noncomputable def CategoryTheory.simpleSubobjectArrow {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X : C} [CategoryTheory.ArtinianObject X] (h : ¬CategoryTheory.Limits.IsZero X) : CategoryTheory.simpleSubobject h ⟶ X

The monomorphism from the arbitrary simple subobject of a non-zero artinian object.

instance CategoryTheory.mono_simpleSubobjectArrow {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X : C} [CategoryTheory.ArtinianObject X] (h : ¬CategoryTheory.Limits.IsZero X) : CategoryTheory.Mono (CategoryTheory.simpleSubobjectArrow h)

instance CategoryTheory.instSimpleSimpleSubobject {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X : C} [CategoryTheory.ArtinianObject X] (h : ¬CategoryTheory.Limits.IsZero X) : CategoryTheory.Simple (CategoryTheory.simpleSubobject h)