Skip to content

[Merged by Bors] - feat: the shift on the category of triangles#6688

Closed
joelriou wants to merge 12 commits intomasterfrom
hasshift_triangle
Closed

[Merged by Bors] - feat: the shift on the category of triangles#6688
joelriou wants to merge 12 commits intomasterfrom
hasshift_triangle

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Aug 20, 2023

If a preadditive category C is equipped with a shift by the integers, then the category of triangles in C is also equipped with a shift.


Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Aug 20, 2023
@joelriou joelriou added WIP Work in progress and removed awaiting-review labels Aug 22, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 22, 2023
@joelriou joelriou removed the WIP Work in progress label Aug 22, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 4, 2023
@ghost
Copy link
Copy Markdown

ghost commented Sep 4, 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 Sep 4, 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 Sep 4, 2023
@joelriou joelriou added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Sep 5, 2023
@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 Sep 5, 2023
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

bors bot pushed a commit that referenced this pull request Sep 5, 2023
If a preadditive category `C` is equipped with a shift by the integers, then the category of triangles in `C` is also equipped with a shift.
@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 5, 2023
@bors
Copy link
Copy Markdown

bors bot commented Sep 5, 2023

Build failed:

@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Sep 5, 2023

bors r+

bors bot pushed a commit that referenced this pull request Sep 5, 2023
If a preadditive category `C` is equipped with a shift by the integers, then the category of triangles in `C` is also equipped with a shift.
@bors
Copy link
Copy Markdown

bors bot commented Sep 5, 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: the shift on the category of triangles [Merged by Bors] - feat: the shift on the category of triangles Sep 5, 2023
@bors bors bot closed this Sep 5, 2023
@bors bors bot deleted the hasshift_triangle branch September 5, 2023 15:17
ebab pushed a commit that referenced this pull request Sep 11, 2023
If a preadditive category `C` is equipped with a shift by the integers, then the category of triangles in `C` is also equipped with a shift.
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
If a preadditive category `C` is equipped with a shift by the integers, then the category of triangles in `C` is also equipped with a shift.
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.

3 participants