Commit 2023-03-02 11:55 2affd54a

View on Github →

feat: port/CategoryTheory.Limits.FunctorCategory (#2380)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/FunctorCategory.lean

added theorem CategoryTheory.Limits.colimit.ι_desc_app

added def CategoryTheory.Limits.colimitFlipIsoCompColim

added def CategoryTheory.Limits.colimitIsoFlipCompColim

added def CategoryTheory.Limits.colimitIsoSwapCompColim

added def CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation

added theorem CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_inv_colimit_map

added theorem CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_app_hom

added theorem CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_inv

added theorem CategoryTheory.Limits.colimit_map_colimitObjIsoColimitCompEvaluation_hom

added theorem CategoryTheory.Limits.colimit_obj_ext

added def CategoryTheory.Limits.combineCocones

added def CategoryTheory.Limits.combineCones

added def CategoryTheory.Limits.combinedIsColimit

added def CategoryTheory.Limits.combinedIsLimit

added def CategoryTheory.Limits.evaluateCombinedCocones

added def CategoryTheory.Limits.evaluateCombinedCones

added def CategoryTheory.Limits.evaluationJointlyReflectsColimits

added def CategoryTheory.Limits.evaluationJointlyReflectsLimits

added theorem CategoryTheory.Limits.limit.lift_π_app

added def CategoryTheory.Limits.limitFlipIsoCompLim

added def CategoryTheory.Limits.limitIsoFlipCompLim

added def CategoryTheory.Limits.limitIsoSwapCompLim

added def CategoryTheory.Limits.limitObjIsoLimitCompEvaluation

added theorem CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_hom_π

added theorem CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_limit_map

added theorem CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_π_app

added theorem CategoryTheory.Limits.limit_map_limitObjIsoLimitCompEvaluation_hom

added theorem CategoryTheory.Limits.limit_obj_ext

added def CategoryTheory.Limits.preservesColimitOfEvaluation

added def CategoryTheory.Limits.preservesColimitsOfEvaluation

added def CategoryTheory.Limits.preservesColimitsOfShapeOfEvaluation

added def CategoryTheory.Limits.preservesLimitOfEvaluation

added def CategoryTheory.Limits.preservesLimitsOfEvaluation

added def CategoryTheory.Limits.preservesLimitsOfShapeOfEvaluation