feat(Algebra/Homology/SpectralObject): construction of the objects on the pages of the spectral sequence

[joelriou]

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: feat(Algebra/Homology/SpectralObject): cycles as cokernels and opcycles as kernels #35361
• depends on: feat(Algebra/Homology/SpectralObject): kernel and cokernel of differentials #35359
• 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.Cycles (new file)	833
Mathlib.Algebra.Homology.SpectralObject.Page (new file)	837

---

Declarations diff

+ E
+ EMap
+ EMap_comp
+ EMap_id
+ H_map_twoδ₂Toδ₁_toCycles
+ Hom
+ SpectralObject
+ cokernelIsoCycles
+ cokernelIsoCycles_hom_fac
+ cokernelSequenceCycles
+ cokernelSequenceCycles_exact
+ cokernelSequenceOpcycles
+ cokernelSequenceOpcycles_exact
+ composableArrows₅
+ composableArrows₅_exact
+ cycles
+ cyclesMap
+ cyclesMap_comp
+ cyclesMap_i
+ cyclesMap_id
+ descCycles
+ descOpcycles
+ epi_H_map_twoδ₁Toδ₀
+ epi_H_map_twoδ₁Toδ₀'
+ exact₁
+ exact₂
+ exact₃
+ fromOpcycles
+ fromOpcycles_H_map_twoδ₁Toδ₀
+ fromOpcyles_δ
+ iCycles
+ iCycles_δ
+ instance : Category (SpectralObject C ι)
+ instance : Epi (X.cokernelSequenceCycles n f g fg h).g := by
+ instance : Epi (X.cokernelSequenceOpcycles n₀ n₁ hn₁ f g).g := by
+ instance : Epi (X.pOpcycles n f g) := by
+ instance : Epi (X.toCycles n f g fg h)
+ instance : Mono (X.fromOpcycles n f g fg h)
+ instance : Mono (X.iCycles n f g) := by
+ instance : Mono (X.kernelSequenceCycles n₀ n₁ hn₁ f g).f := by
+ instance : Mono (X.kernelSequenceOpcycles n f g fg h).f := by
+ isIso_EMap
+ isIso_H_map_twoδ₁Toδ₀
+ isIso_H_map_twoδ₁Toδ₀'
+ isIso_fromOpcycles
+ isIso_toCycles
+ isZero_E_of_isZero_H
+ isZero_H_map_mk₁_of_isIso
+ isZero_H_obj_of_isIso
+ isZero_cycles
+ isZero_opcycles
+ kernelSequenceCycles
+ kernelSequenceCycles_exact
+ kernelSequenceOpcycles
+ kernelSequenceOpcycles_exact
+ liftCycles
+ liftCycles_i
+ liftOpcycles
+ liftOpcycles_fromOpcycles
+ mono_H_map_twoδ₁Toδ₀
+ mono_H_map_twoδ₁Toδ₀'
+ opcycles
+ opcyclesIsoKernel
+ opcyclesIsoKernel_hom_fac
+ opcyclesMap
+ opcyclesMap_comp
+ opcyclesMap_fromOpcycles
+ opcyclesMap_id
+ pOpcycles
+ pOpcycles_δFromOpcycles
+ p_descOpcycles
+ p_fromOpcycles
+ p_opcyclesMap
+ sc₁
+ sc₂
+ sc₃
+ shortComplexE
+ shortComplexEMap
+ shortComplexEMap_comp
+ shortComplexEMap_id
+ toCycles
+ toCycles_cyclesMap
+ toCycles_descCycles
+ toCycles_i
+ zero₁
+ zero₂
+ zero₃
+ δ
+ δFromOpcycles
+ δToCycles
+ δToCycles_iCycles
+ δ_eq_zero_of_isIso₁
+ δ_eq_zero_of_isIso₂
+ δ_naturality
+ δ_pOpcycles
+ δ_toCycles
+ δ_δ

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/SpectralObject): cycles as cokernels and opcycles as kernels #35361
• feat(Algebra/Homology/SpectralObject): kernel and cokernel of differentials #35359
• feat(Algebra/Homology): definition of spectral objects in abelian categories #35357
  By Dependent Issues (🤖). Happy coding!