Skip to content

[Merged by Bors] - feat(Algebra/Homology): compatibilities of homology and shifts#11782

Closed
joelriou wants to merge 7 commits intomasterfrom
homotopy-category-shift-sequence
Closed

[Merged by Bors] - feat(Algebra/Homology): compatibilities of homology and shifts#11782
joelriou wants to merge 7 commits intomasterfrom
homotopy-category-shift-sequence

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Mar 29, 2024

This PR studies the compatibilities of homology and shifts. This results into ShiftSequence instances for the homology functor in the CochainComplex and HomotopyCategory namespaces.


Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Mar 29, 2024
Comment thread Mathlib.lean
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 29, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 18, 2024
@ghost
Copy link
Copy Markdown

ghost commented Apr 18, 2024

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 Apr 18, 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.

LGTM, modulo the merge conflict

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 18, 2024

✌️ 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 removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 18, 2024
@joelriou
Copy link
Copy Markdown
Contributor Author

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Apr 18, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 18, 2024
This PR studies the compatibilities of homology and shifts. This results into `ShiftSequence` instances for the homology functor in the `CochainComplex` and `HomotopyCategory` namespaces.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Homology): compatibilities of homology and shifts [Merged by Bors] - feat(Algebra/Homology): compatibilities of homology and shifts Apr 18, 2024
@mathlib-bors mathlib-bors bot closed this Apr 18, 2024
@mathlib-bors mathlib-bors bot deleted the homotopy-category-shift-sequence branch April 18, 2024 10:42
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
This PR studies the compatibilities of homology and shifts. This results into `ShiftSequence` instances for the homology functor in the `CochainComplex` and `HomotopyCategory` namespaces.
callesonne pushed a commit that referenced this pull request Apr 22, 2024
This PR studies the compatibilities of homology and shifts. This results into `ShiftSequence` instances for the homology functor in the `CochainComplex` and `HomotopyCategory` namespaces.
Jun2M pushed a commit that referenced this pull request Apr 24, 2024
This PR studies the compatibilities of homology and shifts. This results into `ShiftSequence` instances for the homology functor in the `CochainComplex` and `HomotopyCategory` namespaces.
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