Spectral objects in triangulated categories

In this file, we introduce the category SpectralObject C ι of spectral objects in a pretriangulated category C indexed by the category ι.

TODO (@joelriou)

• construct the spectral object indexed by WithTop (WithBot ℤ) consisting of all truncations of an object of a triangulated category equipped with a t-structure
• define a similar notion of spectral objects in abelian categories, show that by applying a homological functor C ⥤ A to a spectral object in the triangulated category C, we obtain a spectral object in the abelian category A
• construct the spectral sequence attached to a spectral object in an abelian category

References

• [Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes, II.4][verdier1996]

structure CategoryTheory.Triangulated.SpectralObject (C : Type u_1) (ι : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Type (max (max (max u_1 u_2) v_1) v_2)

A spectral object in a pretriangulated category C indexed by a category ι consists of a functor ω₁ : ComposableArrows ι 1 ⥤ C, and a functorial distinguished triangle from the category ComposableArrows ι 2, which must be of the form ω₁.obj (mk₁ f) ⟶ ω₁.obj (mk₁ (f ≫ g)) ⟶ ω₁.obj (mk₁ g) ⟶ ... when evaluated on mk₂ f g : ComposableArrows ι 2.

• ω₁ : Functor (ComposableArrows ι 1) C

  A functor from ComposableArrows ι 1 to the pretriangulated category.

• δ' : (ComposableArrows.functorArrows ι 1 2 2 _proof_2 _proof_4).comp self.ω₁ ⟶ (ComposableArrows.functorArrows ι 0 1 2 _proof_6 _proof_2).comp (self.ω₁.comp (shiftFunctor C 1))

  The connecting homomorphism of the spectral object.

• distinguished' (D : ComposableArrows ι 2) : Pretriangulated.Triangle.mk (self.ω₁.map ((ComposableArrows.mapFunctorArrows ι 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4).app D)) (self.ω₁.map ((ComposableArrows.mapFunctorArrows ι 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4).app D)) (self.δ'.app D) ∈ Pretriangulated.distinguishedTriangles

noncomputable def CategoryTheory.Triangulated.SpectralObject.ω₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) : Functor (ComposableArrows ι 2) (Pretriangulated.Triangle C)

The functorial (distinguished) triangle attached to a spectral object in a pretriangulated category.

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {X✝ Y✝ : ComposableArrows ι 2} (φ : X✝ ⟶ Y✝) : (X.ω₂.map φ).hom₁ = X.ω₁.map (ComposableArrows.homMk₁ (φ.app 0) (φ.app 1) ⋯)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) (j : ComposableArrows ι 2) : (X.ω₂.obj j).mor₃ = X.δ'.app j

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {X✝ Y✝ : ComposableArrows ι 2} (φ : X✝ ⟶ Y✝) : (X.ω₂.map φ).hom₂ = X.ω₁.map (ComposableArrows.homMk₁ (φ.app 0) (φ.app ⟨2, ⋯⟩) ⋯)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) (j : ComposableArrows ι 2) : (X.ω₂.obj j).obj₃ = X.ω₁.obj (ComposableArrows.mk₁ (j.map (homOfLE ⋯)))

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) (j : ComposableArrows ι 2) : (X.ω₂.obj j).obj₁ = X.ω₁.obj (ComposableArrows.mk₁ (j.map (homOfLE ⋯)))

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {X✝ Y✝ : ComposableArrows ι 2} (φ : X✝ ⟶ Y✝) : (X.ω₂.map φ).hom₃ = X.ω₁.map (ComposableArrows.homMk₁ (φ.app 1) (φ.app ⟨2, ⋯⟩) ⋯)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) (j : ComposableArrows ι 2) : (X.ω₂.obj j).mor₂ = X.ω₁.map (ComposableArrows.homMk₁ (j.map (homOfLE ⋯)) (CategoryStruct.id (j.obj ⟨2, ⋯⟩)) ⋯)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) (j : ComposableArrows ι 2) : (X.ω₂.obj j).mor₁ = X.ω₁.map (ComposableArrows.homMk₁ (CategoryStruct.id (j.obj 0)) (j.map (homOfLE ⋯)) ⋯)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) (j : ComposableArrows ι 2) : (X.ω₂.obj j).obj₂ = X.ω₁.obj (ComposableArrows.mk₁ (j.map (homOfLE ⋯)))

theorem CategoryTheory.Triangulated.SpectralObject.ω₂_obj_distinguished {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) (D : ComposableArrows ι 2) : X.ω₂.obj D ∈ Pretriangulated.distinguishedTriangles

def CategoryTheory.Triangulated.SpectralObject.δ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : X.ω₁.obj (ComposableArrows.mk₁ g) ⟶ (shiftFunctor C 1).obj (X.ω₁.obj (ComposableArrows.mk₁ f))

The connecting homomorphism X.ω₁.obj (mk₁ g) ⟶ (X.ω₁.obj (mk₁ f))⟦(1 : ℤ)⟧ of a spectral object X in a pretriangulated category when f : i ⟶ j and g : j ⟶ k are composable.

def CategoryTheory.Triangulated.SpectralObject.triangle {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : Pretriangulated.Triangle C

The distinguished triangle attached to a spectral object E : SpectralObjet C ι and composable morphisms f : i ⟶ j and g : j ⟶ k in ι.

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.triangle_obj₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).obj₂ = X.ω₁.obj (ComposableArrows.mk₁ (CategoryStruct.comp f g))

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.triangle_mor₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).mor₁ = X.ω₁.map (ComposableArrows.twoδ₂Toδ₁ f g (CategoryStruct.comp f g) ⋯)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.triangle_mor₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).mor₃ = X.δ f g

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.triangle_obj₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).obj₁ = X.ω₁.obj (ComposableArrows.mk₁ f)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.triangle_mor₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).mor₂ = X.ω₁.map (ComposableArrows.twoδ₁Toδ₀ f g (CategoryStruct.comp f g) ⋯)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.triangle_obj₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).obj₃ = X.ω₁.obj (ComposableArrows.mk₁ g)

