Convergence for exhaustive filtrations

Let F : ℤ → Subobject K be an increasing filtration of a cochain complex of modules K. The filtration is exhaustive in degree n if every element of K^n lies in some F_q. Such a filtration need not reach K at any finite stage: the skeletal filtration of the singular chains of a fibration over an infinite CW complex, or the cell filtration of a twisted complex with infinitely many generators, are exhaustive but not finite. This file proves two convergence statements for the spectral sequence of an exhaustive filtration.

• The filtration of the abutment H^n(K) is exhaustive: every class lies in some piece F_q H^n (CochainComplex.exists_mem_range_filtrationAbutmentFiltrationι). Here F_q H^n is the image of H^n(F_q) ⟶ H^n(K) (CochainComplex.toFiltrationAbutmentFiltration_comp_filtrationAbutmentIso_hom), and its graded pieces are the limit objects E∞ (CategoryTheory.Abelian.SpectralObject.EInftyIsoCokernel). When moreover F_a = ⊥, the filtration of H^n(K) vanishes at a (CochainComplex.isZero_filtrationAbutmentFiltration).
• If the graded pieces F_{i+1}/F_i have vanishing H^m for all i ≥ b, so does the quotient K/F_b (CochainComplex.isZero_homology_cokernel_arrow_of_exhaustive). For a first-quadrant spectral sequence this holds in every degree, for some b depending on the degree. Then F_b H^n = H^n(K) (CochainComplex.isIso_filtrationAbutmentFiltrationι_of_exhaustive). If moreover H^{n+1}(F_{q-r+2}) vanishes (for instance if F_{q-r+2} = ⊥), the object at (p, q) with p + q = n on page r is the corresponding graded piece of H^n(K) (CochainComplex.filtrationSpectralSequencePageXIsoGradedOfExhaustive). If the cohomology of the stages F_i and G_i of two filtrations vanishes in degrees n and n + 1 for all i ≤ a (for instance if F_a = G_a = ⊥), a morphism of such filtered complexes which is an isomorphism on some page induces an isomorphism on H^n (CochainComplex.isIso_homologyMap_of_isIso_spectralSequence_page_of_exhaustive).

The vanishing of H^m(F_j/F_b) for every finite stage j ≥ b holds in any abelian category (CochainComplex.isZero_homology_cokernel_ofLE_of_isZero). The passage to K/F_b, the directed union of the subcomplexes F_j/F_b, uses that cohomology classes of a directed union of subcomplexes of modules come from its members (HomologicalComplex.exists_homologyMap_eq_of_injective).

References

• C. A. Weibel, An introduction to homological algebra, Cambridge Studies in Advanced Mathematics 38, Cambridge University Press, 1994, Theorem 5.5.1.
• J. McCleary, A User's Guide to Spectral Sequences, 2nd ed., Cambridge Studies in Advanced Mathematics 58, Cambridge University Press, 2001, Theorem 2.6.

theorem CochainComplex.isZero_homology_cokernel_ofLE_of_isZero {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 : ∀ (i : ℤ), b ≤ i → CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel ((F i).ofLE (F (i + 1)) ⋯)) m)) (j : ℤ) (hj : b ≤ j) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel ((F b).ofLE (F j) ⋯)) m)

If the graded pieces F_{i+1}/F_i of a filtration have vanishing H^m for all i ≥ b, then so do the quotients F_j/F_b for all j ≥ b.

theorem CochainComplex.exists_mem_range_filtrationAbutmentFiltrationι {R : Type u_1} [Ring R] {K : CochainComplex (ModuleCat R) ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) {n : ℤ} (hex : ∀ (x : ↑(K.X n)), ∃ (q : ℤ), x ∈ (ModuleCat.Hom.hom ((F q).arrow.f n)).range) (x : ↑((spectralObject (filtrationFunctor F hF)).abutment n)) : ∃ (q : ℤ), x ∈ (ModuleCat.Hom.hom ((spectralObject (filtrationFunctor F hF)).abutmentFiltrationι q n)).range

The filtration of the abutment of an exhaustive filtration is exhaustive. If every element of K^n lies in some F_q, then every element of the abutment H^n(K) lies in some piece F_q H^n of its filtration.

theorem CochainComplex.isZero_homology_cokernel_arrow_of_isZero_cokernel_ofLE {R : Type u_1} [Ring R] {K : CochainComplex (ModuleCat R) ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) {b m : ℤ} (hex : ∀ (x : ↑(K.X m)), ∃ (q : ℤ), x ∈ (ModuleCat.Hom.hom ((F q).arrow.f m)).range) (h : ∀ (j : ℤ) (hj : b ≤ j), CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel ((F b).ofLE (F j) ⋯)) m)) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel (F b).arrow) m)

The quotient by a stage of an exhaustive filtration. If every element of K^m lies in some F_q and the quotients F_j/F_b have vanishing H^m for all j ≥ b, then so does K/F_b.

theorem CochainComplex.isZero_homology_cokernel_arrow_of_exhaustive {R : Type u_1} [Ring R] {K : CochainComplex (ModuleCat R) ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) {b m : ℤ} (hex : ∀ (x : ↑(K.X m)), ∃ (q : ℤ), x ∈ (ModuleCat.Hom.hom ((F q).arrow.f m)).range) (h : ∀ (i : ℤ), b ≤ i → CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel ((F i).ofLE (F (i + 1)) ⋯)) m)) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel (F b).arrow) m)

