Skip to content

[Merged by Bors] - feat(CategoryTheory/Triangulated): shifting distinguished triangles and variations on the five lemma#7053

Closed
joelriou wants to merge 4 commits intomasterfrom
triangulated-shift-distinguished
Closed

[Merged by Bors] - feat(CategoryTheory/Triangulated): shifting distinguished triangles and variations on the five lemma#7053
joelriou wants to merge 4 commits intomasterfrom
triangulated-shift-distinguished

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Sep 9, 2023

In this PR, it is shown that the shift of a distinguished triangle is a distinguished triangle. It is also shown that in a morphism between distinguished triangles, if two morphisms are isomorphisms, so is the third.


Open in Gitpod

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.

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 14, 2023
bors bot pushed a commit that referenced this pull request Sep 14, 2023
…nd variations on the five lemma (#7053)

In this PR, it is shown that the shift of a distinguished triangle is a distinguished triangle. It is also shown that in a morphism between distinguished triangles, if two morphisms are isomorphisms, so is the third.
@bors
Copy link
Copy Markdown

bors bot commented Sep 14, 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/Triangulated): shifting distinguished triangles and variations on the five lemma [Merged by Bors] - feat(CategoryTheory/Triangulated): shifting distinguished triangles and variations on the five lemma Sep 14, 2023
@bors bors bot closed this Sep 14, 2023
@bors bors bot deleted the triangulated-shift-distinguished branch September 14, 2023 11:42
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
…nd variations on the five lemma (#7053)

In this PR, it is shown that the shift of a distinguished triangle is a distinguished triangle. It is also shown that in a morphism between distinguished triangles, if two morphisms are isomorphisms, so is the third.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants