Skip to content

[Merged by Bors] - feat(Algebra/Homology/SpectralObject): homology of the differentials#36182

Closed
joelriou wants to merge 130 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-2-homology
Closed

[Merged by Bors] - feat(Algebra/Homology/SpectralObject): homology of the differentials#36182
joelriou wants to merge 130 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-2-homology

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Mar 5, 2026 •
edited
Loading

joelriou and others added 30 commits February 15, 2026 16:39
@joelriou
definition of spectral objects
aa67927
@joelriou
cycles
9dc5eee
@joelriou
year
7de1402
@joelriou
cycles-2
40e2f86
@joelriou
fix
b2691cb
@joelriou
fix
7eb17ab
@joelriou
fix
6f1c0d4
@joelriou
fix
fda2bdf
@joelriou
Merge remote-tracking branch 'origin/master' into spectral-sequences-…
2cb2c7c 
…2-cycles-1
@joelriou
Merge remote-tracking branch 'origin/spectral-sequences-2-cycles-1' i…
7b74d4d 
…nto spectral-sequences-2-cycles-2
@joelriou
Merge remote-tracking branch 'origin/spectral-sequences-2-cycles-2' i…
da149f3 
…nto spectral-sequences-2-page-1
@joelriou
Merge remote-tracking branch 'origin/spectral-sequences-2-cycles-2' i…
ce80f90 
…nto spectral-sequences-2-page-1
@joelriou
Merge remote-tracking branch 'origin/master' into spectral-sequences-…
274bf33 
…2-cycles-1
@joelriou
autoparams
8c103e5
@joelriou
whitespace
8a15deb
@joelriou
cat_disch autoparam
518e7bf
@joelriou @robin-carlier
Update Mathlib/Algebra/Homology/SpectralObject/Cycles.lean
b0f5bff 
Co-authored-by: Robin Carlier <[email protected]>
@joelriou @robin-carlier
Update Mathlib/Algebra/Homology/SpectralObject/Cycles.lean
ecd5916 
Co-authored-by: Robin Carlier <[email protected]>
@joelriou @robin-carlier
Update Mathlib/Algebra/Homology/SpectralObject/Cycles.lean
d2dd6bf 
Co-authored-by: Robin Carlier <[email protected]>
@joelriou @robin-carlier
Update Mathlib/Algebra/Homology/SpectralObject/Cycles.lean
ee72590 
Co-authored-by: Robin Carlier <[email protected]>
@joelriou
reverted some autoparams
93c4e91
@joelriou
Merge remote-tracking branch 'origin/spectral-sequences-2-cycles-1' i…
afb68d5 
…nto spectral-sequences-2-cycles-2
@joelriou
Merge remote-tracking branch 'origin/master' into spectral-sequences-…
fa567c0 
…2-cycles-2
@joelriou
Merge remote-tracking branch 'origin/spectral-sequences-2-cycles-2' i…
edffdbc 
…nto spectral-sequences-2-page-1
@joelriou
wip
5235711
@joelriou
feat(Algebra/Homology): exact sequences for SpectralObject.E
3cf43e5
@joelriou
wip
0064c68
@joelriou
feat(Algebra/Homology/SpectralObject): differentials on pages
cfe51e2
@joelriou
Merge remote-tracking branch 'origin/master' into spectral-sequences-…
945a120 
…2-page-1
@joelriou
Merge remote-tracking branch 'origin/master' into spectral-sequences-…
65f3e83 
…2-page-1
joelriou and others added 6 commits March 13, 2026 09:43
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Mar 13, 2026

Thanks @smorel394 and @robin-carlier for the reviews!

@joelriou joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 13, 2026
@robin-carlier
Copy link
Copy Markdown
Contributor

robin-carlier commented Mar 13, 2026

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 13, 2026

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

trigger_name: issue_comment
wf_run: workflow_run

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 13, 2026
@faenuccio faenuccio self-assigned this Mar 13, 2026
faenuccio
faenuccio reviewed Mar 13, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@faenuccio faenuccio left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! I've added some mostly cosmetic comments.

Mathlib/Algebra/Homology/SpectralObject/Homology.lean
(X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃).Exact := by
rw [ShortComplex.exact_iff_exact_up_to_refinements]
intro A x₂ hx₂
dsimp at hx₂ ⊢
Copy link
Copy Markdown
Contributor

@faenuccio faenuccio Mar 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
dsimp at hx₂ ⊢
dsimp only [dCokernelSequence_X₃, dCokernelSequence_X₂, dCokernelSequence_g, dCokernelSequence_X₁,
dCokernelSequence_f] at hx₂ ⊢

Copy link
Copy Markdown
Contributor Author

@joelriou joelriou Mar 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We usually do not squeeze the (nonterminal) dsimp in category theory.

Copy link
Copy Markdown
Contributor

@faenuccio faenuccio Mar 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh I see. Why so?

Copy link
Copy Markdown
Contributor Author

@joelriou joelriou Mar 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When a specific lemma is used, it can be emphasized by using the syntax dsimp [...], but when it is not needed, a plain dsimp makes the code more readable, and more immune to changes in upstream code. This is also consistent with the recently added dsimp% elaborator #36043.

@faenuccio faenuccio added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 13, 2026
@joelriou joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 13, 2026
@faenuccio
Copy link
Copy Markdown
Contributor

faenuccio commented Mar 13, 2026

@joelriou Can you check CI?

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Mar 13, 2026 •
edited
Loading

@joelriou Can you check CI?

Thanks for reviews! The CI errors seems unrelated to the PR. I am trying to relaunch it.

@faenuccio
Copy link
Copy Markdown
Contributor

faenuccio commented Mar 17, 2026

Thanks!

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 17, 2026
@joelriou
feat(Algebra/Homology/SpectralObject): homology of the differentials (#…
6e77ee2 
…36182)
@mathlib-triage mathlib-triage bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 17, 2026
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 17, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Homology/SpectralObject): homology of the differentials [Merged by Bors] - feat(Algebra/Homology/SpectralObject): homology of the differentials Mar 17, 2026
@mathlib-bors mathlib-bors bot closed this Mar 17, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@robin-carlier robin-carlier robin-carlier left review comments

@faenuccio faenuccio faenuccio left review comments

+1 more reviewer

@smorel394 smorel394 smorel394 left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@faenuccio faenuccio

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@joelriou @smorel394 @robin-carlier @faenuccio