The spectral object of a filtered complex

Mathlib constructs a triangulated spectral object from mapping cones and observes that precomposing it with a functor into cochain complexes produces the spectral object associated to a filtered complex. The remaining bridge applies a homological functor to obtain a spectral object in an abelian category.

This file supplies that bridge for an arbitrary homological functor and then specializes it to homology on the homotopy category. Thus a filtration K : ι ⥤ CochainComplex C ℤ canonically produces an Abelian.SpectralObject C ι, which Mathlib assembles into a spectral sequence.

noncomputable def CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor {D : Type u_1} {A : Type u_2} {ι : Type u_3} [Category.{v_1, u_1} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [Category.{v_2, u_2} A] [Abelian A] [Category.{v_3, u_3} ι] (X : SpectralObject D ι) (F : Functor D A) [F.ShiftSequence ℤ] [F.IsHomological] : Abelian.SpectralObject A ι

Applying a homological functor, in every shifted degree, to a triangulated spectral object produces a spectral object in the target abelian category.

Equations

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

noncomputable def HomotopyCategory.filteredComplexSpectralObject {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.Category.{v_2, u_2} ι] (K : CategoryTheory.Functor ι (CochainComplex C ℤ)) : CategoryTheory.Abelian.SpectralObject C ι

The abelian spectral object associated to a filtered cochain complex K : ι ⥤ CochainComplex C ℤ.

Equations

• HomotopyCategory.filteredComplexSpectralObject K = ((HomotopyCategory.spectralObjectMappingCone C).precomp K).mapHomologicalFunctor (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0)