Skip to content

[Merged by Bors] - feat(Algebra/Homology): more API for SpectralObject.E#36030

Closed
joelriou wants to merge 61 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-2-page-3
Closed

[Merged by Bors] - feat(Algebra/Homology): more API for SpectralObject.E#36030
joelriou wants to merge 61 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-2-page-3

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Mar 3, 2026 •
edited
Loading

joelriou and others added 27 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 joelriou added the t-category-theory Category theory label Mar 3, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 3, 2026 •
edited
Loading

PR summary 998cee5034

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ EIsoH
+ EIsoH_hom_naturality
+ EIsoH_hom_opcyclesIsoH_inv
+ EToCycles
+ EToCycles_i
+ cyclesIsoH
+ cyclesIsoH_hom_EIsoH_inv
+ cyclesIsoH_hom_inv_id
+ cyclesIsoH_inv
+ cyclesIsoH_inv_hom_id
+ homologyDataIdId
+ kernelSequenceCyclesE
+ kernelSequenceCyclesE_exact
+ opcyclesIsoH
+ opcyclesIsoH_hom
+ opcyclesIsoH_hom_inv_id
+ opcyclesIsoH_inv_hom_id
+ opcyclesMap_threeδ₂Toδ₁_opcyclesToE
+ opcyclesToE_map
+ shortComplexOpcyclesThreeδ₂Toδ₁
+ shortComplexOpcyclesThreeδ₂Toδ₁_exact
+ shortComplexOpcyclesThreeδ₂Toδ₁_shortExact
+ πE_EToCycles
++ instance (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) :
++ instance (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) :

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) = (7.00, 0.00)
Current number Change Type
10067 7 backward.isDefEq

Current commit ded4fbb5bd
Reference commit 998cee5034

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

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Mar 3, 2026
robin-carlier
robin-carlier reviewed Mar 5, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@robin-carlier robin-carlier left a comment

Choose a reason for hiding this comment

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

Thanks!

@github-actions github-actions 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 5, 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 Mar 5, 2026
@mathlib-dependent-issues 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 Mar 5, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 5, 2026

This PR/issue depends on:

@robin-carlier
Copy link
Copy Markdown
Contributor

robin-carlier commented Mar 5, 2026

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 5, 2026

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

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 5, 2026
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Mar 5, 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 5, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 5, 2026
@joelriou
feat(Algebra/Homology): more API for SpectralObject.E (#36030)
f7e6e89
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 5, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Homology): more API for SpectralObject.E [Merged by Bors] - feat(Algebra/Homology): more API for SpectralObject.E Mar 5, 2026
@mathlib-bors mathlib-bors bot closed this Mar 5, 2026
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 9, 2026
@joelriou @xroblot
feat(Algebra/Homology): more API for SpectralObject.E (leanprover-c…
3547251 
…ommunity#36030)
seewoo5 pushed a commit to seewoo5/mathlib4 that referenced this pull request Mar 9, 2026
@joelriou @seewoo5
feat(Algebra/Homology): more API for SpectralObject.E (leanprover-c…
1035c7b 
…ommunity#36030)
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 10, 2026
@joelriou @xroblot
feat(Algebra/Homology): more API for SpectralObject.E (leanprover-c…
af1daa5 
…ommunity#36030)
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

Assignees

No one assigned

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.

3 participants

@joelriou @robin-carlier @riccardobrasca