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.

source
@[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
source
@[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
source
@[class]
structure category_theory.noetherian (C : Type u_1) [category_theory.category C] :
Type

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
source
@[class]
structure category_theory.artinian (C : Type u_1) [category_theory.category C] :
Type

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
source
theorem category_theory.exists_simple_subobject {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_zero_object C] {X : C} [category_theory.artinian_object X] (h : ¬category_theory.limits.is_zero X) :
∃ (Y : category_theory.subobject X), category_theory.simple ↑Y
source
noncomputable def category_theory.simple_subobject {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_zero_object C] {X : C} [category_theory.artinian_object X] (h : ¬category_theory.limits.is_zero X) :
C

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

Equations
Instances for category_theory.simple_subobject
source
@[protected, instance]
def category_theory.simple_subobject_arrow.mono {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_zero_object C] {X : C} [category_theory.artinian_object X] (h : ¬category_theory.limits.is_zero X) :
category_theory.mono (category_theory.simple_subobject_arrow h)
source
noncomputable def category_theory.simple_subobject_arrow {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_zero_object C] {X : C} [category_theory.artinian_object X] (h : ¬category_theory.limits.is_zero X) :
category_theory.simple_subobject h ⟶ X

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

Equations
Instances for category_theory.simple_subobject_arrow
source
@[protected, instance]
def category_theory.simple_subobject.simple {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_zero_object C] {X : C} [category_theory.artinian_object X] (h : ¬category_theory.limits.is_zero X) :
category_theory.simple (category_theory.simple_subobject h)