Documentation Verification Report

ArtinianObject

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

Statistics

Metric	Count
Definitions `IsArtinianObject`, `isArtinianObject`, `simpleSubobject`, `simpleSubobjectArrow`	4
Theorems `antitone_chain_condition_of_isArtinianObject`, `exists_simple_subobject`, `instContainsZeroIsArtinianObjectOfHasZeroObject`, `instIsClosedUnderSubobjectsIsArtinianObject`, `instSimpleSimpleSubobject`, `instWellFoundedLTSubobjectOfIsArtinianObject`, `isArtinianObject_iff_antitone_chain_condition`, `isArtinianObject_iff_isEventuallyConstant`, `isArtinianObject_iff_not_strictAnti`, `isArtinianObject_of_isZero`, `isArtinianObject_of_mono`, `isEventuallyConstant_of_isArtinianObject`, `mono_simpleSubobjectArrow`, `not_strictAnti_of_isArtinianObject`	14
Total	18

CategoryTheory

Definitions

Name	Category	Theorems
`IsArtinianObject` 📖	MathDef	6 math math: `isArtinianObject_iff_not_strictAnti`, `Artinian.isArtinianObject`, `isArtinianObject_iff_antitone_chain_condition`, `isArtinianObject_of_mono`, `isArtinianObject_of_isZero`, `isArtinianObject_iff_isEventuallyConstant`
`isArtinianObject` 📖	CompOp	2 math math: `instContainsZeroIsArtinianObjectOfHasZeroObject`, `instIsClosedUnderSubobjectsIsArtinianObject`
`simpleSubobject` 📖	CompOp	2 math math: `instSimpleSimpleSubobject`, `mono_simpleSubobjectArrow`
`simpleSubobjectArrow` 📖	CompOp	1 math math: `mono_simpleSubobjectArrow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_chain_condition_of_isArtinianObject` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `OrderDual` `Subobject` `Nat.instPreorder` `OrderDual.instPreorder` `PartialOrder.toPreorder` `instPartialOrderSubobject` `OrderHom.instFunLike`	—	`isArtinianObject_iff_antitone_chain_condition`
`exists_simple_subobject` 📖	mathematical	`Limits.IsZero`	`Simple` `Functor.obj` `Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `instPartialOrderSubobject` `Subobject.underlying`	—	`Subobject.nontrivial_of_not_isZero` `Limits.HasZeroObject.hasInitial` `Limits.HasZeroObject.initialMonoClass` `IsAtomic.eq_bot_or_exists_atom_le` `IsStronglyAtomic.isAtomic` `instIsStronglyAtomicOfWellFoundedLT` `instWellFoundedLTSubobjectOfIsArtinianObject` `top_ne_bot` `subobject_simple_iff_isAtom`
`instContainsZeroIsArtinianObjectOfHasZeroObject` 📖	mathematical	—	`ObjectProperty.ContainsZero` `isArtinianObject`	—	`Limits.isZero_zero` `ObjectProperty.is_iff` `isArtinianObject_of_isZero`
`instIsClosedUnderSubobjectsIsArtinianObject` 📖	mathematical	—	`ObjectProperty.IsClosedUnderSubobjects` `isArtinianObject`	—	`ObjectProperty.is_iff` `isArtinianObject_of_mono`
`instSimpleSimpleSubobject` 📖	mathematical	`Limits.IsZero`	`Simple` `simpleSubobject`	—	`exists_simple_subobject`
`instWellFoundedLTSubobjectOfIsArtinianObject` 📖	mathematical	—	`WellFoundedLT` `Subobject` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderSubobject`	—	`ObjectProperty.prop_of_is`
`isArtinianObject_iff_antitone_chain_condition` 📖	mathematical	—	`IsArtinianObject` `DFunLike.coe` `OrderHom` `OrderDual` `Subobject` `Nat.instPreorder` `OrderDual.instPreorder` `PartialOrder.toPreorder` `instPartialOrderSubobject` `OrderHom.instFunLike`	—	`ObjectProperty.is_iff` `isArtinianObject.eq_1` `wellFoundedGT_dual_iff` `wellFoundedGT_iff_monotone_chain_condition`
`isArtinianObject_iff_isEventuallyConstant` 📖	mathematical	—	`IsArtinianObject` `IsFiltered.IsEventuallyConstant` `Opposite` `MonoOver` `Preorder.smallCategory` `Nat.instPreorder` `Category.opposite` `ObjectProperty.FullSubcategory.category` `Over` `instCategoryOver` `Over.isMono`	—	`isArtinianObject_iff_antitone_chain_condition` `Functor.monotone` `isIso_unop_iff` `MonoOver.mono` `MonoOver.isIso_iff_subobjectMk_eq` `leOfHom` `OrderHom.monotone` `reflectsIsomorphisms_of_full_and_faithful` `Functor.IsEquivalence.full` `Subobject.instIsEquivalenceMonoOverRepresentative` `Functor.IsEquivalence.faithful` `EquivLike.toEmbeddingLike`
`isArtinianObject_iff_not_strictAnti` 📖	mathematical	—	`IsArtinianObject` `StrictAnti` `Subobject` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderSubobject`	—	`not_strictAnti_of_wellFoundedLT` `instWellFoundedLTSubobjectOfIsArtinianObject` `ObjectProperty.is_iff` `isArtinianObject.eq_1` `WellFoundedLT.eq_1` `isWellFounded_iff` `RelEmbedding.wellFounded_iff_isEmpty` `instIsStrictOrderLt` `RelEmbedding.map_rel_iff`
`isArtinianObject_of_isZero` 📖	mathematical	`Limits.IsZero`	`IsArtinianObject`	—	`isArtinianObject_iff_antitone_chain_condition` `Subobject.subsingleton_of_isZero` `OrderDual.instSubsingleton`
`isArtinianObject_of_mono` 📖	mathematical	—	`IsArtinianObject`	—	`isArtinianObject_iff_antitone_chain_condition` `Functor.monotone` `OrderHom.monotone'` `antitone_chain_condition_of_isArtinianObject` `Subobject.map_obj_injective`
`isEventuallyConstant_of_isArtinianObject` 📖	mathematical	—	`IsFiltered.IsEventuallyConstant` `Opposite` `MonoOver` `Preorder.smallCategory` `Nat.instPreorder` `Category.opposite` `ObjectProperty.FullSubcategory.category` `Over` `instCategoryOver` `Over.isMono`	—	`isArtinianObject_iff_isEventuallyConstant`
`mono_simpleSubobjectArrow` 📖	mathematical	`Limits.IsZero`	`Mono` `simpleSubobject` `simpleSubobjectArrow`	—	`exists_simple_subobject` `Subobject.arrow_mono`
`not_strictAnti_of_isArtinianObject` 📖	mathematical	—	`StrictAnti` `Subobject` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderSubobject`	—	`isArtinianObject_iff_not_strictAnti`

---

← Back to Index