Skip to content

[Merged by Bors] - feat(Algebra/Homology/HomotopyCategory): alternative description of distinguished triangles#9370

Closed
joelriou wants to merge 89 commits intomasterfrom
homotopy-category-degreewise-split
Closed

[Merged by Bors] - feat(Algebra/Homology/HomotopyCategory): alternative description of distinguished triangles#9370
joelriou wants to merge 89 commits intomasterfrom
homotopy-category-degreewise-split

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Dec 31, 2023

joelriou and others added 30 commits December 9, 2023 15:53
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Feb 8, 2024
@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 Feb 9, 2024
@jcommelin jcommelin self-assigned this Feb 13, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 13, 2024
@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 Feb 13, 2024
@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 Feb 13, 2024
@joelriou joelriou added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Feb 13, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 13, 2024
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 Feb 13, 2024
mathlib-bors bot pushed a commit that referenced this pull request Feb 13, 2024
…istinguished triangles (#9370)

In this PR, it is shown that a triangle in the homotopy category is distinguished iff it is isomorphic to the triangle associated to a degreewise split short exact sequence of cochain complexes.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 13, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Homology/HomotopyCategory): alternative description of distinguished triangles [Merged by Bors] - feat(Algebra/Homology/HomotopyCategory): alternative description of distinguished triangles Feb 13, 2024
@mathlib-bors mathlib-bors bot closed this Feb 13, 2024
@mathlib-bors mathlib-bors bot deleted the homotopy-category-degreewise-split branch February 13, 2024 21:13
riccardobrasca pushed a commit that referenced this pull request Feb 18, 2024
…istinguished triangles (#9370)

In this PR, it is shown that a triangle in the homotopy category is distinguished iff it is isomorphic to the triangle associated to a degreewise split short exact sequence of cochain complexes.
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
…istinguished triangles (#9370)

In this PR, it is shown that a triangle in the homotopy category is distinguished iff it is isomorphic to the triangle associated to a degreewise split short exact sequence of cochain complexes.
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