Skip to content

[Merged by Bors] - feat(Algebra/Homology): commutation up to signs of the compatibility isomorphisms of the total complex with shifts in both variables#11517

Closed
joelriou wants to merge 51 commits intomasterfrom
total-complex-shift-compatibility
Closed

[Merged by Bors] - feat(Algebra/Homology): commutation up to signs of the compatibility isomorphisms of the total complex with shifts in both variables#11517
joelriou wants to merge 51 commits intomasterfrom
total-complex-shift-compatibility

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Mar 19, 2024

Shifting horizontally a bicomplex by an integer x and then taking the total complex gives a cochain complex that is isomorphic to the shift of the total complex of the original bicomplex. The same applies to vertical shifts by an integer y. However, when we apply both horizontal and vertical shifts, depending on whether we apply the horizontal shift or the vertical shift first, we get two isomorphisms which differ by the sign (x * y).negOnePow.


Open in Gitpod

joelriou and others added 30 commits February 19, 2024 02:29
…o homological-complex-mapbifunctor + more API
…' into homological-complex-mapbifunctor-homotopy
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…' into homological-complex-mapbifunctor-homotopy
@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 Mar 24, 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 8, 2024
@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 8, 2024
@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 8, 2024
@joelriou joelriou added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 16, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 16, 2024
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jun 7, 2024

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024

🚀 Pull request has been placed on the maintainer queue by erdOne.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 7, 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.

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 8, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 8, 2024
…isomorphisms of the total complex with shifts in both variables (#11517)

Shifting horizontally a bicomplex by an integer `x` and then taking the total complex gives a cochain complex that is isomorphic to the shift of the total complex of the original bicomplex. The same applies to vertical shifts by an integer `y`. However, when we apply both horizontal and vertical shifts, depending on whether we apply the horizontal shift or the vertical shift first, we get two isomorphisms which differ by the sign `(x * y).negOnePow`.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Homology): commutation up to signs of the compatibility isomorphisms of the total complex with shifts in both variables [Merged by Bors] - feat(Algebra/Homology): commutation up to signs of the compatibility isomorphisms of the total complex with shifts in both variables Jun 8, 2024
@mathlib-bors mathlib-bors bot closed this Jun 8, 2024
@mathlib-bors mathlib-bors bot deleted the total-complex-shift-compatibility branch June 8, 2024 04:57
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
…isomorphisms of the total complex with shifts in both variables (#11517)

Shifting horizontally a bicomplex by an integer `x` and then taking the total complex gives a cochain complex that is isomorphic to the shift of the total complex of the original bicomplex. The same applies to vertical shifts by an integer `y`. However, when we apply both horizontal and vertical shifts, depending on whether we apply the horizontal shift or the vertical shift first, we get two isomorphisms which differ by the sign `(x * y).negOnePow`.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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