Colimits

Statistics

Metric	Count
Definitions	0
Theorems `instHasColimitsOfShapeOfPresheafOfModulesValRingCat`, `instHasColimitsOfSizeOfPresheafOfModulesValRingCat`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasColimitsOfShapeOfPresheafOfModulesValRingCat` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape` `SheafOfModules` `instCategory`	—	`CategoryTheory.Presheaf.instIsLocallyInjectiveOfIsIsoFunctorOpposite` `CategoryTheory.IsIso.id` `CategoryTheory.Presheaf.isLocallySurjective_of_iso` `CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful` `CategoryTheory.Functor.Full.comp` `instFullPresheafOfModulesValRingCatForget` `PresheafOfModules.instFullRestrictScalarsIdFunctorOppositeRingCat` `CategoryTheory.Functor.Faithful.comp` `instFaithfulPresheafOfModulesValRingCatForget` `PresheafOfModules.instFaithfulRestrictScalars` `CategoryTheory.Limits.hasColimit_of_iso` `CategoryTheory.Limits.instHasColimitCompOfPreservesColimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `PresheafOfModules.instIsLeftAdjointSheafOfModulesSheafification`
`instHasColimitsOfSizeOfPresheafOfModulesValRingCat` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfSize` `SheafOfModules` `instCategory`	—	`instHasColimitsOfShapeOfPresheafOfModulesValRingCat` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize`

---