Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-09 00:41 12945004

View on Github →

feat(category_theory/limits): preserving pullbacks (#5668) This touches multiple files but it's essentially the same thing as all my other PRs for preserving limits of special shapes - I can split it up if you'd like but hopefully this is alright?

Estimated changes

Modified src/category_theory/abelian/non_preadditive.lean

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

added def category_theory.limits.is_limit_map_cone_pullback_cone_equiv

added def category_theory.limits.is_limit_of_has_pullback_of_preserves_limit

added def category_theory.limits.is_limit_of_is_limit_pullback_cone_map

added def category_theory.limits.is_limit_pullback_cone_map_of_is_limit

added def category_theory.limits.preserves_pullback.iso

added theorem category_theory.limits.preserves_pullback.iso_hom

added def category_theory.limits.preserves_pullback.of_iso_comparison

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

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

added theorem category_theory.limits.map_lift_pullback_comparison

added def category_theory.limits.pullback_comparison

added theorem category_theory.limits.pullback_comparison_comp_fst

added theorem category_theory.limits.pullback_comparison_comp_snd

modified def category_theory.limits.pullback_cone.is_limit.mk

added def category_theory.limits.pullback_is_pullback

modified def category_theory.limits.pushout_cocone.is_colimit.mk