Skip to content

[Merged by Bors] - feat(Algebra/Homology/SpectralObject): first quadrant spectral objects#35375

Closed
joelriou wants to merge 56 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-2-first-quadrant
Closed

[Merged by Bors] - feat(Algebra/Homology/SpectralObject): first quadrant spectral objects#35375
joelriou wants to merge 56 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-2-first-quadrant

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Feb 15, 2026 •
edited
Loading

@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Feb 15, 2026
@mathlib-dependent-issues 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
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 15, 2026 •
edited
Loading

PR summary b187818844

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsFirstQuadrant
+ IsThirdQuadrant
+ instance : Y.HasSpectralSequence coreE₂CohomologicalNat
+ instance : Y.HasSpectralSequence coreE₂HomologicalNat
+ isZero₁_of_isFirstQuadrant
+ isZero₁_of_isThirdQuadrant
+ isZero₂_of_isFirstQuadrant
+ isZero₂_of_isThirdQuadrant

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

@joelriou joelriou mentioned this pull request Feb 15, 2026
Open
43 tasks
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Feb 19, 2026

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

@mathlib-merge-conflicts 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 19, 2026
@github-actions 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
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 3, 2026

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

@mathlib-merge-conflicts 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 Mar 3, 2026
@joelriou joelriou removed the WIP Work in progress label Mar 6, 2026
smorel394
smorel394 reviewed Mar 6, 2026
View reviewed changes
smorel394
smorel394 reviewed Mar 6, 2026
View reviewed changes
smorel394
smorel394 reviewed Mar 6, 2026
View reviewed changes
smorel394
smorel394 reviewed Mar 6, 2026
View reviewed changes
smorel394
smorel394 reviewed Mar 6, 2026
View reviewed changes
smorel394
smorel394 reviewed Mar 6, 2026
View reviewed changes
smorel394
smorel394 reviewed Mar 6, 2026
View reviewed changes
smorel394
smorel394 reviewed Mar 6, 2026
View reviewed changes
@smorel394
Copy link
Copy Markdown
Collaborator

smorel394 commented Mar 6, 2026

I made suggestions that should save a few lines, but they're kind of stupid.
Otherwise it looks fine to me.

joelriou and others added 8 commits March 6, 2026 23:15
@joelriou @smorel394
Update Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
d9ffee9 
Co-authored-by: smorel394 <[email protected]>
@joelriou @smorel394
Update Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
5494c64 
Co-authored-by: smorel394 <[email protected]>
@joelriou @smorel394
Update Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
96b251d 
Co-authored-by: smorel394 <[email protected]>
@joelriou @smorel394
Update Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
45a0183 
Co-authored-by: smorel394 <[email protected]>
@joelriou @smorel394
Update Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
9abb977 
Co-authored-by: smorel394 <[email protected]>
@joelriou @smorel394
Update Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
93a2d46 
Co-authored-by: smorel394 <[email protected]>
@joelriou @smorel394
Update Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
8b13a0b 
Co-authored-by: smorel394 <[email protected]>
@joelriou @smorel394
Update Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
854797d 
Co-authored-by: smorel394 <[email protected]>
robin-carlier
robin-carlier approved these changes Mar 8, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@robin-carlier robin-carlier left a comment •
edited
Loading

Choose a reason for hiding this comment

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

Thanks!

maintainer merge

@robin-carlier
Copy link
Copy Markdown
Contributor

robin-carlier commented Mar 9, 2026

The bot was asleep.

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 9, 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 9, 2026
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Mar 12, 2026

Thanks!

bors merge

@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 12, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 12, 2026
@joelriou
feat(Algebra/Homology/SpectralObject): first quadrant spectral objects (
0791ac7 
#35375)

When a spectral object indexed by the extended integers lies on the first quadrant (typeclass `IsFirstQuadrant`), it will be possible to construct a spectral sequence where the objects on the pages are indexed by `ℕ × ℕ` (TODO).
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 12, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Homology/SpectralObject): first quadrant spectral objects [Merged by Bors] - feat(Algebra/Homology/SpectralObject): first quadrant spectral objects Mar 12, 2026
@mathlib-bors mathlib-bors bot closed this Mar 12, 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 approved these changes

+1 more reviewer

@smorel394 smorel394 smorel394 left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. 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 @riccardobrasca