Colimits

Statistics

Metric	Count
Definitions	0
Theorems `instHasColimitsOfShapeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf`, `instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasColimitsOfShapeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape` `SheafOfModules` `instCategory`	—	`CategoryTheory.Presheaf.instIsLocallyInjectiveOfIsIsoFunctorOpposite` `CategoryTheory.IsIso.id` `CategoryTheory.Presheaf.isLocallySurjective_of_iso` `PresheafOfModules.instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction` `CategoryTheory.Limits.hasColimit_of_iso` `CategoryTheory.Limits.instHasColimitCompOfPreservesColimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `PresheafOfModules.instIsLeftAdjointSheafOfModulesSheafification`
`instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfSize` `SheafOfModules` `instCategory`	—	`instHasColimitsOfShapeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize`

---