feat(Algebra/Homology/SpectralObject): kernel and cokernel of differentials

[joelriou]

---

• 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

---

Declarations diff

+ Hom
+ SpectralObject
+ cokernelSequenceOpcycles
+ cokernelSequenceOpcycles_exact
+ composableArrows₅
+ composableArrows₅_exact
+ cycles
+ cyclesMap
+ cyclesMap_comp
+ cyclesMap_i
+ cyclesMap_id
+ descOpcycles
+ epi_H_map_twoδ₁Toδ₀
+ epi_H_map_twoδ₁Toδ₀'
+ exact₁
+ exact₂
+ exact₃
+ iCycles
+ iCycles_δ
+ instance : Category (SpectralObject C ι)
+ instance : Epi (X.cokernelSequenceOpcycles n₀ n₁ hn₁ f g).g := by
+ instance : Epi (X.pOpcycles n f g) := by
+ instance : Mono (X.iCycles n f g) := by
+ instance : Mono (X.kernelSequenceCycles n₀ n₁ hn₁ f g).f := by
+ isIso_H_map_twoδ₁Toδ₀
+ isIso_H_map_twoδ₁Toδ₀'
+ isZero_H_map_mk₁_of_isIso
+ isZero_cycles
+ isZero_opcycles
+ kernelSequenceCycles
+ kernelSequenceCycles_exact
+ liftCycles
+ liftCycles_i
+ mono_H_map_twoδ₁Toδ₀
+ mono_H_map_twoδ₁Toδ₀'
+ opcycles
+ opcyclesMap
+ opcyclesMap_comp
+ opcyclesMap_id
+ pOpcycles
+ p_descOpcycles
+ p_opcyclesMap
+ sc₁
+ sc₂
+ sc₃
+ zero₁
+ zero₂
+ zero₃
+ δ
+ δ_naturality
+ δ_pOpcycles
+ δ_δ

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!