[Merged by Bors] - feat(Algebra/Homology/SpectralObject): construction of the objects on the pages of the spectral sequence by joelriou · Pull Request #35378 · leanprover-community/mathlib4

joelriou · 2026-02-15T17:49:51Z

Given a spectral object X in an abelian category, we define the objects which shall appear on the various pages of the spectral sequence attached to X.

depends on: [Merged by Bors] - feat(Algebra/Homology/SpectralObject): cycles as cokernels and opcycles as kernels #35361
depends on: [Merged by Bors] - feat(Algebra/Homology/SpectralObject): kernel and cokernel of differentials #35359
depends on: [Merged by Bors] - feat(Algebra/Homology): definition of spectral objects in abelian categories #35357

github-actions · 2026-02-15T17:51:00Z

PR summary 74706992da

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Homology.SpectralObject.Page` (new file)	839

Declarations diff

+ E
+ cokernelSequenceCyclesE
+ cokernelSequenceCyclesEIso
+ cokernelSequenceCyclesE_exact
+ cyclesIso
+ cyclesIso_hom_i
+ cyclesIso_inv_i
+ instance (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) :
+ isIso_map
+ isZero_E_of_isZero_H
+ isZero_H_obj_of_isIso
+ leftHomologyDataShortComplexE
+ leftHomologyDataShortComplexE_f'
+ map
+ map_comp
+ map_id
+ rightHomologyDataShortComplexE
+ rightHomologyDataShortComplexE_g'
+ shortComplex
+ shortComplexMap
+ shortComplexMap_comp
+ shortComplexMap_id
+ δToCycles_cyclesIso_inv
+ δToCycles_πE
+ δ_eq_zero_of_isIso₁
+ δ_eq_zero_of_isIso₂
+ πE

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.

Increase in tech debt: (relative, absolute) = (11.00, 0.00)

Current number	Change	Type
10020	11	backward.isDefEq

Current commit a29cfa1b35
Reference commit 74706992da

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).

mathlib-merge-conflicts · 2026-02-25T08:33:40Z

This pull request has conflicts, please merge master and resolve them.

…2-cycles-1

…nto spectral-sequences-2-cycles-2

…nto spectral-sequences-2-page-1

…2-cycles-1

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

mathlib-dependent-issues · 2026-03-03T11:13:05Z

This PR/issue depends on:

~~[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 spectral objects in abelian categories #35357~~
By Dependent Issues (🤖). Happy coding!

…2-page-1

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

robin-carlier

Thanks!

maintainer delegate

github-actions · 2026-03-04T11:24:33Z

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

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

riccardobrasca · 2026-03-04T12:06:37Z

Thanks!

bors merge

… the pages of the spectral sequence (#35378) Given a spectral object `X` in an abelian category, we define the objects which shall appear on the various pages of the spectral sequence attached to `X`.

mathlib-bors · 2026-03-04T15:44:11Z

Pull request successfully merged into master.

Build succeeded:

… the pages of the spectral sequence (leanprover-community#35378) Given a spectral object `X` in an abelian category, we define the objects which shall appear on the various pages of the spectral sequence attached to `X`.

joelriou added 5 commits February 15, 2026 16:39

definition of spectral objects

aa67927

cycles

9dc5eee

year

7de1402

cycles-2

40e2f86

fix

b2691cb

joelriou added WIP Work in progress t-category-theory Category theory labels Feb 15, 2026

joelriou mentioned this pull request Feb 15, 2026

[Merged by Bors] - feat(Algebra/Homology): spectral sequences #33842

Closed

43 tasks

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Feb 15, 2026

joelriou added 2 commits February 15, 2026 18:51

fix

7eb17ab

fix

6f1c0d4

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

joelriou changed the title ~~feat(Algebra/Homology/SpectralObject): construction of the objects on the page of the spectral sequence~~ feat(Algebra/Homology/SpectralObject): construction of the objects on the pages of the spectral sequence Feb 15, 2026

fix

fda2bdf

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 25, 2026

joelriou added 4 commits February 28, 2026 15:41

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

2cb2c7c

…2-cycles-1

Merge remote-tracking branch 'origin/spectral-sequences-2-cycles-1' i…

7b74d4d

…nto spectral-sequences-2-cycles-2

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

da149f3

…nto spectral-sequences-2-page-1

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

ce80f90

…nto spectral-sequences-2-page-1

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 28, 2026

joelriou and others added 8 commits March 2, 2026 13:47

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

274bf33

…2-cycles-1

autoparams

8c103e5

whitespace

8a15deb

cat_disch autoparam

518e7bf

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

b0f5bff

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

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

ecd5916

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

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

d2dd6bf

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

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

ee72590

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

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

945a120

…2-page-1

joelriou removed the WIP Work in progress label Mar 3, 2026

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

65f3e83

…2-page-1

robin-carlier reviewed Mar 3, 2026

View reviewed changes

joelriou and others added 4 commits March 3, 2026 17:47

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

ef87071

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

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

bf38d26

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

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

878bb8d

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

rename

03d3aaf

joelriou commented Mar 4, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Homology/SpectralObject/Page.lean Outdated

Apply suggestion from @joelriou

ec5e9fa

robin-carlier reviewed Mar 4, 2026

View reviewed changes

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 4, 2026

joelriou and others added 8 commits March 4, 2026 11:35

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

16f7990

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

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

159d58d

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

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

97743ca

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

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

a29cfa1

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

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

c34b035

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

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

e33a518

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

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

be06f26

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

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

b2e43b5

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

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 4, 2026

mathlib-bors bot changed the title ~~feat(Algebra/Homology/SpectralObject): construction of the objects on the pages of the spectral sequence~~ [Merged by Bors] - feat(Algebra/Homology/SpectralObject): construction of the objects on the pages of the spectral sequence Mar 4, 2026

mathlib-bors bot closed this Mar 4, 2026

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 74706992da

Import changes for modified files

Declarations diff

Uh oh!

mathlib-merge-conflicts bot commented Feb 25, 2026

Uh oh!

mathlib-dependent-issues bot commented Mar 3, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

robin-carlier left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Mar 4, 2026

Uh oh!

riccardobrasca commented Mar 4, 2026

Uh oh!

mathlib-bors bot commented Mar 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

joelriou commented Feb 15, 2026 •

edited

Loading

github-actions bot commented Feb 15, 2026 •

edited

Loading