The abutment of a spectral object indexed by EInt and its filtration

Let X be a spectral object in an abelian category, indexed by EInt. Its abutment in degree n is H^n(⊥ ≤ ⊤) (X.abutment n), for a filtered complex the cohomology of the complex. It is filtered by the images of the maps H^n(⊥ ≤ q) ⟶ H^n(⊥ ≤ ⊤): the qth piece is opZ^n(⊥ ≤ q, q ≤ ⊤), the cokernel of δ : H^{n-1}(q ≤ ⊤) ⟶ H^n(⊥ ≤ q), embedded in the abutment by X.abutmentFiltrationι q n (a monomorphism, by exactness). The pieces increase with q (X.abutmentFiltrationMap q n, compatible with the embeddings), and the limit object X.EInfty q n = E^n(⊥ ≤ q ≤ q + 1 ≤ ⊤) of the spectral sequence is the graded piece: the cokernel of F_q H^n ⟶ F_{q+1} H^n (X.EInftyIsoCokernel), from Mathlib's short exact sequence shortComplexOpcyclesThreeδ₂Toδ₁_shortExact.

The filtration is bounded below and exhaustive in degree n as soon as H^n(⊥ ≤ q) vanishes for small q (isZero_abutmentFiltration) and H^n(q ≤ ⊤) vanishes for large q (isIso_abutmentFiltrationι).

Main definitions

• CategoryTheory.Abelian.SpectralObject.abutment X n: the object H^n(⊥ ≤ ⊤).
• CategoryTheory.Abelian.SpectralObject.abutmentFiltration X q n: the qth filtration piece.
• CategoryTheory.Abelian.SpectralObject.EInftyIsoCokernel X q n: E∞ is the graded piece (characterized by opcyclesToE_EInftyIsoCokernel_hom).

@[reducible, inline]

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

The abutment H^n(⊥ ≤ ⊤) of a spectral object indexed by EInt.

@[reducible, inline]

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

The qth piece opZ^n(⊥ ≤ q, q ≤ ⊤) of the filtration of the abutment in degree n: the cokernel of δ : H^{n-1}(q ≤ ⊤) ⟶ H^n(⊥ ≤ q), that is, the image of H^n(⊥ ≤ q) in the abutment.

noncomputable def CategoryTheory.Abelian.SpectralObject.abutmentFiltrationι {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) : X.abutmentFiltration q n ⟶ X.abutment n

The embedding of the qth filtration piece into the abutment.

theorem CategoryTheory.Abelian.SpectralObject.abutmentFiltrationι_eq {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) : X.abutmentFiltrationι q n = X.fromOpcycles (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) ⋯ n

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.pOpcycles_abutmentFiltrationι {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) : CategoryStruct.comp (X.pOpcycles (homOfLE ⋯) (homOfLE ⋯) n) (X.abutmentFiltrationι q n) = (X.H n).map (ComposableArrows.twoδ₂Toδ₁ (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) ⋯)

The embedding of the qth filtration piece is induced by the map H^n(⊥ ≤ q) ⟶ H^n(⊥ ≤ ⊤).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.pOpcycles_abutmentFiltrationι_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) {Z : C} (h : X.abutment n ⟶ Z) : CategoryStruct.comp (X.pOpcycles (homOfLE ⋯) (homOfLE ⋯) n) (CategoryStruct.comp (X.abutmentFiltrationι q n) h) = CategoryStruct.comp ((X.H n).map (ComposableArrows.twoδ₂Toδ₁ (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) ⋯)) h

The embedding of the qth filtration piece is induced by the map H^n(⊥ ≤ q) ⟶ H^n(⊥ ≤ ⊤).

instance CategoryTheory.Abelian.SpectralObject.instMonoAbutmentFiltrationι {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) : Mono (X.abutmentFiltrationι q n)

noncomputable def CategoryTheory.Abelian.SpectralObject.abutmentFiltrationMap {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) : X.abutmentFiltration q n ⟶ X.abutmentFiltration (q + 1) n

The inclusion of the qth filtration piece into the (q + 1)st one.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.abutmentFiltrationMap_ι {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) : CategoryStruct.comp (X.abutmentFiltrationMap q n) (X.abutmentFiltrationι (q + 1) n) = X.abutmentFiltrationι q n

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.abutmentFiltrationMap_ι_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) {Z : C} (h : X.abutment n ⟶ Z) : CategoryStruct.comp (X.abutmentFiltrationMap q n) (CategoryStruct.comp (X.abutmentFiltrationι (q + 1) n) h) = CategoryStruct.comp (X.abutmentFiltrationι q n) h

noncomputable def CategoryTheory.Abelian.SpectralObject.EInftyIsoCokernel {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) : X.EInfty q n ≅ Limits.cokernel (X.abutmentFiltrationMap q n)

The limit object E^n(⊥ ≤ q ≤ q + 1 ≤ ⊤) of the spectral sequence is the graded piece F_{q+1} H^n / F_q H^n of the filtration of the abutment.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesToE_EInftyIsoCokernel_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) : CategoryStruct.comp (X.opcyclesToE (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) ⋯ (n - 1) n (n + 1) ⋯ ⋯) (X.EInftyIsoCokernel q n).hom = Limits.cokernel.π (X.abutmentFiltrationMap q n)

Through EInftyIsoCokernel, the canonical map opZ^n(⊥ ≤ q + 1, q + 1 ≤ ⊤) ⟶ E∞ is the projection to the cokernel of F_q H^n ⟶ F_{q+1} H^n.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesToE_EInftyIsoCokernel_hom_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) (q n : ℤ) {Z : C} (h : Limits.cokernel (X.abutmentFiltrationMap q n) ⟶ Z) : CategoryStruct.comp (X.opcyclesToE (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) ⋯ (n - 1) n (n + 1) ⋯ ⋯) (CategoryStruct.comp (X.EInftyIsoCokernel q n).hom h) = CategoryStruct.comp (Limits.cokernel.π (X.abutmentFiltrationMap q n)) h

Through EInftyIsoCokernel, the canonical map opZ^n(⊥ ≤ q + 1, q + 1 ≤ ⊤) ⟶ E∞ is the projection to the cokernel of F_q H^n ⟶ F_{q+1} H^n.

theorem CategoryTheory.Abelian.SpectralObject.isZero_abutmentFiltration {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) {q n : ℤ} (h : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) : Limits.IsZero (X.abutmentFiltration q n)

The qth filtration piece vanishes when H^n(⊥ ≤ q) does: the filtration is bounded below in degree n when these vanish for small q.

theorem CategoryTheory.Abelian.SpectralObject.isIso_abutmentFiltrationι {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (X : SpectralObject C EInt) {q n : ℤ} (h : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))) : IsIso (X.abutmentFiltrationι q n)

The qth filtration piece is the whole abutment when H^n(q ≤ ⊤) vanishes: the filtration is exhaustive in degree n when these vanish for large q.