The first differential of the spectral sequence of a filtered complex

Let F : EInt ⥤ CochainComplex C ℤ be a functor, for instance the functor of a filtration (CochainComplex.filtrationFunctor). Its spectral sequence CochainComplex.spectralSequence F uses Mathlib's recipe coreE₂Cohomological, in which the first page is numbered 2: the object at (p, q) is the cohomology H^{p+q} of the graded piece F_{q+1}/F_q (when F_q ⟶ F_{q+1} is a monomorphism, CochainComplex.spectralSequenceFirstPageXIsoCokernel), so q is the filtration index and p + q the total degree, and the differential goes from (p, q) to (p + 2, q - 1).

We show that this differential is the connecting map H^{p+q}(F_{q+1}/F_q) ⟶ H^{p+q+1}(F_q/F_{q-1}) of the short exact sequence F_q/F_{q-1} ⟶ F_{q+1}/F_{q-1} ⟶ F_{q+1}/F_q (CochainComplex.spectralSequence_first_page_d_eq). In McCleary's conventions, for the decreasing filtration F^s = F_{-s}, the object at (p, q) is E_1^{s,t} = H^{s+t}(F^s/F^{s+1}) with s = -q - 1 and t = p + 2q + 1, and this differential is d_1 : E_1^{s,t} ⟶ E_1^{s+1,t}.

The connecting maps of the spectral object of a functor with monomorphic transition maps are the connecting maps of the short exact sequences of graded pieces (CochainComplex.spectralObject_δ_comp_spectralObjectHIsoCokernel_hom), by CochainComplex.mappingCone.shiftMap_mappingConeCompTriangle_mor₃.

Main results

• CochainComplex.spectralObject_δ_comp_spectralObjectHIsoCokernel_hom, CochainComplex.spectralObjectHIsoCokernel_inv_comp_spectralObject_δ: the connecting maps of the spectral object, for monomorphic transition maps.
• CochainComplex.spectralSequence_first_page_d_eq: the first differential of the spectral sequence of a filtered complex.

References

• J. McCleary, A User's Guide to Spectral Sequences, §2.2.

theorem CochainComplex.spectralObject_δ_comp_spectralObjectHIsoCokernel_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {ι : Type u_2} [CategoryTheory.Category.{v_2, u_2} ι] (F : CategoryTheory.Functor ι (CochainComplex C ℤ)) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) [CategoryTheory.Mono (F.map f)] [CategoryTheory.Mono (F.map g)] (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : CategoryTheory.CategoryStruct.comp ((spectralObject F).δ f g n₀ n₁ h) (spectralObjectHIsoCokernel F f n₁).hom = CategoryTheory.CategoryStruct.comp (spectralObjectHIsoCokernel F g n₀).hom (⋯.δ n₀ n₁ ⋯)

The connecting maps of the spectral object of F, for monomorphisms F.map f and F.map g, are the connecting maps of the short exact sequences of cokernels cokernel (F.map f) ⟶ cokernel (F.map f ≫ F.map g) ⟶ cokernel (F.map g).

theorem CochainComplex.spectralObjectHIsoCokernel_inv_comp_spectralObject_δ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {ι : Type u_2} [CategoryTheory.Category.{v_2, u_2} ι] (F : CategoryTheory.Functor ι (CochainComplex C ℤ)) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) [CategoryTheory.Mono (F.map f)] [CategoryTheory.Mono (F.map g)] (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : CategoryTheory.CategoryStruct.comp (spectralObjectHIsoCokernel F g n₀).inv ((spectralObject F).δ f g n₀ n₁ h) = CategoryTheory.CategoryStruct.comp (⋯.δ n₀ n₁ ⋯) (spectralObjectHIsoCokernel F f n₁).inv

The form of spectralObject_δ_comp_spectralObjectHIsoCokernel_hom with the identification of H^{n₀}(g) with the cohomology of cokernel (F.map g) moved to the source: on the cohomology of the cokernels, the connecting maps of the spectral object of F are the connecting maps of the short exact sequences of cokernels.

theorem CochainComplex.spectralObjectHIsoCokernel_inv_comp_spectralObject_δ_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {ι : Type u_2} [CategoryTheory.Category.{v_2, u_2} ι] (F : CategoryTheory.Functor ι (CochainComplex C ℤ)) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) [CategoryTheory.Mono (F.map f)] [CategoryTheory.Mono (F.map g)] (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : C} (h✝ : ((spectralObject F).H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (spectralObjectHIsoCokernel F g n₀).inv (CategoryTheory.CategoryStruct.comp ((spectralObject F).δ f g n₀ n₁ h) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (⋯.δ n₀ n₁ ⋯) (spectralObjectHIsoCokernel F f n₁).inv) h✝

The form of spectralObject_δ_comp_spectralObjectHIsoCokernel_hom with the identification of H^{n₀}(g) with the cohomology of cokernel (F.map g) moved to the source: on the cohomology of the cokernels, the connecting maps of the spectral object of F are the connecting maps of the short exact sequences of cokernels.

theorem CochainComplex.spectralSequence_first_page_d_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (F : CategoryTheory.Functor EInt (CochainComplex C ℤ)) (p q : ℤ) [CategoryTheory.Mono (F.map (CategoryTheory.homOfLE ⋯))] [CategoryTheory.Mono (F.map (CategoryTheory.homOfLE ⋯))] : ((spectralSequence F).page 2 spectralSequence_first_page_d_eq._proof_7).d (p, q) (p + 2, q - 1) = CategoryTheory.CategoryStruct.comp (spectralSequenceFirstPageXIsoCokernel F (p, q) q (q + 1) ⋯ ⋯ (p + q) ⋯).hom (CategoryTheory.CategoryStruct.comp (⋯.δ (p + q) (p + q + 1) ⋯) (spectralSequenceFirstPageXIsoCokernel F (p + 2, q - 1) (q - 1) q ⋯ ⋯ (p + q + 1) ⋯).inv)

The first differential of the spectral sequence of a filtered complex. When F_{q-1} ⟶ F_q and F_q ⟶ F_{q+1} are monomorphisms, the differential of the first page (page 2 in Mathlib's numbering) from (p, q) to (p + 2, q - 1) is, under the identifications of the first page with the cohomology of the graded pieces, the connecting map H^{p+q}(F_{q+1}/F_q) ⟶ H^{p+q+1}(F_q/F_{q-1}) of the short exact sequence F_q/F_{q-1} ⟶ F_{q+1}/F_{q-1} ⟶ F_{q+1}/F_q.