Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-24 16:14 8590081f

View on Github →

feat(category_theory): Product comparison (#2753) Construct the product comparison morphism, and show it's an iso iff F preserves binary products.

Estimated changes

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

added def category_theory.limits.prod_comparison

added theorem category_theory.limits.prod_comparison_natural

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

added def category_theory.limits.alternative_cone

added def category_theory.limits.alternative_cone_is_limit

added def category_theory.limits.preserves_binary_prod_of_prod_comparison_iso