theorem CategoryTheory.Triangulated.SpectralObject.triangle_distinguished {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : X.triangle f g ∈ Pretriangulated.distinguishedTriangles

def CategoryTheory.Triangulated.SpectralObject.precomp {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) {ι' : Type u_4} [Category.{u_5, u_4} ι'] (F : Functor ι' ι) : SpectralObject C ι'

The precomposition of a spectral object with a functor.

def CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u_3} [Category.{v_3, u_3} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (X : SpectralObject C ι) (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : SpectralObject D ι

The image of a spectral by a triangulated functor.

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_ω₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u_3} [Category.{v_3, u_3} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (X : SpectralObject C ι) (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : (X.mapTriangulatedFunctor F).ω₁ = X.ω₁.comp F

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ' {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u_3} [Category.{v_3, u_3} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (X : SpectralObject C ι) (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : (X.mapTriangulatedFunctor F).δ' = CategoryStruct.comp (Functor.whiskerRight X.δ' F) (((ComposableArrows.functorArrows ι 0 1 2 _proof_6 _proof_2).comp X.ω₁).whiskerLeft (Functor.commShiftIso F 1).hom)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u_3} [Category.{v_3, u_3} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (X : SpectralObject C ι) (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.mapTriangulatedFunctor F).δ f g = CategoryStruct.comp (F.map (X.δ f g)) ((Functor.commShiftIso F 1).hom.app (X.ω₁.obj (ComposableArrows.mk₁ f)))

structure CategoryTheory.Triangulated.SpectralObject.Hom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X Y : SpectralObject C ι) : Type (max (max u_2 v_1) v_2)

The type of morphisms between spectral objects in pretriangulated categories.

• hom : X.ω₁ ⟶ Y.ω₁

  The natural transformation that is part of a morphism between spectral objects.

• comm {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : CategoryStruct.comp (X.δ f g) ((shiftFunctor C 1).map (self.hom.app (ComposableArrows.mk₁ f))) = CategoryStruct.comp (self.hom.app (ComposableArrows.mk₁ g)) (Y.δ f g)

theorem CategoryTheory.Triangulated.SpectralObject.Hom.ext {C : Type u_1} {ι : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} ι} {inst✝² : Limits.HasZeroObject C} {inst✝³ : HasShift C ℤ} {inst✝⁴ : Preadditive C} {inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive} {inst✝⁶ : Pretriangulated C} {X Y : SpectralObject C ι} {x y : X.Hom Y} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.Triangulated.SpectralObject.Hom.ext_iff {C : Type u_1} {ι : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} ι} {inst✝² : Limits.HasZeroObject C} {inst✝³ : HasShift C ℤ} {inst✝⁴ : Preadditive C} {inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive} {inst✝⁶ : Pretriangulated C} {X Y : SpectralObject C ι} {x y : X.Hom Y} : x = y ↔ x.hom = y.hom

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.Hom.comm_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X Y : SpectralObject C ι} (self : X.Hom Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {Z : C} (h : (shiftFunctor C 1).obj (Y.ω₁.obj (ComposableArrows.mk₁ f)) ⟶ Z) : CategoryStruct.comp (X.δ f g) (CategoryStruct.comp ((shiftFunctor C 1).map (self.hom.app (ComposableArrows.mk₁ f))) h) = CategoryStruct.comp (self.hom.app (ComposableArrows.mk₁ g)) (CategoryStruct.comp (Y.δ f g) h)

instance CategoryTheory.Triangulated.SpectralObject.instCategory {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Category.{max (max u_2 v_1) v_2, max (max (max u_2 v_2) u_1) v_1} (SpectralObject C ι)

theorem CategoryTheory.Triangulated.SpectralObject.hom_ext {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X Y : SpectralObject C ι} {α β : X ⟶ Y} (h : α.hom = β.hom) : α = β

theorem CategoryTheory.Triangulated.SpectralObject.hom_ext_iff {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X Y : SpectralObject C ι} {α β : X ⟶ Y} : α = β ↔ α.hom = β.hom

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.id_hom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : SpectralObject C ι) : (CategoryStruct.id X).hom = CategoryStruct.id X.ω₁

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.comp_hom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X Y Z : SpectralObject C ι} (α : X ⟶ Y) (β : Y ⟶ Z) : (CategoryStruct.comp α β).hom = CategoryStruct.comp α.hom β.hom

theorem CategoryTheory.Triangulated.SpectralObject.comp_hom_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X Y Z : SpectralObject C ι} (α : X ⟶ Y) (β : Y ⟶ Z) {Z✝ : Functor (ComposableArrows ι 1) C} (h : Z.ω₁ ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp α β).hom h = CategoryStruct.comp α.hom (CategoryStruct.comp β.hom h)

def CategoryTheory.Functor.mapTriangulatedSpectralObject {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u_3} [Category.{v_3, u_3} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (ι : Type u_4) [Category.{v_4, u_4} ι] : Functor (Triangulated.SpectralObject C ι) (Triangulated.SpectralObject D ι)

The functor between categories of spectral objects that is induced by a triangulated functor.