Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-07 11:57 18a42f3f

View on Github →

feat(src/category_theory/*): Yoneda preserves limits. (#9580) Shows that yoneda and coyoneda preserves and reflects limits.

Estimated changes

Modified src/category_theory/limits/functor_category.lean

added def category_theory.limits.preserves_colimit_of_evaluation

added def category_theory.limits.preserves_colimits_of_evaluation

added def category_theory.limits.preserves_colimits_of_shape_of_evaluation

added def category_theory.limits.preserves_limit_of_evaluation

added def category_theory.limits.preserves_limits_of_evaluation

added def category_theory.limits.preserves_limits_of_shape_of_evaluation

Modified src/category_theory/limits/yoneda.lean