New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(category_theory/limits): The associativity of pullbacks and pushouts. #10619
Conversation
/-- | ||
Given | ||
|
||
X₁ - f₁ -> X₂ - f₂ -> X₃ | ||
| | | | ||
i₁ i₂ i₃ | ||
∨ ∨ ∨ | ||
Y₁ - g₁ -> Y₂ - g₂ -> Y₃ | ||
|
||
Then the big square is a pullback if both the small squares are. | ||
-/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What happens if we stack the squares vertically? It's math-trivial that a similar statement holds. But it's not Lean defeq, I guess. Can we avoid duplication?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Composing with either pullback_symmetry
or pullback_cone.flip_is_pullback
works.
I'm not sure if there are better ways to do so.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I hope that will be good enough in practice.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
…outs. (#10619) Also provides the pasting lemma for pullback (pushout) squares Co-authored-by: erd1 <the.erd.one@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Also provides the pasting lemma for pullback (pushout) squares