Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-02 00:17 6624bbe7

View on Github →

feat(category_theory/limits): dualizing some results (#7391) Requested on zulip.

Estimated changes

Renamed src/category_theory/limits/shapes/constructions/finite_products_of_binary_products.lean to src/category_theory/limits/constructions/finite_products_of_binary_products.lean

added def category_theory.extend_cofan

added def category_theory.extend_cofan_is_colimit

added theorem category_theory.has_finite_coproducts_of_has_binary_and_terminal

added def category_theory.preserves_finite_coproducts_of_preserves_binary_and_initial

added def category_theory.preserves_ulift_fin_of_preserves_binary_and_initial

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

added theorem category_theory.limits.colimits_from_coequalizers_and_coproducts

added theorem category_theory.limits.finite_colimits_from_coequalizers_and_finite_coproducts

added theorem category_theory.limits.has_colimit_of_coequalizer_and_coproduct

added def category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_colimit

added def category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_is_colimit

added def category_theory.limits.preserves_colimit_of_preserves_coequalizers_and_coproduct

added def category_theory.limits.preserves_colimits_of_preserves_coequalizers_and_coproducts

added def category_theory.limits.preserves_finite_colimits_of_preserves_coequalizers_and_finite_coproducts

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

added def category_theory.limits.is_colimit_map_cocone_binary_cofan_equiv

added def category_theory.limits.is_colimit_of_has_binary_coproduct_of_preserves_colimit

added def category_theory.limits.is_colimit_of_reflects_of_map_is_colimit

added def category_theory.limits.map_is_colimit_of_preserves_of_is_colimit

added def category_theory.limits.preserves_colimit_pair.iso

added theorem category_theory.limits.preserves_colimit_pair.iso_hom

added def category_theory.limits.preserves_colimit_pair.of_iso_coprod_comparison

added def category_theory.limits.preserves_limit_pair.iso

added theorem category_theory.limits.preserves_limit_pair.iso_hom

added def category_theory.limits.preserves_limit_pair.of_iso_prod_comparison

deleted def category_theory.limits.preserves_pair.iso

deleted theorem category_theory.limits.preserves_pair.iso_hom

deleted def category_theory.limits.preserves_pair.of_iso_comparison

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

added def category_theory.limits.is_colimit_cofan_mk_obj_of_is_colimit

added def category_theory.limits.is_colimit_map_cocone_cofan_mk_equiv

added def category_theory.limits.is_colimit_of_has_coproduct_of_preserves_colimit

added def category_theory.limits.is_colimit_of_is_colimit_cofan_mk_obj

added theorem category_theory.limits.preserves_coproduct.inv_hom

added def category_theory.limits.preserves_coproduct.iso

added def category_theory.limits.preserves_coproduct.of_iso_comparison

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

added def category_theory.limits.coprod_comparison

added theorem category_theory.limits.coprod_comparison_inl

added theorem category_theory.limits.coprod_comparison_inr

added theorem category_theory.limits.coprod_comparison_inv_natural

added def category_theory.limits.coprod_comparison_nat_iso

added def category_theory.limits.coprod_comparison_nat_trans

added theorem category_theory.limits.coprod_comparison_natural

modified def category_theory.limits.coprod_is_coprod

added theorem category_theory.limits.map_inl_inv_coprod_comparison

added theorem category_theory.limits.map_inr_inv_coprod_comparison

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

added def category_theory.limits.coproduct_is_coproduct