Spectral pages of a column-filtered total complex

The generic adjacent-column construction is in FilteredTotalComplexAdjacentCore. Here it is specialized to AddCommGrpCat and compared with the filtered spectral object's adjacent layers and connecting maps.

Main definitions and results

• HomologicalComplex₂.columnFilteredInitialPageColumnHomologyIso identifies the initial-page object with vertical column homology.
• HomologicalComplex₂.columnFilteredFirstPage_d_eq computes the initial differential from the horizontal bicomplex differential.

Implementation notes

The comparison transports the generic adjacent cone through filtration-stage isos, then tracks the signed total convention through connecting morphisms. The spectral-page statements here specialize to abelian groups.

References

The proof uses Mathlib's filtered CategoryTheory.Triangulated.SpectralObject, mapping-cone triangles, and homology connecting maps, together with the generic adjacent-column core.

instance HomologicalComplex₂.totalFunctor_additive : (totalFunctor AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ) (ComplexShape.up ℤ)).Additive

noncomputable def HomologicalComplex₂.columnFilteredAdjacentLayerComplex (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p : ℤ) : CochainComplex AddCommGrpCat ℤ

The adjacent filtration layer that contributes column p: the mapping cone of the map from filtration stage -p - 1 to stage -p.

Equations

• K.columnFilteredAdjacentLayerComplex p = CochainComplex.mappingCone (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯))

noncomputable def HomologicalComplex₂.columnFilteredStageIso (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p : ℤ) : K.columnFilteredTotalComplex.obj (columnFiltrationIndex p) ≅ (K.adjacentColumnTotalShortComplex p).X₂

A filtration stage indexed by -p is canonically the total complex of the stupid truncation beginning in column p.

Equations

• K.columnFilteredStageIso p = CategoryTheory.eqToIso ⋯

theorem HomologicalComplex₂.columnFilteredStageIso_comm (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p : ℤ) : CategoryTheory.CategoryStruct.comp (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯)) (K.columnFilteredStageIso p).hom = CategoryTheory.CategoryStruct.comp (K.columnFilteredStageIso (p + 1)).hom (K.adjacentColumnTotalShortComplex p).f

Reindexing filtration stage -p gives precisely the tail beginning at p; the comparison commutes with the adjacent-stage inclusion by the naturality of nested stupid-truncation maps.

theorem HomologicalComplex₂.columnFilteredStageIso_comm_assoc (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p : ℤ) {Z : CochainComplex AddCommGrpCat ℤ} (h : (K.adjacentColumnTotalShortComplex p).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯)) (CategoryTheory.CategoryStruct.comp (K.columnFilteredStageIso p).hom h) = CategoryTheory.CategoryStruct.comp (K.columnFilteredStageIso (p + 1)).hom (CategoryTheory.CategoryStruct.comp (K.adjacentColumnTotalShortComplex p).f h)

Reindexing filtration stage -p gives precisely the tail beginning at p; the comparison commutes with the adjacent-stage inclusion by the naturality of nested stupid-truncation maps.

theorem HomologicalComplex₂.columnFilteredStageIso_inv_comm (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p : ℤ) : CategoryTheory.CategoryStruct.comp (K.adjacentColumnTotalShortComplex p).f (K.columnFilteredStageIso p).inv = CategoryTheory.CategoryStruct.comp (K.columnFilteredStageIso (p + 1)).inv (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯))

Invert the preceding adjacent-stage square. Cancellation by the stage isomorphism turns its commutative square into this inverse orientation.

theorem HomologicalComplex₂.columnFilteredStageIso_inv_comm_assoc (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p : ℤ) {Z : CochainComplex AddCommGrpCat ℤ} (h : K.columnFilteredTotalComplex.obj (columnFiltrationIndex p) ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.adjacentColumnTotalShortComplex p).f (CategoryTheory.CategoryStruct.comp (K.columnFilteredStageIso p).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (K.columnFilteredStageIso (p + 1)).inv (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯))) h

Invert the preceding adjacent-stage square. Cancellation by the stage isomorphism turns its commutative square into this inverse orientation.

noncomputable def HomologicalComplex₂.columnFilteredAdjacentLayerIso (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p : ℤ) : K.columnFilteredAdjacentLayerComplex p ≅ CochainComplex.mappingCone (K.adjacentColumnTotalShortComplex p).f

