Noetherian objects

We shall say that an object X in a category C is Noetherian (type class IsNoetherianObject X) if the ordered type Subobject X satisfies the ascending chain condition. The corresponding property of objects isNoetherianObject : ObjectProperty C is always closed under subobjects.

Future works

• show that isNoetherian is a Serre class when C is an abelian category (TODO @joelriou)

def CategoryTheory.isNoetherianObject {C : Type u} [Category.{v, u} C] : ObjectProperty C

An object X in a category C is Noetherian if Subobject X satisfies the ascending chain condition. This definition is a term in ObjectProperty C which allows to study the stability properties of Noetherian objects. For statements regarding specific objects, it is advisable to use the type class IsNoetherianObject instead.

@[reducible, inline]

abbrev CategoryTheory.IsNoetherianObject {C : Type u} [Category.{v, u} C] (X : C) : Prop

An object X in a category C is Noetherian if Subobject X satisfies the ascending chain condition.

instance CategoryTheory.instWellFoundedGTSubobjectOfIsNoetherianObject {C : Type u} [Category.{v, u} C] (X : C) [IsNoetherianObject X] : WellFoundedGT (Subobject X)

theorem CategoryTheory.isNoetherianObject_iff_monotone_chain_condition {C : Type u} [Category.{v, u} C] (X : C) : IsNoetherianObject X ↔ ∀ (f : ℕ →o Subobject X), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m

theorem CategoryTheory.monotone_chain_condition_of_isNoetherianObject {C : Type u} [Category.{v, u} C] {X : C} [IsNoetherianObject X] (f : ℕ →o Subobject X) : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m

theorem CategoryTheory.isNoetherianObject_iff_not_strictMono {C : Type u} [Category.{v, u} C] (X : C) : IsNoetherianObject X ↔ ∀ (f : ℕ → Subobject X), ¬StrictMono f

theorem CategoryTheory.not_strictMono_of_isNoetherianObject {C : Type u} [Category.{v, u} C] {X : C} [IsNoetherianObject X] (f : ℕ → Subobject X) : ¬StrictMono f

theorem CategoryTheory.isNoetherianObject_iff_isEventuallyConstant {C : Type u} [Category.{v, u} C] (X : C) : IsNoetherianObject X ↔ ∀ (F : Functor ℕ (MonoOver X)), IsFiltered.IsEventuallyConstant F

theorem CategoryTheory.isEventuallyConstant_of_isNoetherianObject {C : Type u} [Category.{v, u} C] {X : C} [IsNoetherianObject X] (F : Functor ℕ (MonoOver X)) : IsFiltered.IsEventuallyConstant F

theorem CategoryTheory.isNoetherianObject_of_isZero {C : Type u} [Category.{v, u} C] {X : C} (hX : Limits.IsZero X) : IsNoetherianObject X

instance CategoryTheory.instContainsZeroIsNoetherianObjectOfHasZeroObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] : isNoetherianObject.ContainsZero

theorem CategoryTheory.isNoetherianObject_of_mono {C : Type u} [Category.{v, u} C] {X Y : C} (i : X ⟶ Y) [Mono i] [IsNoetherianObject Y] : IsNoetherianObject X

instance CategoryTheory.instIsClosedUnderSubobjectsIsNoetherianObject {C : Type u} [Category.{v, u} C] : isNoetherianObject.IsClosedUnderSubobjects