Spectral objects in abelian categories

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

References

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

structure CategoryTheory.Abelian.SpectralObject (C : Type u_1) (ι : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] : Type (max (max (max u_1 u_2) u_3) u_4)

A spectral object in an abelian category category C indexed by a category ι consists of a family of functors H n : ComposableArrows ι 1 ⥤ C for all n : ℤ, and a functorial long exact sequence ⋯ ⟶ (H n₀).obj (mk₁ f) ⟶ (H n₀).obj (mk₁ (f ≫ g)) ⟶ (H n₀).obj (mk₁ g) ⟶ (H n₁).obj (mk₁ f) ⟶ ⋯ when n₀ + 1 = n₁ and f and g are composable morphisms in ι. (This will be shortened as H^n₀(f) ⟶ H^n₀(f ≫ g) ⟶ H^n₀(g) ⟶ H^n₁(f) in the documentation.)

• H (n : ℤ) : Functor (ComposableArrows ι 1) C

  A sequence of functors from ComposableArrows ι 1 to the abelian category. The image of mk₁ f will be referred to as H^n(f) in the documentation.

• δ' (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : (ComposableArrows.functorArrows ι 1 2 2 _proof_2 _proof_4).comp (self.H n₀) ⟶ (ComposableArrows.functorArrows ι 0 1 2 _proof_6 _proof_2).comp (self.H n₁)

  The connecting homomorphism of the spectral object. (Use δ instead.)

• exact₁' (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : ComposableArrows ι 2) : (ComposableArrows.mk₂ ((self.δ' n₀ n₁ h).app D) ((self.H n₁).map ((ComposableArrows.mapFunctorArrows ι 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4).app D))).Exact
• exact₂' (n : ℤ) (D : ComposableArrows ι 2) : (ComposableArrows.mk₂ ((self.H n).map ((ComposableArrows.mapFunctorArrows ι 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4).app D)) ((self.H n).map ((ComposableArrows.mapFunctorArrows ι 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4).app D))).Exact
• exact₃' (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : ComposableArrows ι 2) : (ComposableArrows.mk₂ ((self.H n₀).map ((ComposableArrows.mapFunctorArrows ι 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4).app D)) ((self.δ' n₀ n₁ h).app D)).Exact

def CategoryTheory.Abelian.SpectralObject.δ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.H n₀).obj (ComposableArrows.mk₁ g) ⟶ (X.H n₁).obj (ComposableArrows.mk₁ f)

The connecting homomorphism of the spectral object.

theorem CategoryTheory.Abelian.SpectralObject.δ_naturality {C : Type u_1} {ι : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} ι] [Abelian 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') (n₀ n₁ : ℤ) (hαβ : α.app 1 = β.app 0 := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp ((X.H n₀).map β) (X.δ f' g' n₀ n₁ hn₁) = CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((X.H n₁).map α)

theorem CategoryTheory.Abelian.SpectralObject.δ_naturality_assoc {C : Type u_1} {ι : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} ι] [Abelian 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') (n₀ n₁ : ℤ) (hαβ : α.app 1 = β.app 0 := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : (X.H n₁).obj (ComposableArrows.mk₁ f') ⟶ Z) : CategoryStruct.comp ((X.H n₀).map β) (CategoryStruct.comp (X.δ f' g' n₀ n₁ hn₁) h) = CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (CategoryStruct.comp ((X.H n₁).map α) h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.zero₁ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((X.H n₁).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.zero₁_assoc {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h✝ : (X.H n₁).obj (ComposableArrows.mk₁ fg) ⟶ Z) : CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (CategoryStruct.comp ((X.H n₁).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) h✝) = CategoryStruct.comp 0 h✝

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.zero₂ {C : Type u_1} {ι : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ : ℤ) : CategoryStruct.comp ((X.H n₀).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) ((X.H n₀).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.zero₂_assoc {C : Type u_1} {ι : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ : ℤ) {Z : C} (h✝ : (X.H n₀).obj (ComposableArrows.mk₁ g) ⟶ Z) : CategoryStruct.comp ((X.H n₀).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) (CategoryStruct.comp ((X.H n₀).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)) h✝) = CategoryStruct.comp 0 h✝

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.zero₃ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp ((X.H n₀).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)) (X.δ f g n₀ n₁ hn₁) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.zero₃_assoc {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h✝ : (X.H n₁).obj (ComposableArrows.mk₁ f) ⟶ Z) : CategoryStruct.comp ((X.H n₀).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)) (CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) h✝) = CategoryStruct.comp 0 h✝

def CategoryTheory.Abelian.SpectralObject.sc₁ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : ShortComplex C

The (exact) short complex H^n₀(g) ⟶ H^n₁(f) ⟶ H^n₁(fg) of a spectral object, when f ≫ g = fg and n₀ + 1 = n₁.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₁_X₂ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₁ f g fg h n₀ n₁ hn₁).X₂ = (X.H n₁).obj (ComposableArrows.mk₁ f)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₁_f {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₁ f g fg h n₀ n₁ hn₁).f = X.δ f g n₀ n₁ hn₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₁_X₁ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₁ f g fg h n₀ n₁ hn₁).X₁ = (X.H n₀).obj (ComposableArrows.mk₁ g)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₁_g {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₁ f g fg h n₀ n₁ hn₁).g = (X.H n₁).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₁_X₃ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₁ f g fg h n₀ n₁ hn₁).X₃ = (X.H n₁).obj (ComposableArrows.mk₁ fg)

