[Merged by Bors] - feat(CategoryTheory): a product of distinguished triangles is distinguished #7641
Conversation
joelriou
commented
Oct 12, 2023
•
joelriou
commented
- depends on: [Merged by Bors] - [Merged by Bors] - feat: pretriangulated categories have finite biproducts #7626
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
| `φ' : T' ⟶ productTriangle T` with `T'` distinguished, and such that | ||
| `φ'.hom₁` and `φ'.hom₂` are identities. Then, it suffices to show that | ||
| `φ'.hom₃` is an isomorphism, which is achieved by using Yoneda's lemma | ||
| and a diagram chase. -/ |
There was a problem hiding this comment.
Could you please add a comment near the diagram chase? I think we should mark such proofs, so that we can have real-world test cases for future diagram chasing tactics.
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks again @jcommelin for the reviews! bors merge |
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