The adjacent filtration mapping cone is canonically isomorphic to the mapping cone of the degreewise split adjacent-column short complex.

Equations

• One or more equations did not get rendered due to their size.

theorem HomologicalComplex₂.columnFilteredAdjacentLayerComplex_eq (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p : ℤ) : K.columnFilteredAdjacentLayerComplex p = CochainComplex.mappingCone (K.adjacentColumnTotalShortComplex p).f

The filtration's adjacent mapping cone is the canonical adjacent-column mapping cone.

noncomputable def HomologicalComplex₂.columnFilteredAdjacentLayerConeToShift (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p : ℤ) : K.columnFilteredAdjacentLayerComplex p ⟶ (CategoryTheory.shiftFunctor (CochainComplex AddCommGrpCat ℤ) (-p)).obj (K.X p)

The adjacent column-filtration layer maps quasi-isomorphically to the newly added column, shifted so that total degree p + q corresponds to vertical degree q.

Equations

• K.columnFilteredAdjacentLayerConeToShift p = CategoryTheory.CategoryStruct.comp (K.columnFilteredAdjacentLayerIso p).hom (K.adjacentColumnConeToShift p)

instance HomologicalComplex₂.columnFilteredAdjacentLayerConeToShift_quasiIso (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p : ℤ) : QuasiIso (K.columnFilteredAdjacentLayerConeToShift p)

theorem HomologicalComplex₂.columnFilteredInr_comp_adjacentLayerConeToShift (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p : ℤ) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯))) (K.columnFilteredAdjacentLayerConeToShift p) = CategoryTheory.CategoryStruct.comp (K.columnFilteredStageIso p).hom (CategoryTheory.CategoryStruct.comp (K.adjacentColumnTotalShortComplex p).g (K.singleColumnTotalIso p).hom)

Under the canonical adjacent-layer comparison, the inclusion of the middle filtration stage becomes the quotient map in the adjacent-column short exact sequence.

noncomputable def HomologicalComplex₂.filteredComplexPrecompTriangleIso (X : CategoryTheory.Triangulated.SpectralObject (HomotopyCategory AddCommGrpCat (ComplexShape.up ℤ)) (CochainComplex AddCommGrpCat ℤ)) (F : CategoryTheory.Functor ℤ (CochainComplex AddCommGrpCat ℤ)) {i j k : ℤ} (f : i ⟶ j) (g : j ⟶ k) : (X.precomp F).triangle f g ≅ X.triangle (F.map f) (F.map g)

The triangle constructed after precomposing a spectral object by a filtered complex is canonically isomorphic to the triangle obtained from the two mapped filtration morphisms.

Equations

• One or more equations did not get rendered due to their size.

theorem HomologicalComplex₂.columnFilteredConnecting_comp_homologyFactor (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) : CategoryTheory.CategoryStruct.comp (K.columnFilteredTotalSpectralObject.δ (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (p + q) (p + 1 + q) ⋯) ((HomotopyCategory.homologyFunctorFactors AddCommGrpCat (ComplexShape.up ℤ) (p + 1 + q)).app (K.columnFilteredAdjacentLayerComplex (p + 1))).hom = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors AddCommGrpCat (ComplexShape.up ℤ) (p + q)).app (K.columnFilteredAdjacentLayerComplex p)).hom ((HomologicalComplex.homologyFunctor AddCommGrpCat (ComplexShape.up ℤ) 0).shiftMap (CochainComplex.mappingConeCompTriangle (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯)) (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯))).mor₃ (p + q) (p + 1 + q) ⋯)

The connecting morphism of the column-filtered spectral object, transported from the precomposed spectral-object triangle to the ordinary mapping-cone triangle.

noncomputable def HomologicalComplex₂.columnFilteredAdjacentLayerHomologyIso (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p n : ℤ) : HomologicalComplex.homology (K.columnFilteredAdjacentLayerComplex p) n ≅ ((CategoryTheory.shiftFunctor (HomologicalComplex AddCommGrpCat (ComplexShape.up ℤ)) (-p)).obj (K.X p)).homology n

Homology of an adjacent filtration layer, identified with homology of the shifted new column.

Equations

