Commit 2024-08-04 10:58 cbbb5d7d

View on Github →

feat(Limits/Shapes/Pullback): add more pasting lemmas (#14414) This PR does the following:

Rewrites the current pasting lemmas so that they take any PullbackCone as input, and not just one obtained through PullbackCone.mk.
Adds vertical pasting lemmas
Adds some missing pasting lemmas in terms of the HasPullbacks/HasPushouts API (e.g. pullbackRightPullbackSndIso). This contribution was inspired by the AIM workshop "Formalizing algebraic geometry" in June 2024.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean

added theorem CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst

added theorem CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd

added theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst

added theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst

added theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd

deleted theorem CategoryTheory.Limits.pullbackDiagonalMapIso_hom_fst

deleted theorem CategoryTheory.Limits.pullbackDiagonalMapIso_hom_snd

deleted theorem CategoryTheory.Limits.pullbackDiagonalMapIso_inv_fst

deleted theorem CategoryTheory.Limits.pullbackDiagonalMapIso_inv_snd_fst

deleted theorem CategoryTheory.Limits.pullbackDiagonalMapIso_inv_snd_snd

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

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

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

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

added def CategoryTheory.Limits.PullbackCone.pasteVertFlip

added def CategoryTheory.Limits.PushoutCocone.pasteVertFlip

deleted def CategoryTheory.Limits.bigSquareIsPullback

deleted def CategoryTheory.Limits.bigSquareIsPushout

added def CategoryTheory.Limits.botSquareIsPushout

added theorem CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_hom

added theorem CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_inv

added theorem CategoryTheory.Limits.inr_inl_pushoutRightPushoutInlIso_hom

added theorem CategoryTheory.Limits.inr_inr_pushoutRightPushoutInlIso_hom

added theorem CategoryTheory.Limits.inr_pushoutRightPushoutInlIso_inv

modified def CategoryTheory.Limits.leftSquareIsPullback

added def CategoryTheory.Limits.pasteHorizIsPullback

added def CategoryTheory.Limits.pasteHorizIsPullbackEquiv

added def CategoryTheory.Limits.pasteHorizIsPushout

added def CategoryTheory.Limits.pasteHorizIsPushoutEquiv

added def CategoryTheory.Limits.pasteVertIsPullback

added def CategoryTheory.Limits.pasteVertIsPullbackEquiv

added def CategoryTheory.Limits.pasteVertIsPushout

added def CategoryTheory.Limits.pasteVertIsPushoutEquiv

added def CategoryTheory.Limits.pullbackLeftPullbackSndIso

added theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst

added theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_snd

added theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst

added theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_snd

added theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_snd_snd

modified def CategoryTheory.Limits.rightSquareIsPushout

added def CategoryTheory.Limits.topSquareIsPullback