Skip to content

[Merged by Bors] - feat: naturality of the isomorphisms induced by functors which preserves homology#7624

Closed
joelriou wants to merge 8 commits intomasterfrom
preserves_homology4
Closed

[Merged by Bors] - feat: naturality of the isomorphisms induced by functors which preserves homology#7624
joelriou wants to merge 8 commits intomasterfrom
preserves_homology4

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Oct 11, 2023

If F : C ⥤ D is a functor which preserves homlogy (e.g. preserves finite limits/colimits), there is a natural isomorphism F.mapShortComplex ⋙ ShortComplex.homologyFunctor D ≅ ShortComplex.homologyFunctor C ⋙ F which expresses that F "commutes" with homology.


Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Oct 11, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 11, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 11, 2023
@ghost
Copy link
Copy Markdown

ghost commented Oct 11, 2023

@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 Oct 11, 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 Oct 12, 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

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Oct 12, 2023
bors bot pushed a commit that referenced this pull request Oct 12, 2023
…ves homology (#7624)

If `F : C ⥤ D` is a functor which preserves homlogy (e.g. preserves finite limits/colimits), there is a natural isomorphism `F.mapShortComplex ⋙ ShortComplex.homologyFunctor D ≅ ShortComplex.homologyFunctor C ⋙ F` which expresses that `F` "commutes" with homology.
@bors
Copy link
Copy Markdown

bors bot commented Oct 12, 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: naturality of the isomorphisms induced by functors which preserves homology [Merged by Bors] - feat: naturality of the isomorphisms induced by functors which preserves homology Oct 12, 2023
@bors bors bot closed this Oct 12, 2023
@bors bors bot deleted the preserves_homology4 branch October 12, 2023 12:33
grunweg pushed a commit that referenced this pull request Oct 13, 2023
…ves homology (#7624)

If `F : C ⥤ D` is a functor which preserves homlogy (e.g. preserves finite limits/colimits), there is a natural isomorphism `F.mapShortComplex ⋙ ShortComplex.homologyFunctor D ≅ ShortComplex.homologyFunctor C ⋙ F` which expresses that `F` "commutes" with homology.
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