Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-31 13:18 ca7fee84

View on Github →

feat(category_theory/limits): Results about pullbacks (#9984)

Provided the explicit isomorphism X ×[Z] Y ≅ Y ×[Z] X.
Provided the pullback of f g when either one is iso or when both are mono.

Estimated changes

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

added theorem category_theory.limits.fst_eq_snd_of_mono_eq

added theorem category_theory.limits.has_pullback_of_left_iso

added theorem category_theory.limits.has_pullback_of_right_iso

added theorem category_theory.limits.has_pullback_symmetry

added theorem category_theory.limits.has_pushout_of_left_iso

added theorem category_theory.limits.has_pushout_of_right_iso

added theorem category_theory.limits.has_pushout_symmetry

added theorem category_theory.limits.inl_comp_pushout_symmetry_hom

added theorem category_theory.limits.inl_comp_pushout_symmetry_inv

added theorem category_theory.limits.inl_eq_inr_of_epi_eq

added theorem category_theory.limits.inr_comp_pushout_symmetry_hom

added theorem category_theory.limits.inr_comp_pushout_symmetry_inv

added def category_theory.limits.pullback_cone_of_left_iso

added theorem category_theory.limits.pullback_cone_of_left_iso_X

added theorem category_theory.limits.pullback_cone_of_left_iso_fst

added def category_theory.limits.pullback_cone_of_left_iso_is_limit

added theorem category_theory.limits.pullback_cone_of_left_iso_snd

added theorem category_theory.limits.pullback_cone_of_left_iso_π_app_left

added theorem category_theory.limits.pullback_cone_of_left_iso_π_app_none

added theorem category_theory.limits.pullback_cone_of_left_iso_π_app_right

added def category_theory.limits.pullback_cone_of_right_iso

added theorem category_theory.limits.pullback_cone_of_right_iso_X

added theorem category_theory.limits.pullback_cone_of_right_iso_fst

added def category_theory.limits.pullback_cone_of_right_iso_is_limit

added theorem category_theory.limits.pullback_cone_of_right_iso_snd

added theorem category_theory.limits.pullback_cone_of_right_iso_π_app_left

added theorem category_theory.limits.pullback_cone_of_right_iso_π_app_none

added theorem category_theory.limits.pullback_cone_of_right_iso_π_app_right

added def category_theory.limits.pullback_symmetry

added theorem category_theory.limits.pullback_symmetry_hom_comp_fst

added theorem category_theory.limits.pullback_symmetry_hom_comp_snd

added theorem category_theory.limits.pullback_symmetry_hom_of_epi_eq

added theorem category_theory.limits.pullback_symmetry_hom_of_mono_eq

added theorem category_theory.limits.pullback_symmetry_inv_comp_fst

added theorem category_theory.limits.pullback_symmetry_inv_comp_snd

added theorem category_theory.limits.pushout_cocone.epi_of_is_colimit_mk_id_id

added def category_theory.limits.pushout_cocone.is_colimit_mk_id_id

added def category_theory.limits.pushout_cocone_of_left_iso

added theorem category_theory.limits.pushout_cocone_of_left_iso_X

added theorem category_theory.limits.pushout_cocone_of_left_iso_inl

added theorem category_theory.limits.pushout_cocone_of_left_iso_inr

added def category_theory.limits.pushout_cocone_of_left_iso_is_limit

added theorem category_theory.limits.pushout_cocone_of_left_iso_ι_app_left

added theorem category_theory.limits.pushout_cocone_of_left_iso_ι_app_none

added theorem category_theory.limits.pushout_cocone_of_left_iso_ι_app_right

added def category_theory.limits.pushout_cocone_of_right_iso

added theorem category_theory.limits.pushout_cocone_of_right_iso_X

added theorem category_theory.limits.pushout_cocone_of_right_iso_inl

added theorem category_theory.limits.pushout_cocone_of_right_iso_inr

added def category_theory.limits.pushout_cocone_of_right_iso_is_limit

added theorem category_theory.limits.pushout_cocone_of_right_iso_ι_app_left

added theorem category_theory.limits.pushout_cocone_of_right_iso_ι_app_none

added theorem category_theory.limits.pushout_cocone_of_right_iso_ι_app_right

added def category_theory.limits.pushout_is_pushout

added def category_theory.limits.pushout_symmetry