def CategoryTheory.Abelian.SpectralObject.sc₂ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ : ℤ) : ShortComplex C

The (exact) short complex H^n₀(f) ⟶ H^n₀(fg) ⟶ H^n₀(g) of a spectral object, when f ≫ g = fg.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₂_X₁ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ : ℤ) : (X.sc₂ f g fg h n₀).X₁ = (X.H n₀).obj (ComposableArrows.mk₁ f)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₂_f {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ : ℤ) : (X.sc₂ f g fg h n₀).f = (X.H n₀).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₂_g {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ : ℤ) : (X.sc₂ f g fg h n₀).g = (X.H n₀).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₂_X₂ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ : ℤ) : (X.sc₂ f g fg h n₀).X₂ = (X.H n₀).obj (ComposableArrows.mk₁ fg)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₂_X₃ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ : ℤ) : (X.sc₂ f g fg h n₀).X₃ = (X.H n₀).obj (ComposableArrows.mk₁ g)

def CategoryTheory.Abelian.SpectralObject.sc₃ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : ShortComplex C

The (exact) short complex H^n₀(fg) ⟶ H^n₀(g) ⟶ H^n₁(f) of a spectral object, when f ≫ g = fg and n₀ + 1 = n₁.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₃_X₃ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₃ f g fg h n₀ n₁ hn₁).X₃ = (X.H n₁).obj (ComposableArrows.mk₁ f)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₃_g {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₃ f g fg h n₀ n₁ hn₁).g = X.δ f g n₀ n₁ hn₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₃_f {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₃ f g fg h n₀ n₁ hn₁).f = (X.H n₀).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₃_X₁ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₃ f g fg h n₀ n₁ hn₁).X₁ = (X.H n₀).obj (ComposableArrows.mk₁ fg)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.sc₃_X₂ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₃ f g fg h n₀ n₁ hn₁).X₂ = (X.H n₀).obj (ComposableArrows.mk₁ g)

theorem CategoryTheory.Abelian.SpectralObject.exact₁ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₁ f g fg h n₀ n₁ hn₁).Exact

theorem CategoryTheory.Abelian.SpectralObject.exact₂ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ : ℤ) : (X.sc₂ f g fg h n₀).Exact

theorem CategoryTheory.Abelian.SpectralObject.exact₃ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₃ f g fg h n₀ n₁ hn₁).Exact

@[reducible, inline]

abbrev CategoryTheory.Abelian.SpectralObject.composableArrows₅ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : ComposableArrows C 5

The (exact) sequence H^n₀(f) ⟶ H^n₀(fg) ⟶ H^n₀(g) ⟶ H^n₁(f) ⟶ H^n₁(fg) ⟶ H^n₁(g) of a spectral object, when f ≫ g = fg and n₀ + 1 = n₁.

theorem CategoryTheory.Abelian.SpectralObject.composableArrows₅_exact {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.composableArrows₅ f g fg h n₀ n₁ hn₁).Exact

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δ_δ {C : Type u_1} {ι : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f : i ⟶ j) (g : j ⟶ k) (h : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.δ g h n₀ n₁ hn₁) (X.δ f g n₁ n₂ hn₂) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δ_δ_assoc {C : Type u_1} {ι : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f : i ⟶ j) (g : j ⟶ k) (h : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h✝ : (X.H n₂).obj (ComposableArrows.mk₁ f) ⟶ Z) : CategoryStruct.comp (X.δ g h n₀ n₁ hn₁) (CategoryStruct.comp (X.δ f g n₁ n₂ hn₂) h✝) = CategoryStruct.comp 0 h✝

