Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-14 00:14 bd385fbf

View on Github →

chore(category_theory/limits/functor_category): shuffle limits in functor cats (#4124) Give is_limit versions for statements about limits in the functor category, and write the has_limit versions in terms of those. This also generalises the universes a little. As usual, suggestions for better docstrings or better names appreciated!

Estimated changes

Modified src/category_theory/limits/cones.lean

modified theorem category_theory.limits.cocone.w

modified theorem category_theory.limits.cone.w

Modified src/category_theory/limits/functor_category.lean

deleted theorem category_theory.limits.cocone.functor_w

added def category_theory.limits.combine_cocones

added def category_theory.limits.combine_cones

added def category_theory.limits.combined_is_colimit

added def category_theory.limits.combined_is_limit

deleted theorem category_theory.limits.cone.functor_w

added def category_theory.limits.evaluate_combined_cocones

added def category_theory.limits.evaluate_combined_cones

deleted def category_theory.limits.evaluate_functor_category_colimit_cocone

deleted def category_theory.limits.evaluate_functor_category_limit_cone

added def category_theory.limits.evaluation_jointly_reflects_colimits

added def category_theory.limits.evaluation_jointly_reflects_limits

deleted def category_theory.limits.functor_category_colimit_cocone

deleted def category_theory.limits.functor_category_is_colimit_cocone

deleted def category_theory.limits.functor_category_is_limit_cone

deleted def category_theory.limits.functor_category_limit_cone