Commit 2021-10-07 04:15 cb3c8448

View on Github →

feat(category_theory/limits/*): Filtered colimits preserves finite limits (#9522) Restated category_theory.limits.colimit_limit_to_limit_colimit_is_iso in terms of limit preserving.

Estimated changes

Modified src/category_theory/limits/colimit_limit.lean

modified theorem category_theory.limits.ι_colimit_limit_to_limit_colimit_π

Modified src/category_theory/limits/filtered_colimit_commutes_finite_limit.lean

Modified src/category_theory/limits/functor_category.lean

added def category_theory.limits.colimit_iso_swap_comp_colim

added def category_theory.limits.limit_iso_swap_comp_lim