structure CategoryTheory.Abelian.SpectralObject.Hom {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X X' : SpectralObject C ι) : Type (max (max u_2 u_3) u_4)

The type of morphisms between spectral objects in abelian categories.

• hom (n : ℤ) : X.H n ⟶ X'.H n

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

• comm (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((self.hom n₁).app (ComposableArrows.mk₁ f)) = CategoryStruct.comp ((self.hom n₀).app (ComposableArrows.mk₁ g)) (X'.δ f g n₀ n₁ hn₁)

theorem CategoryTheory.Abelian.SpectralObject.Hom.ext_iff {C : Type u_1} {ι : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} ι} {inst✝² : Abelian C} {X X' : SpectralObject C ι} {x y : X.Hom X'} : x = y ↔ x.hom = y.hom

theorem CategoryTheory.Abelian.SpectralObject.Hom.ext {C : Type u_1} {ι : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} ι} {inst✝² : Abelian C} {X X' : SpectralObject C ι} {x y : X.Hom X'} (hom : x.hom = y.hom) : x = y

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.Hom.comm_assoc {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] {X X' : SpectralObject C ι} (self : X.Hom X') (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {Z : C} (h : (X'.H n₁).obj (ComposableArrows.mk₁ f) ⟶ Z) : CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (CategoryStruct.comp ((self.hom n₁).app (ComposableArrows.mk₁ f)) h) = CategoryStruct.comp ((self.hom n₀).app (ComposableArrows.mk₁ g)) (CategoryStruct.comp (X'.δ f g n₀ n₁ hn₁) h)

@[implicit_reducible]

instance CategoryTheory.Abelian.SpectralObject.instCategory {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] : Category.{max (max u_2 u_3) u_4, max (max (max u_4 u_3) u_2) u_1} (SpectralObject C ι)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.id_hom {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) (x✝ : ℤ) : (CategoryStruct.id X).hom x✝ = CategoryStruct.id (X.H x✝)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.comp_hom {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] {X✝ Y✝ Z✝ : SpectralObject C ι} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (n : ℤ) : (CategoryStruct.comp f g).hom n = CategoryStruct.comp (f.hom n) (g.hom n)

theorem CategoryTheory.Abelian.SpectralObject.comp_hom_assoc {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] {X✝ Y✝ Z✝ : SpectralObject C ι} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (n : ℤ) {Z : Functor (ComposableArrows ι 1) C} (h : Z✝.H n ⟶ Z) : CategoryStruct.comp ((CategoryStruct.comp f g).hom n) h = CategoryStruct.comp (f.hom n) (CategoryStruct.comp (g.hom n) h)

theorem CategoryTheory.Abelian.SpectralObject.isZero_H_map_mk₁_of_isIso {C : Type u_1} {ι : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} ι] [Abelian C] (X : SpectralObject C ι) (n : ℤ) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) [IsIso f] : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ f))

theorem CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) (n₀ : ℤ) {i₀ i₁ i₂ : ι} (f : i₀ ⟶ i₁) (g : i₁ ⟶ i₂) (fg : i₀ ⟶ i₂) (hfg : CategoryStruct.comp f g = fg) (h₁ : Limits.IsZero ((X.H n₀).obj (ComposableArrows.mk₁ f))) : Mono ((X.H n₀).map (ComposableArrows.twoδ₁Toδ₀ f g fg hfg))

theorem CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i₀ i₁ i₂ : ι} (f : i₀ ⟶ i₁) (g : i₁ ⟶ i₂) (fg : i₀ ⟶ i₂) (hfg : CategoryStruct.comp f g = fg) (h₂ : Limits.IsZero ((X.H n₁).obj (ComposableArrows.mk₁ f))) : Epi ((X.H n₀).map (ComposableArrows.twoδ₁Toδ₀ f g fg hfg))

theorem CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} ι] [Abelian C] (X : SpectralObject C ι) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i₀ i₁ i₂ : ι} (f : i₀ ⟶ i₁) (g : i₁ ⟶ i₂) (fg : i₀ ⟶ i₂) (hfg : CategoryStruct.comp f g = fg) (h₁ : Limits.IsZero ((X.H n₀).obj (ComposableArrows.mk₁ f))) (h₂ : Limits.IsZero ((X.H n₁).obj (ComposableArrows.mk₁ f))) : IsIso ((X.H n₀).map (ComposableArrows.twoδ₁Toδ₀ f g fg hfg))

theorem CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀' {C : Type u_1} [Category.{u_4, u_1} C] [Abelian C] {ι' : Type u_3} [Preorder ι'] (X' : SpectralObject C ι') (n₀ : ℤ) (i₀ i₁ i₂ : ι') (h₀₁ : i₀ ≤ i₁) (h₁₂ : i₁ ≤ i₂) (h₁ : Limits.IsZero ((X'.H n₀).obj (ComposableArrows.mk₁ (homOfLE h₀₁)))) : Mono ((X'.H n₀).map (ComposableArrows.twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))

theorem CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀' {C : Type u_1} [Category.{u_4, u_1} C] [Abelian C] {ι' : Type u_3} [Preorder ι'] (X' : SpectralObject C ι') (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) (i₀ i₁ i₂ : ι') (h₀₁ : i₀ ≤ i₁) (h₁₂ : i₁ ≤ i₂) (h₂ : Limits.IsZero ((X'.H n₁).obj (ComposableArrows.mk₁ (homOfLE h₀₁)))) : Epi ((X'.H n₀).map (ComposableArrows.twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))

theorem CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀' {C : Type u_1} [Category.{u_4, u_1} C] [Abelian C] {ι' : Type u_3} [Preorder ι'] (X' : SpectralObject C ι') (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) (i₀ i₁ i₂ : ι') (h₀₁ : i₀ ≤ i₁) (h₁₂ : i₁ ≤ i₂) (h₁ : Limits.IsZero ((X'.H n₀).obj (ComposableArrows.mk₁ (homOfLE h₀₁)))) (h₂ : Limits.IsZero ((X'.H n₁).obj (ComposableArrows.mk₁ (homOfLE h₀₁)))) : IsIso ((X'.H n₀).map (ComposableArrows.twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))