• K.columnFilteredAdjacentLayerHomologyIso p n = isoOfQuasiIsoAt (K.columnFilteredAdjacentLayerConeToShift p) n

theorem HomologicalComplex₂.homologyMap_descShortComplex_comp_delta (S : CategoryTheory.ShortComplex (CochainComplex AddCommGrpCat ℤ)) (hS : S.ShortExact) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (CochainComplex.mappingCone.descShortComplex S) n₀) (hS.δ n₀ n₁ ⋯) = (HomologicalComplex.homologyFunctor AddCommGrpCat (ComplexShape.up ℤ) 0).shiftMap (CochainComplex.mappingCone.triangle S.f).mor₃ n₀ n₁ ⋯

The mapping-cone comparison for a short exact sequence transports the canonical connecting morphism to the ordinary connecting homomorphism in homology.

theorem HomologicalComplex₂.homologyMap_descShortComplex_comp_delta_assoc (S : CategoryTheory.ShortComplex (CochainComplex AddCommGrpCat ℤ)) (hS : S.ShortExact) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : AddCommGrpCat} (h✝ : S.X₁.homology n₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (CochainComplex.mappingCone.descShortComplex S) n₀) (CategoryTheory.CategoryStruct.comp (hS.δ n₀ n₁ ⋯) h✝) = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor AddCommGrpCat (ComplexShape.up ℤ) 0).shiftMap (CochainComplex.mappingCone.triangle S.f).mor₃ n₀ n₁ ⋯) h✝

The mapping-cone comparison for a short exact sequence transports the canonical connecting morphism to the ordinary connecting homomorphism in homology.

theorem HomologicalComplex₂.columnFilteredRawConnecting_comp_stageIso (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor AddCommGrpCat (ComplexShape.up ℤ) 0).shiftMap (CochainComplex.mappingCone.triangle (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯))).mor₃ (p + q) (p + 1 + q) ⋯) (HomologicalComplex.homologyMap (K.columnFilteredStageIso (p + 1)).hom (p + 1 + q)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.columnFilteredAdjacentLayerIso p).hom (p + q)) ((HomologicalComplex.homologyFunctor AddCommGrpCat (ComplexShape.up ℤ) 0).shiftMap (CochainComplex.mappingCone.triangle (K.adjacentColumnTotalShortComplex p).f).mor₃ (p + q) (p + 1 + q) ⋯)

Apply the homology functor to the cone-triangle isomorphism induced by the filtration-stage square. Its third morphism gives the connecting-map square after the shift-map comparison.

theorem HomologicalComplex₂.columnFilteredRawConnecting_comp_stageIso_assoc (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) {Z : AddCommGrpCat} (h : HomologicalComplex.homology (K.adjacentColumnTotalShortComplex (p + 1)).X₂ (p + 1 + q) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor AddCommGrpCat (ComplexShape.up ℤ) 0).shiftMap (CochainComplex.mappingCone.triangle (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯))).mor₃ (p + q) (p + 1 + q) ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.columnFilteredStageIso (p + 1)).hom (p + 1 + q)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.columnFilteredAdjacentLayerIso p).hom (p + q)) ((HomologicalComplex.homologyFunctor AddCommGrpCat (ComplexShape.up ℤ) 0).shiftMap (CochainComplex.mappingCone.triangle (K.adjacentColumnTotalShortComplex p).f).mor₃ (p + q) (p + 1 + q) ⋯)) h

Apply the homology functor to the cone-triangle isomorphism induced by the filtration-stage square. Its third morphism gives the connecting-map square after the shift-map comparison.

theorem HomologicalComplex₂.columnFilteredHomologyMap_inr_comp_coneToShift (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p n : ℤ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (CochainComplex.mappingCone.inr (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯))) n) (HomologicalComplex.homologyMap (K.columnFilteredAdjacentLayerConeToShift p) n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.columnFilteredStageIso p).hom n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.adjacentColumnTotalShortComplex p).g n) (HomologicalComplex.homologyMap (K.singleColumnTotalIso p).hom n))

The inclusion of the middle filtration stage followed by the adjacent-layer comparison, on homology.

