Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-02 17:36 4b0a82c3

View on Github →

feat(category_theory): preservation of (co)limits, (co)limits in functor categories

Estimated changes

Created category_theory/limits/functor_category.lean

added theorem category_theory.limits.cocone.functor_w

added theorem category_theory.limits.cone.functor_w

added def category_theory.limits.evaluate_functor_category_colimit_cocone

added def category_theory.limits.evaluate_functor_category_limit_cone

added def category_theory.limits.functor_category_colimit_cocone

added def category_theory.limits.functor_category_is_colimit_cocone

added def category_theory.limits.functor_category_is_limit_cone

added def category_theory.limits.functor_category_limit_cone

Created category_theory/limits/preserves.lean

added def category_theory.limits.preserves_colimit_of_preserves_colimit_cocone

added def category_theory.limits.preserves_colimits

added def category_theory.limits.preserves_colimits_of_shape

added def category_theory.limits.preserves_limit_of_preserves_limit_cone

added def category_theory.limits.preserves_limits

added def category_theory.limits.preserves_limits_of_shape

added def category_theory.limits.reflects_colimits

added def category_theory.limits.reflects_colimits_of_shape

added def category_theory.limits.reflects_limits

added def category_theory.limits.reflects_limits_of_shape

Modified category_theory/natural_transformation.lean

added theorem category_theory.nat_trans.congr_app