NoetherianObject

📁 Source: Mathlib/CategoryTheory/Subobject/NoetherianObject.lean

Statistics

Metric	Count
Definitions IsNoetherianObject, isNoetherianObject	2
Theorems instContainsZeroIsNoetherianObjectOfHasZeroObject, instIsClosedUnderSubobjectsIsNoetherianObject, instWellFoundedGTSubobjectOfIsNoetherianObject, isEventuallyConstant_of_isNoetherianObject, isNoetherianObject_iff_isEventuallyConstant, isNoetherianObject_iff_monotone_chain_condition, isNoetherianObject_iff_not_strictMono, isNoetherianObject_of_isZero, isNoetherianObject_of_mono, monotone_chain_condition_of_isNoetherianObject, not_strictMono_of_isNoetherianObject	11
Total	13

CategoryTheory

Definitions

Name	Category	Theorems
IsNoetherianObject 📖	MathDef	6 math math: isNoetherianObject_iff_monotone_chain_condition, isNoetherianObject_of_isZero, isNoetherianObject_of_mono, Noetherian.isNoetherianObject, isNoetherianObject_iff_not_strictMono, isNoetherianObject_iff_isEventuallyConstant
isNoetherianObject 📖	CompOp	2 math math: instIsClosedUnderSubobjectsIsNoetherianObject, instContainsZeroIsNoetherianObjectOfHasZeroObject

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContainsZeroIsNoetherianObjectOfHasZeroObject 📖	mathematical	—	ObjectProperty.ContainsZero isNoetherianObject	—	Limits.isZero_zero ObjectProperty.is_iff isNoetherianObject_of_isZero
instIsClosedUnderSubobjectsIsNoetherianObject 📖	mathematical	—	ObjectProperty.IsClosedUnderSubobjects isNoetherianObject	—	ObjectProperty.is_iff isNoetherianObject_of_mono
instWellFoundedGTSubobjectOfIsNoetherianObject 📖	mathematical	—	WellFoundedGT Subobject Preorder.toLT PartialOrder.toPreorder instPartialOrderSubobject	—	ObjectProperty.prop_of_is
isEventuallyConstant_of_isNoetherianObject 📖	mathematical	—	IsFiltered.IsEventuallyConstant MonoOver Preorder.smallCategory Nat.instPreorder ObjectProperty.FullSubcategory.category Over instCategoryOver Over.isMono	—	isNoetherianObject_iff_isEventuallyConstant
isNoetherianObject_iff_isEventuallyConstant 📖	mathematical	—	IsNoetherianObject IsFiltered.IsEventuallyConstant MonoOver Preorder.smallCategory Nat.instPreorder ObjectProperty.FullSubcategory.category Over instCategoryOver Over.isMono	—	isNoetherianObject_iff_monotone_chain_condition MonoOver.mono MonoOver.isIso_iff_subobjectMk_eq leOfHom OrderHom.monotone reflectsIsomorphisms_of_full_and_faithful Functor.IsEquivalence.full Subobject.instIsEquivalenceMonoOverRepresentative Functor.IsEquivalence.faithful
isNoetherianObject_iff_monotone_chain_condition 📖	mathematical	—	IsNoetherianObject DFunLike.coe OrderHom Subobject Nat.instPreorder PartialOrder.toPreorder instPartialOrderSubobject OrderHom.instFunLike	—	ObjectProperty.is_iff isNoetherianObject.eq_1 wellFoundedGT_iff_monotone_chain_condition
isNoetherianObject_iff_not_strictMono 📖	mathematical	—	IsNoetherianObject StrictMono Subobject Nat.instPreorder PartialOrder.toPreorder instPartialOrderSubobject	—	not_strictMono_of_wellFoundedGT instWellFoundedGTSubobjectOfIsNoetherianObject ObjectProperty.is_iff isNoetherianObject.eq_1 WellFoundedGT.eq_1 isWellFounded_iff RelEmbedding.wellFounded_iff_isEmpty instIsStrictOrderGt RelEmbedding.map_rel_iff
isNoetherianObject_of_isZero 📖	mathematical	Limits.IsZero	IsNoetherianObject	—	isNoetherianObject_iff_monotone_chain_condition Subobject.subsingleton_of_isZero
isNoetherianObject_of_mono 📖	mathematical	—	IsNoetherianObject	—	isNoetherianObject_iff_monotone_chain_condition Monotone.comp Functor.monotone OrderHom.monotone' monotone_chain_condition_of_isNoetherianObject Subobject.map_obj_injective
monotone_chain_condition_of_isNoetherianObject 📖	mathematical	—	DFunLike.coe OrderHom Subobject Nat.instPreorder PartialOrder.toPreorder instPartialOrderSubobject OrderHom.instFunLike	—	isNoetherianObject_iff_monotone_chain_condition
not_strictMono_of_isNoetherianObject 📖	mathematical	—	StrictMono Subobject Nat.instPreorder PartialOrder.toPreorder instPartialOrderSubobject	—	isNoetherianObject_iff_not_strictMono

---

← Back to Index