Commit 2025-03-16 16:36 3ef10a6f

View on Github →

feat(CategoryTheory): Noetherian objects (#22373) An object X in a category C is Noetherian if the ordered type Subobject X satisfies the ascending chain condition. In this PR, we show that this property is closed under subobjects. (In a future PR, it shall be shown that if C is an abelian category, then this is a Serre class.)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Category/Preorder.lean

added theorem PartialOrder.isIso_iff_eq

Modified Mathlib/CategoryTheory/ObjectProperty/Basic.lean

added theorem CategoryTheory.ObjectProperty.is_of_prop

added theorem CategoryTheory.ObjectProperty.prop_of_is

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

added theorem CategoryTheory.MonoOver.isIso_iff_subobjectMk_eq

added theorem CategoryTheory.MonoOver.isIso_left_iff_subobjectMk_eq

modified theorem CategoryTheory.MonoOver.subobjectMk_le_mk_of_hom

Modified Mathlib/CategoryTheory/Subobject/Lattice.lean

added theorem CategoryTheory.Subobject.subsingleton_of_isInitial

added theorem CategoryTheory.Subobject.subsingleton_of_isZero

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

added theorem CategoryTheory.MonoOver.isIso_iff_isIso_left

Created Mathlib/CategoryTheory/Subobject/NoetherianObject.lean

added theorem CategoryTheory.isEventuallyConstant_of_isNoetherianObject

added def CategoryTheory.isNoetherianObject

added theorem CategoryTheory.isNoetherianObject_iff_isEventuallyConstant

added theorem CategoryTheory.isNoetherianObject_iff_monotone_chain_condition

added theorem CategoryTheory.isNoetherianObject_iff_not_strictMono

added theorem CategoryTheory.isNoetherianObject_of_isZero

added theorem CategoryTheory.isNoetherianObject_of_mono

added theorem CategoryTheory.monotone_chain_condition_of_isNoetherianObject

added theorem CategoryTheory.not_strictMono_of_isNoetherianObject