The spectral sequence of a spectral object #

The main definition in this file is Abelian.SpectralObject.spectralSequence (TODO). Assume that X is a spectral object indexed by ι in an abelian category C, and that we have data : SpectralSequenceDataCore ι c r₀ for a family of complex shapes c : ℤ → ComplexShape κ for a type κ and r₀ : ℤ. Then, under the assumption X.HasSpectralSequence data (see the file Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean), we obtain X.spectralSequence data (TODO) which is a spectral sequence starting on page r₀, such that the rth page (for r₀ ≤ r) is a homological complex of shape c r.

Outline of the construction #

The construction of the spectral sequence is as follows. If r₀ ≤ r and pq : κ, we define the object of the spectral sequence in position pq on the rth page as E^d(i₀ r pq ≤ i₁ pq ≤ i₂ pq ≤ i₃ r pq) where d := data.deg pq and the indices i₀, i₁, i₂, i₃ are given by data (they all depend on pq, and i₀ and i₃ also depend on the page r), see spectralSequencePageXIso.

When (c r).Rel pq pq', the differential from the object in position pq to the object in position pq' on the rth page can be related to the differential X.d of the spectral object (see the lemma spectralSequence_page_d_eq). Indeed, the assumptions that are part of data give equalities of indices i₂ r pq' = i₀ r pq and i₃ pq' = i₁ pq, so that we have a chain of inequalities i₀ r pq' ≤ i₁ pq' ≤ i₂ pq' ≤ i₃ r pq' ≤ i₂ pq ≤ i₃ r pq for which the API of spectral objects provides a differential X.d : E^n(i₀ r pq ≤ i₁ pq ≤ i₂ pq ≤ i₃ r pq) ⟶ E^{n + 1}(i₀ r pq' ≤ i₁ pq' ≤ i₂ pq' ≤ i₃ r pq').

Now, fix r and three positions pq, pq' and pq'' such that pq is the previous object of pq' for c r and pq'' is the next object of pq'. (Note that in case there are no nontrivial differentials to the object pq' for the complex shape c r, according to the homological complex API, we have pq = pq' and the differential is zero. Similarly, when there are no nontrivial differentials from the object in position pq', we have pq'' = pq and the corresponding differential is zero.) In the favourable case where both (c r).Rel pq pq' and (c r).Rel pq' pq'' hold, the definition SpectralObject.SpectralSequence.shortComplexIso in this file can be used in combination to SpectralObject.SpectralSequence.dHomologyIso in order to compute the homology of the differentials.)

In the general case, using the assumptions in X.HasSpectralSequence data, we provide a limit kernel fork kf and a limit cokernel cofork cc of the differentials on the rth page, together with an epi-mono factorization fac which allows to obtain that the homology of the rth page identifies to the next page (see the definitions SpectralObject.SpectralSequence.homologyData (TODO) and SpectralObject.spectralSequenceHomologyData (TODO)).