FullyFaithfulLimits

Statistics

Metric	Count
Definitions	0
Theorems `preservesColimitsOfShape_iff`, `preservesColimitsOfSize_iff`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`preservesColimitsOfShape_iff` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `CategoryTheory.Functor.comp`	—	`isLeftAdjoint` `CategoryTheory.Limits.comp_preservesColimitsOfShape` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `counit_isIso_of_R_fully_faithful` `CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Functor.map_isIso` `CategoryTheory.NatIso.isIso_app_of_isIso` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.whiskerRight_comp` `CategoryTheory.Functor.map_id` `CategoryTheory.NatIso.isIso_inv_app` `CategoryTheory.Functor.map_inv` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.map_comp`
`preservesColimitsOfSize_iff` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfSize` `CategoryTheory.Functor.comp`	—	`isLeftAdjoint` `CategoryTheory.Limits.comp_preservesColimits` `CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint` `preservesColimitsOfShape_iff` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape`

---