Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-16 01:31 c240fcb3

View on Github →

feat(category_theory/limits): pullbacks from binary products and equalizers (#2143)

feat(category_theory/limits): derive has_binary_products from has_limit (pair X Y)
Rename of_diagram to diagram_iso
feat(category_theory/limits): pullbacks from binary products and equalizers
Fix build
Fix indentation
typos
Fix proof
Remove some simp lemmas that were duplicated during merge

Estimated changes

Modified src/category_theory/limits/over.lean

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

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

added def category_theory.limits.has_colimit_span_of_has_colimit_pair_of_has_colimit_parallel_pair

added def category_theory.limits.has_limit_cospan_of_has_limit_pair_of_has_limit_parallel_pair

added def category_theory.limits.has_pullbacks_of_has_binary_products_of_has_equalizers

added def category_theory.limits.has_pushouts_of_has_binary_coproducts_of_has_coequalizers

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

added def category_theory.limits.pullback_cone.is_limit.mk

deleted theorem category_theory.limits.pullback_cone.mk_left

deleted theorem category_theory.limits.pullback_cone.mk_right

added theorem category_theory.limits.pullback_cone.mk_π_app_left

added theorem category_theory.limits.pullback_cone.mk_π_app_one

added theorem category_theory.limits.pullback_cone.mk_π_app_right

added def category_theory.limits.pushout_cocone.is_colimit.mk

added theorem category_theory.limits.pushout_cocone.mk_ι_app_left

added theorem category_theory.limits.pushout_cocone.mk_ι_app_right

added theorem category_theory.limits.pushout_cocone.mk_ι_app_zero