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

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

See https://stacks.math.columbia.edu/tag/0FCG

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

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

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

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

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

See https://stacks.math.columbia.edu/tag/0FCF

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

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

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

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

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

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

theorem CategoryTheory.Noetherian.noetherianObject {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} [self : CategoryTheory.Noetherian C] (X : C), CategoryTheory.NoetherianObject X

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

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

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

theorem CategoryTheory.Artinian.artinianObject {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} [self : CategoryTheory.Artinian C] (X : C), CategoryTheory.ArtinianObject X

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.Subobject X), 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.

Equations

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

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.

Equations

• CategoryTheory.simpleSubobjectArrow h = ⋯.choose.arrow

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