Skip to content

[Merged by Bors] - feat(CategoryTheory): a product of distinguished triangles is distinguished#7641

Closed
joelriou wants to merge 8 commits intomasterfrom
triangulated-product-distinguished
Closed

[Merged by Bors] - feat(CategoryTheory): a product of distinguished triangles is distinguished#7641
joelriou wants to merge 8 commits intomasterfrom
triangulated-product-distinguished

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Oct 12, 2023 •
edited
Loading

@joelriou joelriou added the t-category-theory Category theory label Oct 12, 2023
github-actions[bot]
github-actions bot reviewed Oct 12, 2023
View reviewed changes
@joelriou joelriou mentioned this pull request Oct 12, 2023
Closed
11 tasks
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 12, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 20, 2023
@ghost
Copy link
Copy Markdown

ghost commented Oct 20, 2023

This PR/issue depends on:

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 20, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 20, 2023
jcommelin
jcommelin reviewed Oct 21, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean Outdated
`φ' : 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. -/
Copy link
Copy Markdown
Member

@jcommelin jcommelin Oct 21, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@bors
Copy link
Copy Markdown

bors bot commented Oct 21, 2023

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Oct 21, 2023
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Oct 21, 2023

Thanks again @jcommelin for the reviews!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 21, 2023
bors bot pushed a commit that referenced this pull request Oct 21, 2023
@joelriou
feat(CategoryTheory): a product of distinguished triangles is disting…
154503a 
…uished (#7641)
bors bot pushed a commit that referenced this pull request Oct 21, 2023
@joelriou
feat(CategoryTheory): a product of distinguished triangles is disting…
ce6094f 
…uished (#7641)
@bors
Copy link
Copy Markdown

bors bot commented Oct 21, 2023

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat(CategoryTheory): a product of distinguished triangles is distinguished [Merged by Bors] - feat(CategoryTheory): a product of distinguished triangles is distinguished Oct 21, 2023
@bors bors bot closed this Oct 21, 2023
@bors bors bot deleted the triangulated-product-distinguished branch October 21, 2023 10:50
@joelriou joelriou mentioned this pull request Jun 13, 2025
Open
11 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@github-actions github-actions[bot] github-actions[bot] left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@joelriou @jcommelin