Documentation Verification Report

EssentiallySmall

📁 Source: Mathlib/CategoryTheory/Limits/EssentiallySmall.lean

Statistics

Metric	Count
Definitions `EssentiallySmall`, `EssentiallySmall`	2
Theorems `hasColimitsOfShape_of_essentiallySmall`, `hasCoproductsOfShape_of_small`, `hasLimitsOfShape_of_essentiallySmall`, `hasProductsOfShape_of_small`	4
Total	6

CategoryTheory

Definitions

Name	Category	Theorems
`EssentiallySmall` 📖	CompData	25 math math: `instEssentiallySmallFGAlgCat`, `instEssentiallySmallFGModuleCat`, `EssentiallySmall.mk'`, `instEssentiallySmallOpposite`, `essentiallySmall_monoOver`, `essentiallySmall_iff`, `essentiallySmall_of_small_of_locallySmall`, `essentiallySmall_fullSubcategory_mem`, `ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1`, `instEssentiallySmallLightProfinite`, `StructuredArrow.essentiallySmall`, `IsFiltered.instEssentiallySmallFullSubcategoryFilteredClosure`, `instEssentiallySmallLightDiagram`, `Discrete.essentiallySmallOfSmall`, `essentiallySmall_of_fully_faithful`, `CostructuredArrow.essentiallySmall`, `Noetherian.toEssentiallySmall`, `essentiallySmall_congr`, `essentiallySmall_of_le`, `essentiallySmallSelf`, `Artinian.toEssentiallySmall`, `IsCofiltered.instEssentiallySmallFullSubcategoryCofilteredClosure`, `ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall`, `essentiallySmall_monoOver_iff_small_subobject`, `essentiallySmall_iff_of_thin`

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasColimitsOfShape_of_essentiallySmall` 📖	mathematical	—	`HasColimitsOfShape`	—	`hasColimitsOfShape_of_equivalence` `hasColimitsOfShapeOfHasColimitsOfSize`
`hasCoproductsOfShape_of_small` 📖	mathematical	`HasCoproducts`	`HasCoproductsOfShape`	—	`hasColimitsOfShape_of_equivalence`
`hasLimitsOfShape_of_essentiallySmall` 📖	mathematical	—	`HasLimitsOfShape`	—	`hasLimitsOfShape_of_equivalence` `hasLimitsOfShapeOfHasLimits`
`hasProductsOfShape_of_small` 📖	mathematical	`HasProducts`	`HasProductsOfShape`	—	`hasLimitsOfShape_of_equivalence`

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`EssentiallySmall` 📖	CompData	22 math math: `essentiallySmall_unop_iff`, `instEssentiallySmallLimitsOfShapeOfSmallOfSmallOfLocallySmall`, `instEssentiallySmallMap`, `instEssentiallySmallColimitsCardinalClosureOfLocallySmall`, `isEssentiallySmall_limitsClosure`, `instEssentiallySmallMax`, `instEssentiallySmallOfSmall`, `IsCardinalFilteredGenerator.essentiallyLarge_top`, `CategoryTheory.instEssentiallySmallIsCardinalPresentableOfHasCardinalFilteredGenerator`, `instEssentiallySmallColimitsClosureOfSmallOfLocallySmall`, `CategoryTheory.exists_equivalence_iff_of_locallySmall`, `instEssentiallySmallTopOfEssentiallySmall`, `IsCardinalFilteredGenerator.essentiallySmall_isPresentable`, `instEssentiallySmallLimitsClosureOfSmallOfLocallySmall`, `instEssentiallySmallOppositeOp`, `EssentiallySmall.of_le`, `instEssentiallySmallIsoClosure`, `exists_equivalence_iff`, `instEssentiallySmallUnopOfOpposite`, `essentiallySmall_op_iff`, `instEssentiallySmallRetractClosureOfLocallySmall`, `CategoryTheory.IsFinitelyAccessibleCategory.instEssentiallySmallIsFinitelyPresentable`

---

← Back to Index