The spectral object with values in the homotopy category

Let C be an additive category. In this file, we show that the mapping cone defines a spectral object with values in the homotopy category of ℤ-indexed cochain complexes C that is indexed by the category CochainComplex C ℤ. (It follows that to any functor ι ⥤ CochainComplex C ℤ (e.g. a filtered complex), there is an associated spectral object indexed by ι.)

noncomputable def HomotopyCategory.composableArrowsFunctor (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Functor (CategoryTheory.ComposableArrows (CochainComplex C ℤ) 1) (CochainComplex C ℤ)

The functor ComposableArrows (CochainComplex C ℤ) 1 ⥤ CochainComplex C ℤ which sends a morphism of cochain complexes to its mapping cone.

@[simp]

theorem HomotopyCategory.composableArrowsFunctor_obj (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (f : CategoryTheory.ComposableArrows (CochainComplex C ℤ) 1) : (composableArrowsFunctor C).obj f = CochainComplex.mappingCone (f.map' 0 1 composableArrowsFunctor._proof_2 composableArrowsFunctor._proof_3)

@[simp]

theorem HomotopyCategory.composableArrowsFunctor_map (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X✝ Y✝ : CategoryTheory.ComposableArrows (CochainComplex C ℤ) 1} (φ : X✝ ⟶ Y✝) : (composableArrowsFunctor C).map φ = CochainComplex.mappingCone.map (X✝.map' 0 1 composableArrowsFunctor._proof_2 composableArrowsFunctor._proof_3) (Y✝.map' 0 1 composableArrowsFunctor._proof_2 composableArrowsFunctor._proof_3) (φ.app 0) (φ.app 1) ⋯

noncomputable def HomotopyCategory.spectralObjectMappingCone (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Triangulated.SpectralObject (HomotopyCategory C (ComplexShape.up ℤ)) (CochainComplex C ℤ)

The spectral object with values in (HomotopyCategory C (.up ℤ) that is indexed by CochainComplex C ℤ.

@[simp]

theorem HomotopyCategory.spectralObjectMappingCone_δ'_app (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (D : CategoryTheory.ComposableArrows (CochainComplex C ℤ) 2) : (spectralObjectMappingCone C).δ'.app D = ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj (CochainComplex.mappingConeCompTriangle (D.map' 0 1 composableArrowsFunctor._proof_2 spectralObjectMappingCone._proof_2) (D.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))).mor₃

@[simp]

theorem HomotopyCategory.spectralObjectMappingCone_ω₁ (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (spectralObjectMappingCone C).ω₁ = (composableArrowsFunctor C).comp (quotient C (ComplexShape.up ℤ))