Stabilization of the pages of the spectral sequence of a filtered complex

Let F : ℤ → Subobject K be an increasing filtration of a cochain complex K. On the spectral sequence of CochainComplex.filtrationFunctor F hF, the object at (p, q) on page r ≥ 2 is isomorphic to the limit object E^{p+q}(⊥ ≤ q ≤ q + 1 ≤ ⊤) as soon as H^{p+q+1}(F_{q-r+2}) = 0 and H^{p+q-1}(K / F_{q+r-1}) = 0 (CochainComplex.filtrationSpectralSequencePageXIsoEInfty). For a finite filtration, F_a = ⊥ and F_b = ⊤, this holds on every page r with q - r + 2 ≤ a and b ≤ q + r - 1 (CochainComplex.filtrationSpectralSequencePageXIsoEInftyOfFinite).

Main results

• CochainComplex.isZero_spectralObject_H_bot, CochainComplex.isZero_spectralObject_H_top: the vanishing of H^m(⊥ ≤ a) and H^m(b ≤ ⊤) for the spectral object of a filtration, from the vanishing of H^m(F_a) and H^m(K / F_b).
• CochainComplex.filtrationSpectralSequencePageXIsoEInfty: identification of the page objects with EInfty under the two vanishing conditions.
• CochainComplex.filtrationSpectralSequencePageXIsoEInftyOfFinite: the case of a finite filtration.

theorem CochainComplex.isZero_spectralObject_H_bot {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (a m : ℤ) (h : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Subobject.underlying.obj (F a)) m)) : CategoryTheory.Limits.IsZero (((spectralObject (filtrationFunctor F hF)).H m).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))

H^m(⊥ ≤ a) vanishes for the spectral object of a filtration when H^m(F_a) does.

theorem CochainComplex.isZero_spectralObject_H_top {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (b m : ℤ) (h : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel (F b).arrow) m)) : CategoryTheory.Limits.IsZero (((spectralObject (filtrationFunctor F hF)).H m).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))

H^m(b ≤ ⊤) vanishes for the spectral object of a filtration when H^m(K / F_b) does.

noncomputable def CochainComplex.filtrationSpectralSequencePageXIsoEInfty {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (r : ℤ) (hr : 2 ≤ r) (pq : ℤ × ℤ) (n : ℤ) (hn : n = pq.1 + pq.2) (h₀ : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Subobject.underlying.obj (F (pq.2 - r + 2))) (n + 1))) (h₃ : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel (F (pq.2 + r - 1)).arrow) (n - 1))) : ((spectralSequence (filtrationFunctor F hF)).page r ⋯).X pq ≅ (spectralObject (filtrationFunctor F hF)).EInfty pq.2 n

Stabilization of the pages of the spectral sequence of a filtered complex. The object at pq = (p, q) on page r ≥ 2 is E^{p+q}(⊥ ≤ q ≤ q + 1 ≤ ⊤) when H^{p+q+1}(F_{q-r+2}) and H^{p+q-1}(K / F_{q+r-1}) vanish.

noncomputable def CochainComplex.filtrationSpectralSequencePageXIsoEInftyOfFinite {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) {a b : ℤ} (ha : F a = ⊥) (hb : F b = ⊤) (r : ℤ) (hr : 2 ≤ r) (pq : ℤ × ℤ) (hra : pq.2 - r + 2 ≤ a) (hrb : b ≤ pq.2 + r - 1) : ((spectralSequence (filtrationFunctor F hF)).page r ⋯).X pq ≅ (spectralObject (filtrationFunctor F hF)).EInfty pq.2 (pq.1 + pq.2)

Stabilization for a finite filtration. If F_a = ⊥ and F_b = ⊤, then the object at pq = (p, q) on every page r ≥ 2 with q - r + 2 ≤ a and b ≤ q + r - 1 is E^{p+q}(⊥ ≤ q ≤ q + 1 ≤ ⊤).