Stabilization of the pages of the spectral sequence of a spectral object indexed by EInt

Let X be a spectral object in an abelian category, indexed by EInt. Its spectral sequence X.spectralSequence coreE₂Cohomological has on page r at (p, q) the object E^{p+q}(q - r + 2 ≤ q ≤ q + 1 ≤ q + r - 1). We introduce the limit object X.EInfty q n = E^n(⊥ ≤ q ≤ q + 1 ≤ ⊤) and show that the page-r object at (p, q) is isomorphic to X.EInfty q (p + q) as soon as H^{p+q+1}(⊥ ≤ q - r + 2) and H^{p+q-1}(q + r - 1 ≤ ⊤) vanish (spectralSequencePageXIsoEInfty). The isomorphism is the composite of the canonical maps E^n(i₀ ≤ i₁ ≤ i₂ ≤ i₃) ⟶ E^n(i₀' ≤ i₁ ≤ i₂ ≤ i₃') for i₀' ≤ i₀ and i₃ ≤ i₃', which are isomorphisms under these vanishing conditions (Mathlib's isoMapFourδ₁Toδ₀' and isoMapFourδ₄Toδ₃').

Main definitions

• CategoryTheory.Abelian.SpectralObject.EInfty X q n: the object E^n(⊥ ≤ q ≤ q + 1 ≤ ⊤).
• CategoryTheory.Abelian.SpectralObject.spectralSequencePageXIsoEInfty: the isomorphism of a page object with EInfty under the vanishing conditions.

theorem CategoryTheory.Abelian.SpectralObject.coe_le_coe_add_one (q : ℤ) : WithBotTop.coe q ≤ WithBotTop.coe (q + 1)

The inequality q ≤ q + 1 in EInt.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Abelian.SpectralObject.EInfty {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) : C

The object E^n(⊥ ≤ q ≤ q + 1 ≤ ⊤) of a spectral object indexed by EInt. Under the vanishing conditions of spectralSequencePageXIsoEInfty, it is isomorphic to the object at (n - q, q) on the rth page of the spectral sequence.

noncomputable def CategoryTheory.Abelian.SpectralObject.spectralSequencePageXIsoEInfty {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (r : ℤ) (hr : 2 ≤ r) (pq : ℤ × ℤ) (n : ℤ) (hn : n = pq.1 + pq.2) (h₀ : Limits.IsZero ((X.H (n + 1)).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (h₃ : Limits.IsZero ((X.H (n - 1)).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) : ((X.spectralSequence coreE₂Cohomological).page r ⋯).X pq ≅ X.EInfty pq.2 n

The object at pq = (p, q) on page r ≥ 2 of the spectral sequence of X is X.EInfty q (p + q) when H^{p+q+1}(⊥ ≤ q - r + 2) and H^{p+q-1}(q + r - 1 ≤ ⊤) vanish.

theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp_spectralSequencePageXIsoEInfty_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (r : ℤ) (hr : 2 ≤ r) (pq : ℤ × ℤ) (n : ℤ) (hn : n = pq.1 + pq.2) (h₀ : Limits.IsZero ((X.H (n + 1)).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (h₃ : Limits.IsZero ((X.H (n - 1)).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) : CategoryStruct.comp (X.mapFourδ₁Toδ₀' ⊥ (WithBotTop.coe (pq.2 - r + 2)) (WithBotTop.coe pq.2) (WithBotTop.coe (pq.2 + 1)) (WithBotTop.coe (pq.2 + r - 1)) ⋯ ⋯ ⋯ ⋯ (n - 1) n (n + 1) ⋯ ⋯) (CategoryStruct.comp (X.spectralSequencePageXIso coreE₂Cohomological r hr pq (WithBotTop.coe (pq.2 - r + 2)) (WithBotTop.coe pq.2) (WithBotTop.coe (pq.2 + 1)) (WithBotTop.coe (pq.2 + r - 1)) ⋯ ⋯ ⋯ ⋯ (n - 1) n (n + 1) hn ⋯ ⋯).inv (X.spectralSequencePageXIsoEInfty r hr pq n hn h₀ h₃).hom) = X.mapFourδ₄Toδ₃' ⊥ (WithBotTop.coe pq.2) (WithBotTop.coe (pq.2 + 1)) (WithBotTop.coe (pq.2 + r - 1)) ⊤ ⋯ ⋯ ⋯ ⋯ (n - 1) n (n + 1) ⋯ ⋯

The isomorphism spectralSequencePageXIsoEInfty is characterized by the canonical maps from E^n(⊥ ≤ q ≤ q + 1 ≤ q + r - 1) to the page object and to X.EInfty q n.

theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp_spectralSequencePageXIsoEInfty_hom_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (r : ℤ) (hr : 2 ≤ r) (pq : ℤ × ℤ) (n : ℤ) (hn : n = pq.1 + pq.2) (h₀ : Limits.IsZero ((X.H (n + 1)).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) (h₃ : Limits.IsZero ((X.H (n - 1)).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) {Z : C} (h : X.EInfty pq.2 n ⟶ Z) : CategoryStruct.comp (X.mapFourδ₁Toδ₀' ⊥ (WithBotTop.coe (pq.2 - r + 2)) (WithBotTop.coe pq.2) (WithBotTop.coe (pq.2 + 1)) (WithBotTop.coe (pq.2 + r - 1)) ⋯ ⋯ ⋯ ⋯ (n - 1) n (n + 1) ⋯ ⋯) (CategoryStruct.comp (X.spectralSequencePageXIso coreE₂Cohomological r hr pq (WithBotTop.coe (pq.2 - r + 2)) (WithBotTop.coe pq.2) (WithBotTop.coe (pq.2 + 1)) (WithBotTop.coe (pq.2 + r - 1)) ⋯ ⋯ ⋯ ⋯ (n - 1) n (n + 1) hn ⋯ ⋯).inv (CategoryStruct.comp (X.spectralSequencePageXIsoEInfty r hr pq n hn h₀ h₃).hom h)) = CategoryStruct.comp (X.mapFourδ₄Toδ₃' ⊥ (WithBotTop.coe pq.2) (WithBotTop.coe (pq.2 + 1)) (WithBotTop.coe (pq.2 + r - 1)) ⊤ ⋯ ⋯ ⋯ ⋯ (n - 1) n (n + 1) ⋯ ⋯) h

The isomorphism spectralSequencePageXIsoEInfty is characterized by the canonical maps from E^n(⊥ ≤ q ≤ q + 1 ≤ q + r - 1) to the page object and to X.EInfty q n.