Artinian objects

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

Future works

• when C is an abelian category, relate IsArtinianObject in C with IsNoetherianObject in Cᵒᵖ.

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

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

Equations

• CategoryTheory.isArtinianObject X = WellFoundedLT (CategoryTheory.Subobject X)

@[reducible, inline]

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

An object X in a category C is Artinian if Subobject X satisfies the descending chain condition.

Equations

• CategoryTheory.IsArtinianObject X = CategoryTheory.isArtinianObject.Is X

instance CategoryTheory.instWellFoundedLTSubobjectOfIsArtinianObject {C : Type u} [Category.{v, u} C] (X : C) [IsArtinianObject X] : WellFoundedLT (Subobject X)

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

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

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

theorem CategoryTheory.not_strictAnti_of_isArtinianObject {C : Type u} [Category.{v, u} C] {X : C} [IsArtinianObject X] (f : ℕ → Subobject X) : ¬StrictAnti f

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

theorem CategoryTheory.isEventuallyConstant_of_isArtinianObject {C : Type u} [Category.{v, u} C] {X : C} [IsArtinianObject X] (F : Functor ℕ (MonoOver X)ᵒᵖ) : IsFiltered.IsEventuallyConstant F

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

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

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

instance CategoryTheory.instIsClosedUnderSubobjectsIsArtinianObject {C : Type u} [Category.{v, u} C] : isArtinianObject.IsClosedUnderSubobjects

theorem CategoryTheory.exists_simple_subobject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {X : C} [IsArtinianObject X] (h : ¬Limits.IsZero X) : ∃ (Y : Subobject X), Simple (Subobject.underlying.obj Y)

noncomputable def CategoryTheory.simpleSubobject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {X : C} [IsArtinianObject X] (h : ¬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} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {X : C} [IsArtinianObject X] (h : ¬Limits.IsZero X) : 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} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {X : C} [IsArtinianObject X] (h : ¬Limits.IsZero X) : Mono (simpleSubobjectArrow h)

instance CategoryTheory.instSimpleSimpleSubobject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {X : C} [IsArtinianObject X] (h : ¬Limits.IsZero X) : Simple (simpleSubobject h)