feat(Algebra/Homology/SpectralObject): first quadrant spectral objects

[joelriou]

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

---

• depends on: feat(Algebra/Homology/SpectralObject): HasSpectralSequence #35374
• depends on: feat(Order/Fin): lemmas about Fin.clamp #35373
• depends on: feat(Algebra/Homology/SpectralObject): SpectralSequenceMkData #35372
• depends on: feat(Algebra/Homology): definition of spectral objects in abelian categories #35357
• depends on: feat(Algebra/Homology/SpectralSequence): complex shapes for pages of spectral sequences #35355

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Algebra/Homology/SpectralObject): HasSpectralSequence #35374
• feat(Order/Fin): lemmas about Fin.clamp #35373
• feat(Algebra/Homology/SpectralObject): SpectralSequenceMkData #35372
• feat(Algebra/Homology): definition of spectral objects in abelian categories #35357
• feat(Algebra/Homology/SpectralSequence): complex shapes for pages of spectral sequences #35355
  By Dependent Issues (🤖). Happy coding!

[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.SpectralSequence.ComplexShape (new file)	101
Mathlib.Order.Fin.Clamp (new file)	342
Mathlib.Algebra.Homology.SpectralObject.Basic (new file)	781
Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (new file)	786

---

Declarations diff

+ HasSpectralSequence
+ Hom
+ IsFirstQuadrant
+ IsThirdQuadrant
+ SpectralObject
+ SpectralSequenceMkData
+ composableArrows₅
+ composableArrows₅_exact
+ epi_H_map_twoδ₁Toδ₀
+ epi_H_map_twoδ₁Toδ₀'
+ exact₁
+ exact₂
+ exact₃
+ instance (E : SpectralObject C EInt) : E.HasSpectralSequence mkDataE₂Cohomological
+ instance : Category (SpectralObject C ι)
+ instance : Y.HasSpectralSequence mkDataE₂CohomologicalNat
+ instance : Y.HasSpectralSequence mkDataE₂HomologicalNat
+ instance {l : ℕ} (E : SpectralObject C (Fin (l + 1))) :
+ isIso_H_map_twoδ₁Toδ₀
+ isIso_H_map_twoδ₁Toδ₀'
+ isZero_H_map_mk₁_of_isIso
+ isZero_H_obj_mk₁_i₀_le
+ isZero_H_obj_mk₁_i₀_le'
+ isZero_H_obj_mk₁_i₃_le
+ isZero_H_obj_mk₁_i₃_le'
+ isZero₁_of_isFirstQuadrant
+ isZero₁_of_isThirdQuadrant
+ isZero₂_of_isFirstQuadrant
+ isZero₂_of_isThirdQuadrant
+ i₀_le
+ i₃_le
+ le₀'₀
+ le₀₁'
+ le₁₂'
+ le₂₃'
+ le₃₃'
+ mkDataE₂Cohomological
+ mkDataE₂CohomologicalFin
+ mkDataE₂CohomologicalNat
+ mkDataE₂HomologicalNat
+ mono_H_map_twoδ₁Toδ₀
+ mono_H_map_twoδ₁Toδ₀'
+ sc₁
+ sc₂
+ sc₃
+ spectralSequenceFin
+ spectralSequenceFin_rel_iff
+ spectralSequenceNat
+ spectralSequenceNat_rel_iff
+ 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).