The comparison theorem for spectral objects indexed by EInt

A morphism φ : X ⟶ Y of spectral objects induces maps on the objects opZ^n(f, g) (CategoryTheory.Abelian.SpectralObject.opcyclesMapOfHom), compatible with Mathlib's short exact sequences 0 ⟶ opZ^n(f₁, f₂ ≫ f₃) ⟶ opZ^n(f₁ ≫ f₂, f₃) ⟶ E^n(f₁, f₂, f₃) ⟶ 0 (isIso_opcyclesMapOfHom_of_isIso). For EInt, these are the extensions 0 ⟶ F_q H^n ⟶ F_{q+1} H^n ⟶ E∞ ⟶ 0 of the filtration of the abutment H^n(⊥ ≤ ⊤); by induction on q and the three-lemma, an isomorphism on E∞ gives one on the abutment for finite filtrations; by stabilization, so does an isomorphism on some page.

Main results

• CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment: the comparison theorem on E∞.
• CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment_of_isIso_page: on a page.

theorem CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : SpectralObject C EInt} (φ : X ⟶ Y) {a b n : ℤ} (hab : a ≤ b) (hXa : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (hYa : Limits.IsZero ((Y.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (hXb : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (hYb : Limits.IsZero ((Y.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (hE : ∀ (q : ℤ), a ≤ q → q < b → IsIso (EMap φ (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n - 1) n (n + 1) ⋯ ⋯)) : IsIso ((φ.hom n).app (ComposableArrows.mk₁ (homOfLE ⋯)))

The comparison theorem on E∞. Let φ : X ⟶ Y be a morphism of spectral objects indexed by EInt and a ≤ b such that H^n(⊥ ≤ a) and H^n(b ≤ ⊤) vanish for X and Y (the filtrations of the abutments in degree n start at a and end at b). If φ is an isomorphism on EInfty q n for a ≤ q < b, then it is an isomorphism on the abutment H^n(⊥ ≤ ⊤).

theorem CategoryTheory.Abelian.SpectralObject.spectralSequencePageXMap_comp_pageXIsoEInfty_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : SpectralObject C EInt} (φ : X ⟶ Y) (r : ℤ) (hr : 2 ≤ r) (pq : ℤ × ℤ) (n : ℤ) (hn : n = pq.1 + pq.2) (hX₀ : Limits.IsZero ((X.H (n + 1)).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (hX₃ : Limits.IsZero ((X.H (n - 1)).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (hY₀ : Limits.IsZero ((Y.H (n + 1)).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (hY₃ : Limits.IsZero ((Y.H (n - 1)).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) : CategoryStruct.comp (spectralSequencePageXMap coreE₂Cohomological φ r hr pq) (Y.spectralSequencePageXIsoEInfty r hr pq n hn hY₀ hY₃).hom = CategoryStruct.comp (X.spectralSequencePageXIsoEInfty r hr pq n hn hX₀ hX₃).hom (EMap φ (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n - 1) n (n + 1) ⋯ ⋯)

The morphisms of pages spectralSequencePageXMap correspond to the maps EMap on the limit objects EInfty through the isomorphisms spectralSequencePageXIsoEInfty.

theorem CategoryTheory.Abelian.SpectralObject.isIso_hom_app_abutment_of_isIso_page {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : SpectralObject C EInt} (φ : X ⟶ Y) {a b : ℤ} (n : ℤ) (hXa : ∀ (m i : ℤ), n ≤ m → m ≤ n + 1 → i ≤ a → Limits.IsZero ((X.H m).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (hYa : ∀ (m i : ℤ), n ≤ m → m ≤ n + 1 → i ≤ a → Limits.IsZero ((Y.H m).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (hXb : ∀ (m i : ℤ), n - 1 ≤ m → m ≤ n → b ≤ i → Limits.IsZero ((X.H m).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (hYb : ∀ (m i : ℤ), n - 1 ≤ m → m ≤ n → b ≤ i → Limits.IsZero ((Y.H m).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (r : ℤ) (hr : 2 ≤ r) (h : ∀ (pq : ℤ × ℤ), IsIso (((spectralSequenceMap coreE₂Cohomological φ).hom r hr).f pq)) : IsIso ((φ.hom n).app (ComposableArrows.mk₁ (homOfLE ⋯)))

The comparison theorem. Let φ : X ⟶ Y be a morphism of spectral objects indexed by EInt and integers a, b (no inequality between them is needed) such that H^m(⊥ ≤ i) vanishes for i ≤ a and m ∈ {n, n + 1}, and H^m(i ≤ ⊤) vanishes for i ≥ b and m ∈ {n - 1, n}, for X and Y. If the induced morphism of spectral sequences is an isomorphism on every object of some page r ≥ 2, then φ is an isomorphism on the abutments H^n(⊥ ≤ ⊤).