Skip to content

[Merged by Bors] - feat: basic definitions for Algebra.Homology.ShortComplex.Homology#4204

Closed
joelriou wants to merge 11 commits intomasterfrom
shortcomplex_homology_defs
Closed

[Merged by Bors] - feat: basic definitions for Algebra.Homology.ShortComplex.Homology#4204
joelriou wants to merge 11 commits intomasterfrom
shortcomplex_homology_defs

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented May 22, 2023

This PR introduces the basic definition of a HomologyData for S : ShortComplex C.


In future PR, the API shall be developed, and S.homology : C shall be defined as h.left.H for some choice of h : S.HomologyData. Then, almost by definition, the homology shall be a self-dual notion.

Note: When we know that a short complex S has homology (e.g. if C is abelian), then any h : S.LeftHomologyData
will provide an isomorphism h.homologyIso : S.homology ≅ h.H (and similarly for RightHomologyData). The user may provide both Left and Right homology data, but only one of these shall be necessary.

Open in Gitpod

@kim-em kim-em added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 22, 2023
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 24, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented May 24, 2023

This PR/issue depends on:

@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 24, 2023
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 24, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented May 24, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 24, 2023
bors bot pushed a commit that referenced this pull request May 24, 2023
…4204)

This PR introduces the basic definition of a `HomologyData` for `S : ShortComplex C`.
@bors
Copy link
Copy Markdown

bors bot commented May 24, 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: basic definitions for Algebra.Homology.ShortComplex.Homology [Merged by Bors] - feat: basic definitions for Algebra.Homology.ShortComplex.Homology May 24, 2023
@bors bors bot closed this May 24, 2023
@bors bors bot deleted the shortcomplex_homology_defs branch May 24, 2023 23:18
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.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants