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 sequence attached to a spectral object in an abelian category (the spectral sequence is already constructed: it remains to study convergence)

References

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

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.

Equations

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

@[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_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.ω₂_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 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.ω₂_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.ω₁.map (ComposableArrows.homMk₁ (j.map (homOfLE ⋯)) (CategoryStruct.id (j.obj ⟨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.ω₂_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, ⋯⟩) ⋯)

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.

Equations

• X.δ f g = X.δ'.app (CategoryTheory.ComposableArrows.mk₂ f g)

theorem CategoryTheory.Triangulated.SpectralObject.δ_naturality {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) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : ComposableArrows.mk₁ f ⟶ ComposableArrows.mk₁ f') (β : ComposableArrows.mk₁ g ⟶ ComposableArrows.mk₁ g') (hαβ : α.app 1 = β.app 0) : CategoryStruct.comp (X.ω₁.map β) (X.δ f' g') = CategoryStruct.comp (X.δ f g) ((shiftFunctor C 1).map (X.ω₁.map α))

theorem CategoryTheory.Triangulated.SpectralObject.δ_naturality_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 : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : ComposableArrows.mk₁ f ⟶ ComposableArrows.mk₁ f') (β : ComposableArrows.mk₁ g ⟶ ComposableArrows.mk₁ g') (hαβ : α.app 1 = β.app 0) {Z : C} (h : (shiftFunctor C 1).obj (X.ω₁.obj (ComposableArrows.mk₁ f')) ⟶ Z) : CategoryStruct.comp (X.ω₁.map β) (CategoryStruct.comp (X.δ f' g') h) = CategoryStruct.comp (X.δ f g) (CategoryStruct.comp ((shiftFunctor C 1).map (X.ω₁.map α)) h)

@[implicit_reducible]

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 : SpectralObject C ι and composable morphisms f : i ⟶ j and g : j ⟶ k in ι.

Equations

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

@[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_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₁ (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₁ 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

noncomputable def CategoryTheory.Triangulated.SpectralObject.mapTriangle {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} {i' j' k' : ι} {f' : i' ⟶ j'} {g' : j' ⟶ k'} (φ : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') : X.triangle f g ⟶ X.triangle f' g'

Given a spectral object X indexed by ι in a triangulated category, this is the morphisms of distinguished triangles X.triangle f g ⟶ X.triangle f' g' induced by a morphism mk₂ f g ⟶ mk₂ f' g' in ComposableArrows ι 2.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.mapTriangle_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 ι) {i j k : ι} {f : i ⟶ j} {g : j ⟶ k} {i' j' k' : ι} {f' : i' ⟶ j'} {g' : j' ⟶ k'} (φ : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') : (X.mapTriangle φ).hom₂ = X.ω₁.map ((ComposableArrows.functorArrows ι 0 2 2 _proof_8 _proof_4).map φ)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.mapTriangle_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 ι) {i j k : ι} {f : i ⟶ j} {g : j ⟶ k} {i' j' k' : ι} {f' : i' ⟶ j'} {g' : j' ⟶ k'} (φ : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') : (X.mapTriangle φ).hom₃ = X.ω₁.map ((ComposableArrows.functorArrows ι 1 2 2 _proof_2 _proof_4).map φ)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.mapTriangle_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 ι) {i j k : ι} {f : i ⟶ j} {g : j ⟶ k} {i' j' k' : ι} {f' : i' ⟶ j'} {g' : j' ⟶ k'} (φ : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') : (X.mapTriangle φ).hom₁ = X.ω₁.map ((ComposableArrows.functorArrows ι 0 1 2 _proof_6 _proof_2).map φ)

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.

Equations

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

@[implicit_reducible]

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 object by a triangulated functor.

Equations

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

@[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_reducible]

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 ι)

Equations

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

@[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 ι} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.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.ω₁

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

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 ι} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {Z : Functor (ComposableArrows ι 1) C} (h : Z✝.ω₁ ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g).hom h = CategoryStruct.comp f.hom (CategoryStruct.comp g.hom h)

def CategoryTheory.Triangulated.SpectralObject.triangleMap {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) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : X.triangle f g ⟶ Y.triangle f g

If φ : X ⟶ Y is a morphism of spectral objects indexed by ι in a triangulated category, this is the induced morphism of distinguished triangles X.triangle f g ⟶ Y.triangle f g associated to two composable morphisms f and g in ι.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.triangleMap_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 ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (triangleMap φ f g).hom₃ = φ.hom.app (ComposableArrows.mk₁ g)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.triangleMap_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 ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (triangleMap φ f g).hom₁ = φ.hom.app (ComposableArrows.mk₁ f)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.triangleMap_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 ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (triangleMap φ f g).hom₂ = φ.hom.app (ComposableArrows.mk₁ (CategoryStruct.comp f g))

@[implicit_reducible]

noncomputable def CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor {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 ι) {A : Type u_4} [Category.{v_4, u_4} A] [Abelian A] (F : Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] : Abelian.SpectralObject A ι

If X is a spectral object indexed by ι in a triangulated category C, and F : C ⥤ A is a homological functor, this is the spectral object in the abelian category A that is obtained by applying F to X.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor_H {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 ι) {A : Type u_4} [Category.{v_4, u_4} A] [Abelian A] (F : Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (n : ℤ) : (X.mapHomologicalFunctor F).H n = X.ω₁.comp (F.shift n)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor_δ {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 ι) {A : Type u_4} [Category.{v_4, u_4} A] [Abelian A] (F : Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁ := by lia) : (X.mapHomologicalFunctor F).δ f g n₀ n₁ h = F.homologySequenceδ (X.triangle f g) n₀ n₁ h

@[implicit_reducible]

noncomputable def CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctorFunctor {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {A : Type u_4} [Category.{v_4, u_4} A] [Abelian A] (F : Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (ι : Type u_5) [Category.{v_5, u_5} ι] : Functor (SpectralObject C ι) (Abelian.SpectralObject A ι)

Given a homological functor F : C ⥤ A, this is the functor which sends a spectral object X : SpectralObject C ι in the triangulated category C to the spectral object X.mapHomologicalFunctor F in the abelian category A.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctorFunctor_map_hom {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {A : Type u_4} [Category.{v_4, u_4} A] [Abelian A] (F : Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (ι : Type u_5) [Category.{v_5, u_5} ι] {X✝ Y✝ : SpectralObject C ι} (φ : X✝ ⟶ Y✝) (n : ℤ) : ((mapHomologicalFunctorFunctor F ι).map φ).hom n = Functor.whiskerRight φ.hom (F.shift n)

@[simp]

theorem CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctorFunctor_obj {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {A : Type u_4} [Category.{v_4, u_4} A] [Abelian A] (F : Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (ι : Type u_5) [Category.{v_5, u_5} ι] (X : SpectralObject C ι) : (mapHomologicalFunctorFunctor F ι).obj X = X.mapHomologicalFunctor F

@[implicit_reducible]

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.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapTriangulatedSpectralObject_map_hom {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} ι] {X✝ Y✝ : Triangulated.SpectralObject C ι} (α : X✝ ⟶ Y✝) : ((F.mapTriangulatedSpectralObject ι).map α).hom = whiskerRight α.hom F

@[simp]

theorem CategoryTheory.Functor.mapTriangulatedSpectralObject_obj {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} ι] (X : Triangulated.SpectralObject C ι) : (F.mapTriangulatedSpectralObject ι).obj X = X.mapTriangulatedFunctor F