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] - refactor: introduce the new homology API for homological complex and rename the old one #7954
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, modulo 1 comment.
bors d+
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Johan Commelin <johan@commelin.net>
bors merge |
…rename the old one (#7954) This PR renames definitions of the current homology API (adding a `'` to `homology`, `cycles`, `QuasiIso`) so as to create space for the development of the new homology API of homological complexes: this PR also contains the new definition of `HomologicalComplex.homology` which involves the homology theory of short complexes. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
…rename the old one (#7954) This PR renames definitions of the current homology API (adding a `'` to `homology`, `cycles`, `QuasiIso`) so as to create space for the development of the new homology API of homological complexes: this PR also contains the new definition of `HomologicalComplex.homology` which involves the homology theory of short complexes. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
This PR renames definitions of the current homology API (adding a
'
tohomology
,cycles
,QuasiIso
) so as to create space for the development of the new homology API of homological complexes: this PR also contains the new definition ofHomologicalComplex.homology
which involves the homology theory of short complexes.Next, the plan is to develop this new homology API, and then make small PRs which remove the downstream uses of the old homology API, replacing these with the new API. Significant steps will include refactors of projective/injective resolutions and left/right derived functors. Enabling the use of the new homology API in the development of group cohomology is also important. (Eventually, when the old API is no longer used and when old statements all have equivalents in the new homology API, it could be removed.)