Yoneda

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

Statistics

Metric	Count
Definitions yonedaYonedaColimit	1
Theorems instPreservesColimitFunctorOppositeTypeObjCoyonedaOpYoneda, yonedaYonedaColimit_app_inv	2
Total	3

CategoryTheory

Definitions

Name	Category	Theorems
yonedaYonedaColimit 📖	CompOp	1 math math: yonedaYonedaColimit_app_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesColimitFunctorOppositeTypeObjCoyonedaOpYoneda 📖	mathematical	—	Limits.PreservesColimit Functor Opposite Category.opposite types Functor.category Functor.obj coyoneda Opposite.op yoneda	—	Limits.hasColimitOfHasColimitsOfShape Limits.functorCategoryHasColimit Limits.hasColimitCompEvaluation yonedaYonedaColimit_app_inv Iso.inv_hom_id_assoc IsIso.comp_isIso Iso.isIso_inv preservesColimit_of_isIso_post
yonedaYonedaColimit_app_inv 📖	mathematical	—	Iso.inv types Functor.obj Opposite Category.opposite Functor.comp Functor Functor.category Functor.op yoneda Limits.colimit Limits.functorCategoryHasColimit Limits.hasColimitOfHasColimitsOfShape Functor.flip Opposite.op Iso.app yonedaYonedaColimit CategoryStruct.comp Category.toCategoryStruct evaluation Limits.hasColimitCompEvaluation Iso.hom Limits.colimitObjIsoColimitCompEvaluation Limits.colimit.post coyoneda	—	Limits.functorCategoryHasColimit Limits.hasColimitOfHasColimitsOfShape Limits.hasColimitCompEvaluation Limits.PreservesColimitsOfShape.preservesColimit Limits.PreservesColimitsOfSize.preservesColimitsOfShape Limits.Types.instPreservesColimitsOfSizeUliftFunctor Limits.colimit.hom_ext Limits.colimit.ι_post Limits.ι_colimMap_assoc Limits.instHasColimitCompOfPreservesColimit ι_preservesColimitIso_inv_assoc Functor.map_comp_assoc Limits.colimitObjIsoColimitCompEvaluation_ι_inv Functor.whiskerLeft_app types_ext NatTrans.ext' FunctorToTypes.colimit.map_ι_apply map_yonedaEquiv

---

← Back to Index