The quotient by a stage of an exhaustive filtration. If every element of K^m lies in some F_q and the graded pieces F_{i+1}/F_i have vanishing H^m for all i ≥ b, then so does K/F_b.

theorem CochainComplex.isIso_filtrationAbutmentFiltrationι_of_exhaustive {R : Type u_1} [Ring R] {K : CochainComplex (ModuleCat R) ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) {b n : ℤ} (hex : ∀ (x : ↑(K.X n)), ∃ (q : ℤ), x ∈ (ModuleCat.Hom.hom ((F q).arrow.f n)).range) (h : ∀ (i : ℤ), b ≤ i → CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel ((F i).ofLE (F (i + 1)) ⋯)) n)) : CategoryTheory.IsIso ((spectralObject (filtrationFunctor F hF)).abutmentFiltrationι b n)

The filtration of the abutment reaches H^n(K). If every element of K^n lies in some F_q and the graded pieces F_{i+1}/F_i have vanishing H^n for all i ≥ b, then the bth piece of the filtration of H^n(K) is everything.

noncomputable def CochainComplex.filtrationSpectralSequencePageXIsoGradedOfExhaustive {R : Type u_1} [Ring R] {K : CochainComplex (ModuleCat R) ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) (r : ℤ) (hr : 2 ≤ r) (pq : ℤ × ℤ) (hex : ∀ (x : ↑(K.X (pq.1 + pq.2 - 1))), ∃ (i : ℤ), x ∈ (ModuleCat.Hom.hom ((F i).arrow.f (pq.1 + pq.2 - 1))).range) (h₀ : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Subobject.underlying.obj (F (pq.2 - r + 2))) (pq.1 + pq.2 + 1))) (h₃ : ∀ (i : ℤ), pq.2 + r - 1 ≤ i → CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel ((F i).ofLE (F (i + 1)) ⋯)) (pq.1 + pq.2 - 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 an exhaustive filtration. Let pq = (p, q) and n = p + q. Suppose that every element of K^{n-1} lies in some F_i, that H^{n+1}(F_{q-r+2}) vanishes, and that the graded pieces F_{i+1}/F_i have vanishing H^{n-1} for all i ≥ q + r - 1. Then the object at (p, q) on page r ≥ 2 is the graded piece F_{q+1} H^n / F_q H^n of the filtration of the abutment H^n(K).

theorem CochainComplex.isIso_homologyMap_of_isIso_spectralSequence_page_of_exhaustive {R : Type u_1} [Ring R] {K : CochainComplex (ModuleCat R) ℤ} (F : ℤ → CategoryTheory.Subobject K) (hF : Monotone F) {L : CochainComplex (ModuleCat R) ℤ} (G : ℤ → CategoryTheory.Subobject L) (hG : Monotone G) (α : filtrationFunctor F hF ⟶ filtrationFunctor G hG) (n : ℤ) {a b : ℤ} (hFa : ∀ (m : ℤ), n ≤ m → m ≤ n + 1 → ∀ i ≤ a, CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Subobject.underlying.obj (F i)) m)) (hGa : ∀ (m : ℤ), n ≤ m → m ≤ n + 1 → ∀ i ≤ a, CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Subobject.underlying.obj (G i)) m)) (hFex : ∀ (m : ℤ), n - 1 ≤ m → m ≤ n → ∀ (x : ↑(K.X m)), ∃ (q : ℤ), x ∈ (ModuleCat.Hom.hom ((F q).arrow.f m)).range) (hGex : ∀ (m : ℤ), n - 1 ≤ m → m ≤ n → ∀ (x : ↑(L.X m)), ∃ (q : ℤ), x ∈ (ModuleCat.Hom.hom ((G q).arrow.f m)).range) (hFb : ∀ (m : ℤ), n - 1 ≤ m → m ≤ n → ∀ (i : ℤ), b ≤ i → CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel ((F i).ofLE (F (i + 1)) ⋯)) m)) (hGb : ∀ (m : ℤ), n - 1 ≤ m → m ≤ n → ∀ (i : ℤ), b ≤ i → CategoryTheory.Limits.IsZero (HomologicalComplex.homology (CategoryTheory.Limits.cokernel ((G i).ofLE (G (i + 1)) ⋯)) m)) (r : ℤ) (hr : 2 ≤ r) (h : ∀ (pq : ℤ × ℤ), CategoryTheory.IsIso (((CategoryTheory.Abelian.SpectralObject.spectralSequenceMap CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological (spectralObjectMap α)).hom r hr).f pq)) : CategoryTheory.IsIso (HomologicalComplex.homologyMap (α.app ⊤) n)

The comparison theorem for exhaustive filtrations. Let α be a morphism between the functors of filtrations F of K and G of L, and let n be a degree. Suppose that the stages F_i and G_i at all indices i ≤ a have vanishing cohomology in degrees n and n + 1 (for instance F_a = G_a = ⊥), that in degrees n - 1 and n every element of K and of L lies in some stage of the filtration, and that the graded pieces of both filtrations at all indices i ≥ b have vanishing cohomology (no inequality between a and b is needed). If the morphism of spectral sequences induced by α is an isomorphism on every object of some page r ≥ 2, then α.app ⊤ induces an isomorphism on H^n.