-
Notifications
You must be signed in to change notification settings - Fork 235
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): the total complex of a bicomplex #9331
Conversation
joelriou
commented
Dec 29, 2023
•
edited
edited
- depends on: [Merged by Bors] - refactor(Algebra/Homology): the category of bicomplexes #9333
- depends on: [Merged by Bors] - feat(Algebra/Homology): signs for the construction of the total complex #9335
This PR/issue depends on: |
exact h₁₂ (by simpa only [← h, ← h₂] using ComplexShape.rel_π₂ c₁ c₁₂ i₁ h₁) | ||
· exact d₂_eq_zero _ _ _ _ _ h₁ | ||
simp only [GradedObject.ι_descMapObj, comp_zero, w₁, w₂, add_zero] | ||
d_comp_d' i₁₂ i₁₂' i₁₂'' h₁ h₂ := by |
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.
This proof is massive. Do you think you can factor out some parts, and possibly deduplicate a bit?
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.
Thanks for the review! In the last commit 2f17fe7 I have added definitions D₁
and D₂
, so that the differential is d := D₁ + D₂
, and in order to prove d_comp_d
, I have obtained separate lemmas D₁_D₁
, D₂_D₁
and D₂_D₂
. The code is then slightly longer, but appears in smaller chunks; overall, it should be more manageable. (I also believe that introducing these definitions D₁
and D₂
will ease certain future developments.)
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.
Thanks 🎉
bors merge
Build failed (retrying...): |
Pull request successfully merged into master. Build succeeded: |