Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-07 19:06 9a0ba082

View on Github →

feat(category_theory/limits/preserves): transfer preserving limits through nat iso (#4932)

Move two defs higher in the file
Shorten some proofs using newer lemmas
Show that we can transfer preservation of limits through natural isomorphism in the functor.

Estimated changes

Modified src/category_theory/limits/preserves/basic.lean

deleted def category_theory.limits.preserves_colimit_of_iso

added def category_theory.limits.preserves_colimit_of_iso_diagram

added def category_theory.limits.preserves_colimit_of_nat_iso

added def category_theory.limits.preserves_colimits_of_nat_iso

added def category_theory.limits.preserves_colimits_of_shape_of_nat_iso

deleted def category_theory.limits.preserves_limit_of_iso

added def category_theory.limits.preserves_limit_of_iso_diagram

added def category_theory.limits.preserves_limit_of_nat_iso

added def category_theory.limits.preserves_limits_of_nat_iso

added def category_theory.limits.preserves_limits_of_shape_of_nat_iso

Modified src/category_theory/limits/shapes/constructions/preserve_binary_products.lean