Commit 2021-01-09 00:41 12945004View 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?
added theorem category_theory.limits.preserves_pullback.iso_hom
added theorem category_theory.limits.map_lift_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
modified def category_theory.limits.pushout_cocone.is_colimit.mk