Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-10 09:20 ce0e2c44

View on Github →

feat(category_theory/limits): Pullback API (#10620) Needed for constructing fibered products of Schemes

Estimated changes

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

added def category_theory.limits.pullback.congr_hom

added theorem category_theory.limits.pullback.congr_hom_inv

added def category_theory.limits.pullback_cone.is_limit_of_comp_mono

added def category_theory.limits.pullback_is_pullback_of_comp_mono

added def category_theory.limits.pushout.congr_hom

added theorem category_theory.limits.pushout.congr_hom_inv

added def category_theory.limits.pushout_cocone.is_colimit_of_epi_comp

added def category_theory.limits.pushout_is_pushout_of_epi_comp