The first differential of a column-filtered total complex

This file continues the identification of the initial page with column homology by tracking its horizontal differential. The spectral-object differential is first expressed as the connecting morphism for two adjacent columns. At the chain level, the standard section and retraction show that this connecting morphism is induced by the horizontal differential of the bicomplex.

theorem HomologicalComplex₂.columnFilteredInitialPage_d_eq_connecting (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) : CategoryTheory.CategoryStruct.comp ((K.columnFilteredTotalSpectralSequence.page 2 columnFilteredInitialPage_d_eq_connecting._proof_1).d (p, q) (p + 1, q)) (K.columnFilteredInitialPageColumnHomologyIso (p + 1) q).hom = CategoryTheory.CategoryStruct.comp (K.columnFilteredInitialPageColumnHomologyIso p q).hom (CategoryTheory.CategoryStruct.comp (K.columnShiftHomologyIso p q).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.singleColumnTotalIso p).inv (p + q)) (CategoryTheory.CategoryStruct.comp (⋯.δ (p + q) (p + 1 + q) ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.adjacentColumnTotalShortComplex (p + 1)).g (p + 1 + q)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.singleColumnTotalIso (p + 1)).hom (p + 1 + q)) (K.columnShiftHomologyIso (p + 1) q).hom)))))

Under the initial-page column-homology identifications, the first differential is the connecting morphism of the adjacent-column short exact sequence.

noncomputable def HomologicalComplex₂.singleColumnTotalι (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q n : ℤ) (h : p + q = n) : (K.X p).X q ⟶ ((K.singleColumnBicomplex p).total (ComplexShape.up ℤ)).X n

The inclusion of a bidegree term into the total complex of its single-column bicomplex.

Equations

• K.singleColumnTotalι p q n h = CategoryTheory.CategoryStruct.comp ((K.singleColumnXIso p p ⋯).inv.f q) ((K.singleColumnBicomplex p).ιTotal (ComplexShape.up ℤ) p q n h)

theorem HomologicalComplex₂.singleColumnTotalι_section_d_retraction_projection (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) : CategoryTheory.CategoryStruct.comp (K.singleColumnTotalι p q (p + q) ⋯) (CategoryTheory.CategoryStruct.comp (K.adjacentColumnTotalSection p (p + q)) (CategoryTheory.CategoryStruct.comp (((K.truncatedBicomplex p).total (ComplexShape.up ℤ)).d (p + q) (p + 1 + q)) (CategoryTheory.CategoryStruct.comp (K.adjacentColumnTotalRetraction p (p + 1 + q)) ((K.adjacentColumnTotalShortComplex (p + 1)).g.f (p + 1 + q))))) = CategoryTheory.CategoryStruct.comp ((K.d p (p + 1)).f q) (K.singleColumnTotalι (p + 1) q (p + 1 + q) ⋯)

One horizontal step in the adjacent-column connecting construction is the horizontal differential of the original bicomplex. The vertical part of the total differential vanishes after projecting to the newly added next column.

theorem HomologicalComplex₂.singleColumnTotalι_cycle (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) {A : AddCommGrpCat} (p q : ℤ) (a : A ⟶ (K.X p).X q) (ha : CategoryTheory.CategoryStruct.comp a ((K.X p).d q (q + 1)) = 0) : CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp (K.singleColumnTotalι p q (p + q) ⋯) (((K.singleColumnBicomplex p).total (ComplexShape.up ℤ)).d (p + q) (p + 1 + q))) = 0

A vertical cocycle gives a cocycle in the total complex of its single-column bicomplex.

theorem HomologicalComplex₂.adjacentColumnConnecting_representative (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) {A : AddCommGrpCat} (p q : ℤ) (a : A ⟶ (K.X p).X q) (ha : CategoryTheory.CategoryStruct.comp a ((K.X p).d q (q + 1)) = 0) : let S := K.adjacentColumnTotalShortComplex p; have hS := ⋯; let n := p + q; let n' := p + 1 + q; CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles S.X₃ (CategoryTheory.CategoryStruct.comp a (K.singleColumnTotalι p q n ⋯)) n' ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ S.X₃ n) (CategoryTheory.CategoryStruct.comp (hS.δ n n' ⋯) (HomologicalComplex.homologyMap (K.adjacentColumnTotalShortComplex (p + 1)).g n'))) = CategoryTheory.CategoryStruct.comp (((K.singleColumnBicomplex (p + 1)).total (ComplexShape.up ℤ)).liftCycles (CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp ((K.d p (p + 1)).f q) (K.singleColumnTotalι (p + 1) q n' ⋯))) (p + 1 + 1 + q) ⋯ ⋯) (((K.singleColumnBicomplex (p + 1)).total (ComplexShape.up ℤ)).homologyπ n')

The connecting morphism for two adjacent columns sends a vertical cocycle to its horizontal differential, viewed as a cocycle in the next single-column total complex.

theorem HomologicalComplex₂.singleColumnTotalι_comp_singleColumnTotalIso_hom (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) : CategoryTheory.CategoryStruct.comp (K.singleColumnTotalι p q (p + q) ⋯) ((K.singleColumnTotalIso p).hom.f (p + q)) = (CochainComplex.shiftFunctorObjXIso (K.X p) (-p) (p + q) q ⋯).inv

The canonical inclusion of a bidegree term into a single-column total complex is the inverse of the standard shifted-column component isomorphism.

theorem HomologicalComplex₂.singleColumnTotal_liftCycles_homologyIso (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) {A : AddCommGrpCat} (p q : ℤ) (a : A ⟶ (K.X p).X q) (ha : CategoryTheory.CategoryStruct.comp a ((K.X p).d q (q + 1)) = 0) : let T := (K.singleColumnBicomplex p).total (ComplexShape.up ℤ); CategoryTheory.CategoryStruct.comp (T.liftCycles (CategoryTheory.CategoryStruct.comp a (K.singleColumnTotalι p q (p + q) ⋯)) (p + 1 + q) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (T.homologyπ (p + q)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.singleColumnTotalIso p).hom (p + q)) (K.columnShiftHomologyIso p q).hom)) = CategoryTheory.CategoryStruct.comp ((K.X p).liftCycles a (q + 1) ⋯ ha) ((K.X p).homologyπ q)

A cocycle representative is unchanged after passing from a single-column total complex to the shifted column and then to column homology.

theorem HomologicalComplex₂.columnFilteredInitialPage_d_eq_horizontalHomologyMap (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) : CategoryTheory.CategoryStruct.comp ((K.columnFilteredTotalSpectralSequence.page 2 columnFilteredInitialPage_d_eq_connecting._proof_1).d (p, q) (p + 1, q)) (K.columnFilteredInitialPageColumnHomologyIso (p + 1) q).hom = CategoryTheory.CategoryStruct.comp (K.columnFilteredInitialPageColumnHomologyIso p q).hom (HomologicalComplex.homologyMap (K.d p (p + 1)) q)

Under the initial-page column-homology isomorphisms, the first spectral-sequence differential is the map on vertical homology induced by the horizontal bicomplex differential.