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} [Category.{u_2, u_1} C] (X : C) : Prop

A noetherian object is an object which does not have infinite increasing sequences of subobjects.

• subobject_gt_wellFounded' : WellFounded fun (x1 x2 : Subobject X) => x1 > x2

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

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

An artinian object is an object which does not have infinite decreasing sequences of subobjects.

• subobject_lt_wellFounded' : WellFounded fun (x1 x2 : Subobject X) => x1 < x2

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

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

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

• equiv_smallCategory : ∃ (S : Type u_3) (x : SmallCategory S), Nonempty (C ≌ S)
• noetherianObject (X : C) : NoetherianObject X

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

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

• equiv_smallCategory : ∃ (S : Type u_3) (x : SmallCategory S), Nonempty (C ≌ S)
• artinianObject (X : C) : ArtinianObject X

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

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

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

Equations

• CategoryTheory.simpleSubobject h = CategoryTheory.Subobject.underlying.obj ⋯.choose

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

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

Equations

• CategoryTheory.simpleSubobjectArrow h = ⋯.choose.arrow

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

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