# mathlibdocumentation

category_theory.noetherian

# 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]
structure category_theory.noetherian_object {C : Type u_1} (X : C) :
Prop
• subobject_gt_well_founded :

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

Instances of this typeclass
@[class]
structure category_theory.artinian_object {C : Type u_1} (X : C) :
Prop
• subobject_lt_well_founded :

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

Instances of this typeclass
@[class]
structure category_theory.noetherian (C : Type u_1)  :
Type
• to_essentially_small :
• noetherian_object : ∀ (X : C),

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

Instances for category_theory.noetherian
• category_theory.noetherian.has_sizeof_inst
@[class]
structure category_theory.artinian (C : Type u_1)  :
Type
• to_essentially_small :
• artinian_object : ∀ (X : C),

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

Instances for category_theory.artinian
• category_theory.artinian.has_sizeof_inst
theorem category_theory.exists_simple_subobject {C : Type u_1} {X : C}  :
∃ (Y : ,
noncomputable def category_theory.simple_subobject {C : Type u_1} {X : C}  :
C

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

Equations
Instances for category_theory.simple_subobject
@[protected, instance]
noncomputable def category_theory.simple_subobject_arrow {C : Type u_1} {X : C}  :

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

Equations
Instances for category_theory.simple_subobject_arrow
@[protected, instance]