Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-09 16:13 a87f62bc

View on Github →

feat(category_theory/limits/preserves): preserving binary products (#5061) This moves and re-does my old file about preserving binary products to match the new API and framework for preservation of special shapes, and also cleans up some existing API. (I can split this up if necessary but they're all pretty minor changes, so hope this is okay!)

Estimated changes

Modified src/category_theory/closed/cartesian.lean

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

Created src/category_theory/limits/preserves/shapes/binary_products.lean

added def category_theory.limits.is_limit_map_cone_binary_fan_equiv

added def category_theory.limits.is_limit_of_has_binary_product_of_preserves_limit

added def category_theory.limits.is_limit_of_reflects_of_map_is_limit

added def category_theory.limits.map_is_limit_of_preserves_of_is_limit

added def category_theory.limits.preserves_pair.iso

added theorem category_theory.limits.preserves_pair.iso_hom

added def category_theory.limits.preserves_pair.of_iso_comparison

Modified src/category_theory/limits/shapes/binary_products.lean

added def category_theory.limits.coprod_is_coprod

modified def category_theory.limits.map_pair

modified def category_theory.limits.prod_comparison

added def category_theory.limits.prod_is_prod

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

deleted def category_theory.limits.alternative_cone

deleted def category_theory.limits.alternative_cone_is_limit

deleted def category_theory.limits.preserves_binary_prod_of_prod_comparison_iso