Documentation Verification Report

Grothendieck

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Grothendieck.lean

Statistics

Metric	Count
Definitions `fiberwiseColimitLimitIso`	1
Theorems `fiberwiseColimitLimitIso_hom_app`, `fiberwiseColimitLimitIso_inv_app`, `preservesLimitsOfShape_colim_grothendieck`	3
Total	4

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`fiberwiseColimitLimitIso` 📖	CompOp	2 math math: `fiberwiseColimitLimitIso_hom_app`, `fiberwiseColimitLimitIso_inv_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fiberwiseColimitLimitIso_hom_app` 📖	mathematical	`HasColimitsOfShape` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Functor.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.Cat.str` `PreservesLimitsOfShape` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `colim`	`CategoryTheory.NatTrans.app` `fiberwiseColimit` `limit` `CategoryTheory.Grothendieck` `CategoryTheory.Grothendieck.instCategory` `CategoryTheory.Functor.comp` `fiberwiseColim` `CategoryTheory.Iso.hom` `functorCategoryHasLimit` `hasLimitOfHasLimitsOfShape` `CategoryTheory.Functor.flip` `hasColimitOfHasColimitsOfShape` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Grothendieck.ι` `fiberwiseColimitLimitIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `colimit` `hasColimit_ι_comp` `CategoryTheory.Functor.whiskeringLeft` `HasColimit.isoOfNatIso` `CategoryTheory.Iso.symm` `limitCompWhiskeringLeftIsoCompLimit` `CategoryTheory.preservesLimitIso` `CategoryTheory.evaluation` `HasLimit.isoOfNatIso` `CategoryTheory.Iso.trans` `CategoryTheory.Functor.associator` `CategoryTheory.Functor.isoWhiskerLeft` `fiberwiseColimCompEvaluationIso` `CategoryTheory.Iso.inv` `limitObjIsoLimitCompEvaluation`	—	`functorCategoryHasLimit` `hasLimitOfHasLimitsOfShape` `hasColimitOfHasColimitsOfShape`
`fiberwiseColimitLimitIso_inv_app` 📖	mathematical	`HasColimitsOfShape` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Functor.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.Cat.str` `PreservesLimitsOfShape` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `colim`	`CategoryTheory.NatTrans.app` `limit` `CategoryTheory.Functor.comp` `CategoryTheory.Grothendieck` `CategoryTheory.Grothendieck.instCategory` `fiberwiseColim` `fiberwiseColimit` `CategoryTheory.Iso.inv` `functorCategoryHasLimit` `hasLimitOfHasLimitsOfShape` `CategoryTheory.Functor.flip` `hasColimitOfHasColimitsOfShape` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Grothendieck.ι` `fiberwiseColimitLimitIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.evaluation` `colimit` `hasColimit_ι_comp` `CategoryTheory.Iso.hom` `limitObjIsoLimitCompEvaluation` `CategoryTheory.Functor.whiskeringLeft` `HasLimit.isoOfNatIso` `CategoryTheory.Iso.trans` `CategoryTheory.Functor.associator` `CategoryTheory.Functor.isoWhiskerLeft` `CategoryTheory.Iso.symm` `fiberwiseColimCompEvaluationIso` `CategoryTheory.preservesLimitIso` `HasColimit.isoOfNatIso` `limitCompWhiskeringLeftIsoCompLimit`	—	`hasColimit_ι_comp` `CategoryTheory.Category.assoc`
`preservesLimitsOfShape_colim_grothendieck` 📖	mathematical	`HasColimitsOfShape` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Functor.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.Cat.str` `PreservesLimitsOfShape` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `colim`	`CategoryTheory.Grothendieck` `CategoryTheory.Grothendieck.instCategory` `hasColimitsOfShape_grothendieck`	—	`hasColimitsOfShape_grothendieck` `functorCategoryHasLimit` `hasLimitOfHasLimitsOfShape` `hasColimitOfHasColimitsOfShape` `instHasLimitCompOfPreservesLimit` `PreservesLimitsOfShape.preservesLimit` `hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit` `CategoryTheory.preservesLimit_of_isIso_post` `limit.hom_ext` `limit.post_π` `CategoryTheory.Iso.trans_assoc` `CategoryTheory.Category.assoc` `HasLimit.isoOfNatIso_hom_π` `CategoryTheory.Category.id_comp` `CategoryTheory.preservesLimitIso_hom_π_assoc` `colimit.hom_ext` `ι_colimMap` `hasColimit_ι_comp` `ι_colimitFiberwiseColimitIso_inv_assoc` `HasColimit.isoOfNatIso_ι_hom_assoc` `ι_colimMap_assoc` `hasLimitCompEvaluation` `limitObjIsoLimitCompEvaluation_inv_π_app_assoc` `HasLimit.isoOfNatIso_hom_π_assoc` `CategoryTheory.Category.comp_id` `ι_colimitFiberwiseColimitIso_hom` `limitCompWhiskeringLeftIsoCompLimit_inv_π` `CategoryTheory.Iso.isIso_hom`

---

← Back to Index