The comparison theorem for filtered complexes

A morphism α : filtrationFunctor F hF ⟶ filtrationFunctor G hG of filtered complexes induces the morphism of spectral sequences spectralSequenceMap coreE₂Cohomological (spectralObjectMap α). If the filtrations are finite and this morphism is an isomorphism on some page, then α.app ⊤ induces isomorphisms in cohomology. The last step, from the abutments to the cohomology of the filtered complexes, holds for all filtrations.

Main results

• CochainComplex.isIso_homologyMap_app_top_of_isIso_abutment: an isomorphism on the abutments gives an isomorphism in cohomology.
• CochainComplex.isIso_homologyMap_of_isIso_spectralSequence_page: the comparison theorem.

theorem CochainComplex.isIso_homologyMap_app_top_of_isIso_abutment {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {F : ℤ → CategoryTheory.Subobject K} {hF : Monotone F} {G : ℤ → CategoryTheory.Subobject L} {hG : Monotone G} (α : filtrationFunctor F hF ⟶ filtrationFunctor G hG) (n : ℤ) (h : CategoryTheory.IsIso (((spectralObjectMap α).hom n).app (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))) : CategoryTheory.IsIso (HomologicalComplex.homologyMap (α.app ⊤) n)

The map in cohomology induced by α.app ⊤ is an isomorphism as soon as the morphism of spectral objects induced by α is an isomorphism on the abutment H^n(⊥ ≤ ⊤).

theorem CochainComplex.isIso_homologyMap_of_isIso_spectralSequence_page {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (G : ℤ → CategoryTheory.Subobject L) (hG : Monotone G) (α : filtrationFunctor F hF ⟶ filtrationFunctor G hG) {a b : ℤ} (hFa : F a = ⊥) (hGa : G a = ⊥) (hFb : F b = ⊤) (hGb : G b = ⊤) (r : ℤ) (hr : 2 ≤ r) (h : ∀ (pq : ℤ × ℤ), CategoryTheory.IsIso (((CategoryTheory.Abelian.SpectralObject.spectralSequenceMap CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological (spectralObjectMap α)).hom r hr).f pq)) (n : ℤ) : CategoryTheory.IsIso (HomologicalComplex.homologyMap (α.app ⊤) n)

The comparison theorem for filtered complexes. Let α be a morphism between the functors of finite increasing filtrations F of K and G of L (F_a = G_a = ⊥ and F_b = G_b = ⊤). If the induced morphism of spectral sequences is an isomorphism on every object of some page r ≥ 2, then α.app ⊤ induces isomorphisms in cohomology.