Commit 2022-07-27 14:34 f11e306a

View on Github →

feat(category_theory/limits/construction): Construct finite limits from terminal objects and pullbacks (#14948) Also provides the dual version, and also in terms of preserves_limit.

Estimated changes

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

added def is_binary_coproduct_of_is_initial_is_pushout

added def is_binary_product_of_is_terminal_is_pullback

added def preserves_binary_coproducts_of_preserves_initial_and_pushouts

added def preserves_binary_products_of_preserves_terminal_and_pullbacks

Modified src/category_theory/limits/constructions/equalizers.lean

added def category_theory.limits.has_coequalizers_of_pushouts_and_binary_coproducts.coequalizer_cocone

added def category_theory.limits.has_coequalizers_of_pushouts_and_binary_coproducts.coequalizer_cocone_is_colimit

added def category_theory.limits.has_coequalizers_of_pushouts_and_binary_coproducts.construct_coequalizer

added def category_theory.limits.has_coequalizers_of_pushouts_and_binary_coproducts.pushout_inl

added theorem category_theory.limits.has_coequalizers_of_pushouts_and_binary_coproducts.pushout_inl_eq_pushout_inr

added theorem category_theory.limits.has_coequalizers_of_pushouts_and_binary_coproducts

modified theorem category_theory.limits.has_equalizers_of_pullbacks_and_binary_products

added def category_theory.limits.preserves_coequalizers_of_pushouts_and_binary_coproducts

added def category_theory.limits.preserves_equalizers_of_pullbacks_and_binary_products

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

added theorem category_theory.limits.has_finite_colimits_of_has_initial_and_pushouts

added theorem category_theory.limits.has_finite_limits_of_has_terminal_and_pullbacks

added def category_theory.limits.preserves_finite_colimits_of_preserves_initial_and_pushouts

added def category_theory.limits.preserves_finite_limits_of_preserves_terminal_and_pullbacks

Modified src/category_theory/limits/preserves/shapes/pullbacks.lean

added theorem category_theory.limits.has_pullback_of_preserves_pullback

added theorem category_theory.limits.has_pushout_of_preserves_pushout