Commit 2024-07-24 09:19 805fac1b

View on Github →

feat(Pullback/CommSq): add more pasting lemmas for IsPullback (#14985) This PR adds two (variants) of pasting lemmas in the IsPullback framework. These are variants where the second square has a morphism that is induced from the universal property of the first. This work was inspired by the AIM workshop "Formalizing algebraic geometry" in June 2024.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

added theorem CategoryTheory.IsPullback.hom_ext

added theorem CategoryTheory.IsPullback.id_horiz

added theorem CategoryTheory.IsPullback.id_vert

added theorem CategoryTheory.IsPullback.isoIsPullback_hom_fst

added theorem CategoryTheory.IsPullback.isoIsPullback_hom_snd

added theorem CategoryTheory.IsPullback.isoIsPullback_inv_fst

added theorem CategoryTheory.IsPullback.isoIsPullback_inv_snd

added theorem CategoryTheory.IsPullback.lift_fst

added theorem CategoryTheory.IsPullback.lift_snd

added theorem CategoryTheory.IsPullback.of_bot'

added theorem CategoryTheory.IsPullback.of_right'

added theorem CategoryTheory.IsPushout.hom_ext

added theorem CategoryTheory.IsPushout.id_horiz

added theorem CategoryTheory.IsPushout.id_vert

added theorem CategoryTheory.IsPushout.inl_desc

added theorem CategoryTheory.IsPushout.inl_isoIsPushout_hom

added theorem CategoryTheory.IsPushout.inl_isoIsPushout_inv

added theorem CategoryTheory.IsPushout.inr_desc

added theorem CategoryTheory.IsPushout.inr_isoIsPushout_hom

added theorem CategoryTheory.IsPushout.inr_isoIsPushout_inv

deleted theorem CategoryTheory.IsPushout.of_bot

added theorem CategoryTheory.IsPushout.of_left'

added theorem CategoryTheory.IsPushout.of_left

deleted theorem CategoryTheory.IsPushout.of_right

added theorem CategoryTheory.IsPushout.of_top'

added theorem CategoryTheory.IsPushout.of_top