mathlib3 documentation

category_theory.noetherian

Artinian and noetherian categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [category_theory.category 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

Instances of this typeclass
@[class]
structure category_theory.artinian_object {C : Type u_1} [category_theory.category 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

Instances of this typeclass
@[class]

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]

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

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

Equations
Instances for category_theory.simple_subobject

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

Equations
Instances for category_theory.simple_subobject_arrow