feat(Algebra/Homology): spectral sequences by joelriou · Pull Request #33842 · leanprover-community/mathlib4

joelriou · 2026-01-11T15:37:39Z

This PR concludes a series of 44 PRs which contains two mostly independent developments:

The construction of the spectral object attached to objects in a triangulated category C equipped with a t-structure;
The definition of a category of spectral sequences and the construction of the spectral sequence attached to a spectral object indexed by the extended integers (the integers with +/- infinity) in an abelian category, and this very PR adds the computation of the first page of the spectral sequence.

We now have two ways to construct a spectral object in triangulated categories (the spectral object attached to a filtered complex, and the spectral object attached to a t-structure 1.). After applying a homological functor to these spectral objects, we obtain a spectral object in an abelian category, and the construction 2. allows to define spectral sequences. When more results are obtained about derived functors, the hypercohomology spectral sequence and the Grothendieck spectral sequence of composition of derived functors shall follow.

The study of the stabilization and convergence of spectral sequences is not yet included (even though all the necessary code appears in #25848).

The mathematical material is discussed in https://hal.science/hal-04546712v5 (§5.4.1 and §5.4.4).

Dependency graph: https://jriou.org/tmp/spectral-sequences.pdf

The construction of the spectral object attached to objects in a triangulated category C equipped with a t-structure;

The definition of a category of spectral sequences and the construction of the spectral sequence attached to a spectral object indexed by the extended integers (the integers with +/- infinity) in an abelian category.

Prerequisites:

github-actions · 2026-01-11T15:38:49Z

PR summary 7d837a8020

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Homology.SpectralObject.FirstPage` (new file)	979

Declarations diff

+ HasFirstPageComputation
+ instance : coreE₂Cohomological.HasFirstPageComputation
+ instance : coreE₂CohomologicalNat.HasFirstPageComputation
+ instance : coreE₂HomologicalNat.HasFirstPageComputation
+ spectralSequenceFirstPageXIso
+ spectralSequenceFirstPageXIso_hom
+ spectralSequenceFirstPageXIso_inv
+ spectralSequence_first_page_d_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

…2-spectral-sequence-2

Co-authored-by: Robin Carlier <[email protected]>

…2-spectral-sequence-2

…quence-2' into spectral-sequences

mathlib-dependent-issues · 2026-04-04T12:48:31Z

This PR/issue depends on:

~~[Merged by Bors] - feat(CategoryTheory/Triangulated/TStructure): the spectral object #35370~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated/TStructure): properties of truncations indexed by EInt that use the octahedron axiom #35369~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated/TStructure): extensions of truncations to the extended integers #35368~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated/TStucture): induced t-structures #35367~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated/TStructure): truncLE and truncGT #35364~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated/TStructure): properties of truncLT and truncGE which use the octahedron axiom #35363~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated/TStructure): more on truncLT and truncGE #35362~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralObject): the spectral sequence #36555~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralObject): starting the construction of the spectral sequence #36550~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralObject): homology of the differentials #36182~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralObject): induced morphisms that are epi/mono #36153~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralObject): differentials on pages #36032~~
~~[Merged by Bors] - feat(Algebra/Homology): more API for SpectralObject.E #36030~~
~~[Merged by Bors] - feat(Algebra/Homology): exact sequences for SpectralObject.E #36029~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralObject): construction of the objects on the pages of the spectral sequence #35378~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralObject): cycles as cokernels and opcycles as kernels #35361~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralObject): kernel and cokernel of differentials #35359~~
~~[Merged by Bors] - feat(Algebra/Homology): definition of the category of spectral sequences #35356~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralObject): first quadrant spectral objects #35375~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralObject): HasSpectralSequence #35374~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralSequence): complex shapes for pages of spectral sequences #35355~~
~~[Merged by Bors] - feat(Algebra/Homology/SpectralObject): SpectralSequenceDataCore #35372~~
~~[Merged by Bors] - feat(Algebra/Homology): definition of spectral objects in abelian categories #35357~~
~~[Merged by Bors] - feat(CategoryTheory/Shift): the shift on a full subcategory #34372~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated): bounded objects for a t-structure #34368~~
~~[Merged by Bors] - feat(CategoryTheory/ObjectProperty): stability unfer finite products #34366~~
~~[Merged by Bors] - feat(CategoryTheory): ObjectProperty.lift is additive #34359~~
~~[Merged by Bors] - feat(Algebra/Homology): a homology data from an epi-mono factorization #33875~~
~~[Merged by Bors] - feat(Order): WithBotTop and the extended integers #33876~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated): a triangulated subcategory is a pretriangulated category #34373~~
~~[Merged by Bors] - chore(CategoryTheory/Limits): fix name of Fan.IsLimit.desc #34358~~
~~[Merged by Bors] - feat(Algebra/Homology/ShortComplex): cycles can be computed with a limit kernel fork #33874~~
~~[Merged by Bors] - feat(CategoryTheory/Category/Preorder): isIso_homOfLE #33877~~
~~[Merged by Bors] - feat(CategoryTheory/ComposableArrows): isIso_iff #33879~~
~~[Merged by Bors] - feat(CategoryTheory/ComposableArrows): API for the composition of three arrows #33880~~
~~[Merged by Bors] - feat(CategoryTheory/ComposableArrows): API for the composition of four arrows #33881~~
~~[Merged by Bors] - feat(Algebra/Homology): exact sequences with four terms #33437~~
~~[Merged by Bors] - feat(CategoryTheory/ObjectProperty): various additions #33883~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated): functors to Triangle #33886~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated): fully faithful triangulated functors #33887~~
~~[Merged by Bors] - feat(CategoryTheory/Shift): more API for NatTrans.CommShift #33888~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated): distinguished_iff_of_isZero #33890~~
~~[Merged by Bors] - feat(Order/Fin): lemmas about Fin.clamp #35373~~
By Dependent Issues (🤖). Happy coding!

joelriou added WIP Work in progress t-category-theory Category theory labels Jan 11, 2026

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 11, 2026

joelriou added 8 commits January 12, 2026 08:35

cleaning up

6f0b12e

whitespace

707e3c9

cleaning up

dfb8b22

cleaning up

4f29428

cleaning up

cf9df8d

cleaning up

76cbc40

cleaning up

127074e

fix

374820e

This was referenced Jan 12, 2026

[Merged by Bors] - feat(Algebra/Homology/ShortComplex): cycles can be computed with a limit kernel fork #33874

Closed

[Merged by Bors] - feat(Algebra/Homology): a homology data from an epi-mono factorization #33875

Closed

feat(Data): the extended integers

46d122e

fix

215b7a3

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 12, 2026

joelriou mentioned this pull request Jan 12, 2026

[Merged by Bors] - feat(CategoryTheory/ObjectProperty): various additions #33883

Closed

fix

e8e22e8

cleaning up

eb9c0e0

github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Mar 22, 2026

joelriou and others added 20 commits March 22, 2026 14:16

fix

8dddf9d

Merge remote-tracking branch 'origin/master' into spectral-sequences-…

99221d6

…2-spectral-sequence-2

Merge remote-tracking branch 'origin/master' into spectral-sequences-…

bb25a55

…2-spectral-sequence-2

Update Mathlib/Algebra/Homology/SpectralObject/SpectralSequence.lean

6cb1888

Co-authored-by: Robin Carlier <[email protected]>

Update Mathlib/Algebra/Homology/SpectralObject/SpectralSequence.lean

d555e38

Co-authored-by: Robin Carlier <[email protected]>

Update Mathlib/Algebra/Homology/SpectralObject/SpectralSequence.lean

e140cd2

Co-authored-by: Robin Carlier <[email protected]>

Update Mathlib/Algebra/Homology/SpectralObject/SpectralSequence.lean

632b836

Co-authored-by: Robin Carlier <[email protected]>

Update Mathlib/Algebra/Homology/SpectralObject/SpectralSequence.lean

3f585e0

Co-authored-by: Robin Carlier <[email protected]>

Apply suggestions from code review

f9c3b08

Co-authored-by: Robin Carlier <[email protected]>

Update Mathlib/Algebra/Homology/SpectralObject/SpectralSequence.lean

db78007

Co-authored-by: Robin Carlier <[email protected]>

Merge remote-tracking branch 'origin/master' into spectral-sequences-…

6dc36ec

…2-spectral-sequence-2

remove auxiliary goals

fdc1947

better syntax

c6db8d8

fix

e20eb11

Merge remote-tracking branch 'origin/master' into spectral-sequences-…

8de894b

…2-spectral-sequence-2

better automation

9f9c059

comment about the user-facing API

88e29b3

make spectralSequence irreducible

e42e53b

removed remark about not unfolded spectralSequence

9303383

Merge remote-tracking branch 'origin/spectral-sequences-2-spectral-se…

54012db

…quence-2' into spectral-sequences

mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 4, 2026

joelriou added 3 commits April 4, 2026 16:27

Merge remote-tracking branch 'origin/master' into spectral-sequences

cdea3b6

cleaning up

aee91ca

Merge remote-tracking branch 'origin/master' into spectral-sequences

66e16c6

joelriou removed the WIP Work in progress label Apr 4, 2026

joelriou added 2 commits April 4, 2026 16:54

fix

3b30ad3

cleaning up

c6ff0e1

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Algebra/Homology): spectral sequences#33842

feat(Algebra/Homology): spectral sequences#33842
joelriou wants to merge 256 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences

joelriou commented Jan 11, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Jan 11, 2026 •

edited

Loading

Declarations diff

Uh oh!

mathlib-dependent-issues bot commented Apr 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

joelriou commented Jan 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 7d837a8020

Import changes for modified files

Declarations diff

Uh oh!

mathlib-dependent-issues bot commented Apr 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

joelriou commented Jan 11, 2026 •

edited

Loading

github-actions bot commented Jan 11, 2026 •

edited

Loading