Commit 2020-12-10 08:44 ac669c74

View on Github →

chore(category_theory/limits/preserves): cleanup (#4163) (edited to update). This PR entirely re-does the construction of limits from products and equalizers in a shorter way. With the new preserves limits machinery this new construction also shows that a functor which preserves products and equalizers preserves all limits, which previously was really annoying to do

Estimated changes

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

added theorem category_theory.limits.has_limit_of_equalizer_and_product

added def category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_is_limit

added def category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit

deleted def category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_hom

deleted def category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_inv

deleted def category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_iso

deleted def category_theory.limits.has_limit_of_has_products_of_has_equalizers.diagram

added def category_theory.limits.preserves_finite_limits_of_preserves_equalizers_and_finite_products

added def category_theory.limits.preserves_limit_of_preserves_equalizers_and_product

added def category_theory.limits.preserves_limits_of_preserves_equalizers_and_products