Documentation Verification Report

Limits

📁 Source: Mathlib/Topology/Sheaves/Limits.lean

Statistics

Metric	Count
Definitions `instCreatesLimitsOfShapeSheafPresheafForgetOfHasLimitsOfShape`, `instCreatesLimitsSheafPresheafForgetOfHasLimits`	2
Theorems `instHasColimitsOfShapePresheaf`, `instHasColimitsOfSizePresheafOfHasColimits`, `instHasLimitsOfShapePresheaf`, `instHasLimitsOfShapeSheaf`, `instHasLimitsOfSizeSheafOfHasLimits`, `instHasLimitsPresheaf`, `isSheaf_of_isLimit`, `limit_isSheaf`	8
Total	10

TopCat

Definitions

Name	Category	Theorems
`instCreatesLimitsOfShapeSheafPresheafForgetOfHasLimitsOfShape` 📖	CompOp	—
`instCreatesLimitsSheafPresheafForgetOfHasLimits` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasColimitsOfShapePresheaf` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape` `Presheaf` `instCategoryPresheaf`	—	`CategoryTheory.Limits.functorCategoryHasColimitsOfShape`
`instHasColimitsOfSizePresheafOfHasColimits` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfSize` `Presheaf` `instCategoryPresheaf`	—	`instHasColimitsOfShapePresheaf` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize`
`instHasLimitsOfShapePresheaf` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape` `Presheaf` `instCategoryPresheaf`	—	`CategoryTheory.Limits.functorCategoryHasLimitsOfShape`
`instHasLimitsOfShapeSheaf` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape` `Sheaf` `instCategorySheaf`	—	`CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape` `instHasLimitsOfShapePresheaf`
`instHasLimitsOfSizeSheafOfHasLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfSize` `Sheaf` `instCategorySheaf`	—	`instHasLimitsOfShapeSheaf` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits`
`instHasLimitsPresheaf` 📖	mathematical	—	`CategoryTheory.Limits.HasLimits` `Presheaf` `instCategoryPresheaf`	—	`instHasLimitsOfShapePresheaf` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits`
`isSheaf_of_isLimit` 📖	mathematical	`Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `Presheaf` `instCategoryPresheaf`	`CategoryTheory.Limits.Cone.pt`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `Presheaf.isSheaf_of_iso` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `instHasLimitsOfShapeSheaf` `CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit` `instHasLimitsOfShapePresheaf` `CategoryTheory.Sheaf.cond`
`limit_isSheaf` 📖	mathematical	`Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `Presheaf` `instCategoryPresheaf`	`CategoryTheory.Limits.limit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `instHasLimitsOfShapePresheaf`	—	`isSheaf_of_isLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `instHasLimitsOfShapePresheaf`

---

← Back to Index