theorem HomologicalComplex₂.columnFilteredHomologyMap_inr_comp_coneToShift_assoc (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p n : ℤ) {Z : AddCommGrpCat} (h : HomologicalComplex.homology ((CategoryTheory.shiftFunctor (CochainComplex AddCommGrpCat ℤ) (-p)).obj (K.X p)) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (CochainComplex.mappingCone.inr (K.columnFilteredTotalComplex.map (CategoryTheory.homOfLE ⋯))) n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.columnFilteredAdjacentLayerConeToShift p) n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.columnFilteredStageIso p).hom n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.adjacentColumnTotalShortComplex p).g n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.singleColumnTotalIso p).hom n) h))

The inclusion of the middle filtration stage followed by the adjacent-layer comparison, on homology.

theorem HomologicalComplex₂.columnFilteredHomologyMap_coneToShift_comp_singleColumnTotalIso_inv (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p n : ℤ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.columnFilteredAdjacentLayerConeToShift p) n) (HomologicalComplex.homologyMap (K.singleColumnTotalIso p).inv n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.columnFilteredAdjacentLayerIso p).hom n) (HomologicalComplex.homologyMap (CochainComplex.mappingCone.descShortComplex (K.adjacentColumnTotalShortComplex p)) n)

The adjacent-layer cone comparison factors through the short-complex cone projection and the single-column total isomorphism. Cancel that final isomorphism after applying homology to expose the short-complex map.

theorem HomologicalComplex₂.columnFilteredHomologyMap_coneToShift_comp_singleColumnTotalIso_inv_assoc (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p n : ℤ) {Z : AddCommGrpCat} (h : ((K.singleColumnBicomplex p).total (ComplexShape.up ℤ)).homology n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.columnFilteredAdjacentLayerConeToShift p) n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.singleColumnTotalIso p).inv n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (K.columnFilteredAdjacentLayerIso p).hom n) (HomologicalComplex.homologyMap (CochainComplex.mappingCone.descShortComplex (K.adjacentColumnTotalShortComplex p)) n)) h

The adjacent-layer cone comparison factors through the short-complex cone projection and the single-column total isomorphism. Cancel that final isomorphism after applying homology to expose the short-complex map.

noncomputable def HomologicalComplex₂.columnFilteredInitialPageXIso (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) : (K.columnFilteredTotalSpectralSequence.page 2 columnFilteredInitialPageXIso._proof_1).X (p, q) ≅ (K.columnFilteredTotalSpectralObject.H (p + q)).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))

The initial-page object before transporting adjacent-layer homology to column homology.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HomologicalComplex₂.columnFilteredAdjacentLayerSpectralHomologyIso (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) : (K.columnFilteredTotalSpectralObject.H (p + q)).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)) ≅ HomologicalComplex.homology (K.columnFilteredAdjacentLayerComplex p) (p + q)

The spectral object's adjacent-layer term is ordinary homology of the corresponding mapping cone.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HomologicalComplex₂.columnShiftHomologyIso (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) : ((CategoryTheory.shiftFunctor (HomologicalComplex AddCommGrpCat (ComplexShape.up ℤ)) (-p)).obj (K.X p)).homology (p + q) ≅ (K.X p).homology q

Homology of a shifted column in total degree p + q is column homology in degree q.

Equations

• K.columnShiftHomologyIso p q = (CochainComplex.ShiftSequence.shiftIso AddCommGrpCat (-p) (p + q) q ⋯).app (K.X p)

noncomputable def HomologicalComplex₂.columnFilteredInitialPageColumnHomologyIso (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) : (K.columnFilteredTotalSpectralSequence.page 2 columnFilteredInitialPageXIso._proof_1).X (p, q) ≅ (K.X p).homology q

The initial page of the column filtration is vertical column homology.

Equations

• One or more equations did not get rendered due to their size.

theorem HomologicalComplex₂.columnFilteredFirstPage_d_eq (K : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (p q : ℤ) : (K.columnFilteredTotalSpectralSequence.page 2 columnFilteredInitialPageXIso._proof_1).d (p, q) (p + 1, q) = CategoryTheory.CategoryStruct.comp (K.columnFilteredInitialPageXIso p q).hom (CategoryTheory.CategoryStruct.comp (K.columnFilteredTotalSpectralObject.δ (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (p + q) (p + 1 + q) ⋯) (K.columnFilteredInitialPageXIso (p + 1) q).inv)

The raw formula for the horizontal differential on the initial page.