Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
wants to merge 7 commits into from

Conversation

joelriou
Copy link
Collaborator

@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
Mathlib.lean Show resolved Hide resolved
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Mar 29, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Apr 18, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot 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
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
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.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot 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
Collaborator 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
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.

3 participants