Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 07:52 8b8f08d0

View on Github →

feat(category_theory/limits): The associativity of pullbacks and pushouts. (#10619) Also provides the pasting lemma for pullback (pushout) squares

Estimated changes

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

added def category_theory.limits.big_square_is_pullback

added def category_theory.limits.big_square_is_pushout

added theorem category_theory.limits.has_pullback_assoc

added theorem category_theory.limits.has_pullback_assoc_symm

added theorem category_theory.limits.has_pushout_assoc

added theorem category_theory.limits.has_pushout_assoc_symm

added theorem category_theory.limits.inl_inl_pushout_assoc_hom

added theorem category_theory.limits.inl_inl_pushout_left_pushout_inr_iso_hom

added theorem category_theory.limits.inl_inr_pushout_assoc_inv

added theorem category_theory.limits.inl_pushout_assoc_inv

added theorem category_theory.limits.inl_pushout_left_pushout_inr_iso_inv

added theorem category_theory.limits.inr_inl_pushout_assoc_hom

added theorem category_theory.limits.inr_inl_pushout_left_pushout_inr_iso_hom

added theorem category_theory.limits.inr_inr_pushout_assoc_inv

added theorem category_theory.limits.inr_pushout_assoc_hom

added theorem category_theory.limits.inr_pushout_left_pushout_inr_iso_hom

added theorem category_theory.limits.inr_pushout_left_pushout_inr_iso_inv

added def category_theory.limits.left_square_is_pullback

added def category_theory.limits.pullback_assoc

added theorem category_theory.limits.pullback_assoc_hom_fst

added theorem category_theory.limits.pullback_assoc_hom_snd_fst

added theorem category_theory.limits.pullback_assoc_hom_snd_snd

added theorem category_theory.limits.pullback_assoc_inv_fst_fst

added theorem category_theory.limits.pullback_assoc_inv_fst_snd

added theorem category_theory.limits.pullback_assoc_inv_snd

added def category_theory.limits.pullback_assoc_is_pullback

added def category_theory.limits.pullback_assoc_symm_is_pullback

added def category_theory.limits.pullback_pullback_left_is_pullback

added def category_theory.limits.pullback_pullback_right_is_pullback

added def category_theory.limits.pullback_right_pullback_fst_iso

added theorem category_theory.limits.pullback_right_pullback_fst_iso_hom_fst

added theorem category_theory.limits.pullback_right_pullback_fst_iso_hom_snd

added theorem category_theory.limits.pullback_right_pullback_fst_iso_inv_fst

added theorem category_theory.limits.pullback_right_pullback_fst_iso_inv_snd_fst

added theorem category_theory.limits.pullback_right_pullback_fst_iso_inv_snd_snd

added def category_theory.limits.pushout_assoc

added def category_theory.limits.pushout_assoc_is_pushout

added def category_theory.limits.pushout_assoc_symm_is_pushout

added def category_theory.limits.pushout_left_pushout_inr_iso

added def category_theory.limits.pushout_pushout_left_is_pushout

added def category_theory.limits.pushout_pushout_right_is_pushout

added def category_theory.limits.right_square_is_pushout