Convergence of the spectral sequence of a filtered complex

Let F : ℤ → Subobject K be an increasing filtration of a cochain complex K. The abutment H^n(⊥ ≤ ⊤) of the spectral object of F is the cohomology H^n(K) (CochainComplex.filtrationAbutmentIso), filtered by the images of the cohomology of the subcomplexes F_q (Abelian.SpectralObject.abutmentFiltration): through filtrationAbutmentIso, the qth piece is the image of the map H^n(F_q) ⟶ H^n(K) induced by the inclusion (CochainComplex.toFiltrationAbutmentFiltration_comp_filtrationAbutmentIso_hom). The graded pieces of this filtration are the limit objects E^n(⊥ ≤ q ≤ q + 1 ≤ ⊤) (Abelian.SpectralObject.EInftyIsoCokernel).

For a finite filtration (F_a = ⊥ and F_b = ⊤) the spectral sequence converges strongly: the filtration of H^n(K) vanishes at a and is everything at b (CochainComplex.isZero_filtrationAbutmentFiltration, CochainComplex.isIso_filtrationAbutmentFiltrationι), and the page-r object at (p, q) is the graded piece F_{q+1} H^{p+q} / F_q H^{p+q} on every page r with q - r + 2 ≤ a and b ≤ q + r - 1 (CochainComplex.filtrationSpectralSequencePageXIsoGradedOfFinite).

Main results

• CochainComplex.filtrationAbutmentIso: the abutment is H^n(K).
• CochainComplex.toFiltrationAbutmentFiltration: the epimorphism from H^n(F_q) onto the qth piece of the filtration of the abutment, and CochainComplex.toFiltrationAbutmentFiltration_comp_filtrationAbutmentIso_hom: the filtration of the abutment is the image filtration of H^n(K).
• CochainComplex.filtrationSpectralSequencePageXIsoGradedOfFinite: strong convergence for a finite filtration.

noncomputable def CochainComplex.filtrationAbutmentIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (n : ℤ) : (spectralObject (filtrationFunctor F hF)).abutment n ≅ HomologicalComplex.homology K n

The abutment H^n(⊥ ≤ ⊤) of the spectral object of a filtration of K is H^n(K).

theorem CochainComplex.filtrationAbutmentIso_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (n : ℤ) : (filtrationAbutmentIso F hF n).hom = CategoryTheory.CategoryStruct.comp (spectralObjectHIsoCokernel (filtrationFunctor F hF) (CategoryTheory.homOfLE CategoryTheory.Abelian.SpectralObject.abutment._proof_1) n).hom (HomologicalComplex.homologyMap (CategoryTheory.Limits.cokernel.desc ((filtrationFunctor F hF).map (CategoryTheory.homOfLE CategoryTheory.Abelian.SpectralObject.abutment._proof_1)) (filtrationFunctorArrow F hF ⊤) ⋯) n)

The isomorphism filtrationAbutmentIso is induced by the map from the cokernel of F_⊥ ⟶ K, which is zero, to K.

noncomputable def CochainComplex.toFiltrationAbutmentFiltration {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (q n : ℤ) : HomologicalComplex.homology (CategoryTheory.Subobject.underlying.obj (F q)) n ⟶ (spectralObject (filtrationFunctor F hF)).abutmentFiltration q n

The map from H^n(F_q) onto the qth piece opZ^n(⊥ ≤ q, q ≤ ⊤) of the filtration of the abutment. Through filtrationAbutmentIso, the latter is embedded in H^n(K) as the image of the map induced by the inclusion F_q ⟶ K (CochainComplex.toFiltrationAbutmentFiltration_comp_filtrationAbutmentIso_hom).

instance CochainComplex.instEpiToFiltrationAbutmentFiltration {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (q n : ℤ) : CategoryTheory.Epi (toFiltrationAbutmentFiltration F hF q n)

@[simp]

theorem CochainComplex.toFiltrationAbutmentFiltration_comp_filtrationAbutmentIso_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (q n : ℤ) : CategoryTheory.CategoryStruct.comp (toFiltrationAbutmentFiltration F hF q n) (CategoryTheory.CategoryStruct.comp ((spectralObject (filtrationFunctor F hF)).abutmentFiltrationι q n) (filtrationAbutmentIso F hF n).hom) = HomologicalComplex.homologyMap (F q).arrow n

The filtration of the abutment is the image filtration. Through filtrationAbutmentIso, the qth piece of the filtration of the abutment is the image of the map H^n(F_q) ⟶ H^n(K) induced by the inclusion of the subcomplex F_q: this map factors as the epimorphism toFiltrationAbutmentFiltration followed by the embedding of the qth piece.

@[simp]

theorem CochainComplex.toFiltrationAbutmentFiltration_comp_filtrationAbutmentIso_hom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (q n : ℤ) {Z : C} (h : HomologicalComplex.homology K n ⟶ Z) : CategoryTheory.CategoryStruct.comp (toFiltrationAbutmentFiltration F hF q n) (CategoryTheory.CategoryStruct.comp ((spectralObject (filtrationFunctor F hF)).abutmentFiltrationι q n) (CategoryTheory.CategoryStruct.comp (filtrationAbutmentIso F hF n).hom h)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (F q).arrow n) h

The filtration of the abutment is the image filtration. Through filtrationAbutmentIso, the qth piece of the filtration of the abutment is the image of the map H^n(F_q) ⟶ H^n(K) induced by the inclusion of the subcomplex F_q: this map factors as the epimorphism toFiltrationAbutmentFiltration followed by the embedding of the qth piece.

theorem CochainComplex.isZero_filtrationAbutmentFiltration {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 : ℤ} (ha : F a = ⊥) (n : ℤ) : CategoryTheory.Limits.IsZero ((spectralObject (filtrationFunctor F hF)).abutmentFiltration a n)

The ath piece of the filtration of H^n(K) vanishes when F_a = ⊥.

theorem CochainComplex.isIso_filtrationAbutmentFiltrationι {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 : ℤ} (hb : F b = ⊤) (n : ℤ) : CategoryTheory.IsIso ((spectralObject (filtrationFunctor F hF)).abutmentFiltrationι b n)

The bth piece of the filtration of H^n(K) is everything when F_b = ⊤.

noncomputable def CochainComplex.filtrationSpectralSequencePageXIsoGradedOfFinite {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 ≅ CategoryTheory.Limits.cokernel ((spectralObject (filtrationFunctor F hF)).abutmentFiltrationMap pq.2 (pq.1 + pq.2))

Strong convergence for a finite filtration. If F_a = ⊥ and F_b = ⊤, then on every page r ≥ 2 with q - r + 2 ≤ a and b ≤ q + r - 1, the object at pq = (p, q) is the graded piece F_{q+1} H^{p+q} / F_q H^{p+q} of the filtration of the abutment H^{p+q}(K).