Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-03 05:24 6f745cd2

View on Github →

feat(category_theory/limits): Lemmas about preserving pullbacks (#10438)

Estimated changes

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

added def category_theory.limits.is_colimit_map_cocone_pushout_cocone_equiv

added def category_theory.limits.is_colimit_of_has_pushout_of_preserves_colimit

added def category_theory.limits.is_colimit_of_is_colimit_pushout_cocone_map

added def category_theory.limits.is_colimit_pushout_cocone_map_of_is_colimit

added theorem category_theory.limits.preserves_pullback.iso_hom_fst

added theorem category_theory.limits.preserves_pullback.iso_hom_snd

added theorem category_theory.limits.preserves_pullback.iso_inv_fst

added theorem category_theory.limits.preserves_pullback.iso_inv_snd

added def category_theory.limits.preserves_pullback_symmetry

added theorem category_theory.limits.preserves_pushout.inl_iso_hom

added theorem category_theory.limits.preserves_pushout.inl_iso_inv

added theorem category_theory.limits.preserves_pushout.inr_iso_hom

added theorem category_theory.limits.preserves_pushout.inr_iso_inv

added def category_theory.limits.preserves_pushout.iso

added theorem category_theory.limits.preserves_pushout.iso_hom

added def category_theory.limits.preserves_pushout.of_iso_comparison

added def category_theory.limits.preserves_pushout_symmetry

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

added theorem category_theory.limits.inl_comp_pushout_comparison

added theorem category_theory.limits.inr_comp_pushout_comparison

added def category_theory.limits.pullback_cone.iso_mk

added def category_theory.limits.pushout_cocone.iso_mk

added def category_theory.limits.pushout_comparison

added theorem category_theory.limits.pushout_comparison_map_desc