feat(Algebra/Homology/SpectralObject): SpectralSequenceMkData

[joelriou]

In this file, we introduce a structure SpectralSequenceMkData which contains a recipe for the construction of the pages of the spectral sequence attached to a spectral object.

---

• depends on: feat(Algebra/Homology): definition of spectral objects in abelian categories #35357

[github-actions]

PR summary 99884c2730

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Homology.SpectralObject.Basic (new file)	781
Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (new file)	784

---

Declarations diff

+ Hom
+ SpectralObject
+ SpectralSequenceMkData
+ composableArrows₅
+ composableArrows₅_exact
+ epi_H_map_twoδ₁Toδ₀
+ epi_H_map_twoδ₁Toδ₀'
+ exact₁
+ exact₂
+ exact₃
+ instance : Category (SpectralObject C ι)
+ isIso_H_map_twoδ₁Toδ₀
+ isIso_H_map_twoδ₁Toδ₀'
+ isZero_H_map_mk₁_of_isIso
+ i₀_le
+ i₃_le
+ le₀'₀
+ le₀₁'
+ le₁₂'
+ le₂₃'
+ le₃₃'
+ mkDataE₂Cohomological
+ mono_H_map_twoδ₁Toδ₀
+ mono_H_map_twoδ₁Toδ₀'
+ sc₁
+ sc₂
+ sc₃
+ zero₁
+ zero₂
+ zero₃
+ δ
+ δ_naturality
+ δ_δ

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/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-dependent-issues]

This PR/issue depends on:

• feat(Algebra/Homology): definition of spectral objects in abelian categories #35357
  By Dependent Issues (🤖). Happy coding!