Spectral objects in abelian categories

Let X be a spectral object index by the category ι in the abelian category C. The purpose of this file is to introduce the homology X.E of the short complex X.shortComplex (X.H n₀).obj (mk₁ f₃) ⟶ (X.H n₁).obj (mk₁ f₂) ⟶ (X.H n₂).obj (mk₁ f₁) when f₁, f₂ and f₃ are composable morphisms in ι and the equalities n₀ + 1 = n₁ and n₁ + 1 = n₂ hold (both maps in the short complex are given by X.δ). All the relevant objects in the spectral sequence attached to spectral objects can be defined in terms of this homology X.E: the objects in all pages, including the page at infinity.

References

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

def CategoryTheory.Abelian.SpectralObject.shortComplex {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : ShortComplex C

The short complex consisting of the composition of two morphisms X.δ, given three composable morphisms f₁, f₂ and f₃ in ι, and three consecutive integers.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplex_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = (X.H n₂).obj (ComposableArrows.mk₁ f₁)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplex_X₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = (X.H n₁).obj (ComposableArrows.mk₁ f₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplex_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f = X.δ f₂ f₃ n₀ n₁ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplex_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = X.δ f₁ f₂ n₁ n₂ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplex_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = (X.H n₀).obj (ComposableArrows.mk₁ f₃)

noncomputable def CategoryTheory.Abelian.SpectralObject.E {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : C

The homology of the short complex shortComplex consisting of two morphisms X.δ. In the documentation, we shorten it as E^n₁(f₁, f₂, f₃)

theorem CategoryTheory.Abelian.SpectralObject.isZero_E_of_isZero_H {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X.H n₁).obj (ComposableArrows.mk₁ f₂))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : Limits.IsZero (X.E f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)

def CategoryTheory.Abelian.SpectralObject.shortComplexMap {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯

The functoriality of shortComplex with respect to morphisms in ComposableArrows ι 3.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂).τ₁ = (X.H n₀).map (ComposableArrows.homMk₁ (α.app 2) (α.app 3) ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂).τ₃ = (X.H n₂).map (ComposableArrows.homMk₁ (α.app 0) (α.app 1) ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂).τ₂ = (X.H n₁).map (ComposableArrows.homMk₁ (α.app 1) (α.app 2) ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMap_id {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (CategoryStruct.id (ComposableArrows.mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂ = CategoryStruct.id (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') {i'' j'' k'' l'' : ι} (f₁'' : i'' ⟶ j'') (f₂'' : j'' ⟶ k'') (f₃'' : k'' ⟶ l'') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (β : ComposableArrows.mk₃ f₁' f₂' f₃' ⟶ ComposableArrows.mk₃ f₁'' f₂'' f₃'') (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (CategoryStruct.comp α β) n₀ n₁ n₂ hn₁ hn₂ = CategoryStruct.comp (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) (X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') {i'' j'' k'' l'' : ι} (f₁'' : i'' ⟶ j'') (f₂'' : j'' ⟶ k'') (f₃'' : k'' ⟶ l'') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (β : ComposableArrows.mk₃ f₁' f₂' f₃' ⟶ ComposableArrows.mk₃ f₁'' f₂'' f₃'') (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : ShortComplex C} (h : X.shortComplex f₁'' f₂'' f₃'' n₀ n₁ n₂ ⋯ ⋯ ⟶ Z) : CategoryStruct.comp (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (CategoryStruct.comp α β) n₀ n₁ n₂ hn₁ hn₂) h = CategoryStruct.comp (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂) h)

noncomputable def CategoryTheory.Abelian.SpectralObject.map {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.E f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂

The functoriality of E with respect to morphisms in ComposableArrows ι 3.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.map_id {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.map f₁ f₂ f₃ f₁ f₂ f₃ (CategoryStruct.id (ComposableArrows.mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂ = CategoryStruct.id (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.map_comp {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') {i'' j'' k'' l'' : ι} (f₁'' : i'' ⟶ j'') (f₂'' : j'' ⟶ k'') (f₃'' : k'' ⟶ l'') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (β : ComposableArrows.mk₃ f₁' f₂' f₃' ⟶ ComposableArrows.mk₃ f₁'' f₂'' f₃'') (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.map f₁ f₂ f₃ f₁'' f₂'' f₃'' (CategoryStruct.comp α β) n₀ n₁ n₂ hn₁ hn₂ = CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) (X.map f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.map_comp_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') {i'' j'' k'' l'' : ι} (f₁'' : i'' ⟶ j'') (f₂'' : j'' ⟶ k'') (f₃'' : k'' ⟶ l'') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (β : ComposableArrows.mk₃ f₁' f₂' f₃' ⟶ ComposableArrows.mk₃ f₁'' f₂'' f₃'') (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.E f₁'' f₂'' f₃'' n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X.map f₁ f₂ f₃ f₁'' f₂'' f₃'' (CategoryStruct.comp α β) n₀ n₁ n₂ hn₁ hn₂) h = CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.map f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂) h)

theorem CategoryTheory.Abelian.SpectralObject.isIso_map {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ) (h₀ : IsIso ((X.H n₀).map ((ComposableArrows.functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))) (h₁ : IsIso ((X.H n₁).map ((ComposableArrows.functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))) (h₂ : IsIso ((X.H n₂).map ((ComposableArrows.functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : IsIso (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (hf : IsIso f) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : X.δ f g n₀ n₁ hn₁ = 0

theorem CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (hg : IsIso g) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : X.δ f g n₀ n₁ hn₁ = 0

theorem CategoryTheory.Abelian.SpectralObject.isZero_H_obj_of_isIso {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (hf : IsIso f) (n : ℤ) : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ f))

noncomputable def CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData

E^n₁(f₁, f₂, f₃) identifies to the cokernel of δToCycles : H^{n₀}(f₃) ⟶ Z^{n₁}(f₁, f₂).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_π {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).π = Limits.cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_H {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).H = Limits.cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_K {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).K = X.cycles f₁ f₂ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_i {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).i = X.iCycles f₁ f₂ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_f' {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f' = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁

noncomputable def CategoryTheory.Abelian.SpectralObject.cyclesIso {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).cycles ≅ X.cycles f₁ f₂ n₁

The cycles of the short complex shortComplex at E^{n₁}(f₁, f₂, f₃) identifies to Z^{n₁}(f₁, f₂).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_i {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).iCycles = X.iCycles f₁ f₂ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_i_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₂ ⟶ Z) : CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv (CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).iCycles h) = CategoryStruct.comp (X.iCycles f₁ f₂ n₁) h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom (X.iCycles f₁ f₂ n₁) = (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).iCycles

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : 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.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom (CategoryStruct.comp (X.iCycles f₁ f₂ n₁) h) = CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).iCycles h

noncomputable def CategoryTheory.Abelian.SpectralObject.πE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.cycles f₁ f₂ n₁ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

The epimorphism Z^{n₁}(f₁, f₂) ⟶ E^{n₁}(f₁, f₂, f₃).

@[implicit_reducible]

instance CategoryTheory.Abelian.SpectralObject.instEpiπE {C : Type u_2} {ι : Type u_4} [Category.{u_1, u_2} C] [Category.{u_3, u_4} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Epi (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv = (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).toCycles

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).cycles ⟶ Z) : CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv h) = CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).toCycles h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δToCycles_πE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δToCycles_πE_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : ShortComplex C

The (exact) sequence H^{n-1}(f₃) ⟶ Z^n(f₁, f₂) ⟶ E^n(f₁, f₂, f₃) ⟶ 0.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_X₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = X.cycles f₁ f₂ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = (X.H n₀).obj (ComposableArrows.mk₁ f₃)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

noncomputable def CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≅ { X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁, X₂ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).cycles, X₃ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology, f := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).toCycles, g := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyπ, zero := ⋯ }

The short complex H^{n-1}(f₃) ⟶ Z^n(f₁, f₂) ⟶ E^n(f₁, f₂, f₃) identifies to the cokernel sequence of the definition of the homology of the short complex shortComplex as a cokernel of ShortComplex.toCycles.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_hom_τ₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₃ = CategoryStruct.id (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_inv_τ₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₂ = (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).hom

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_hom_τ₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₂ = (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).inv

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_inv_τ₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₁ = CategoryStruct.id ((X.H n₀).obj (ComposableArrows.mk₁ f₃))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_hom_τ₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₁ = CategoryStruct.id ((X.H n₀).obj (ComposableArrows.mk₁ f₃))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_inv_τ₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₃ = CategoryStruct.id (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_exact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).Exact

instance CategoryTheory.Abelian.SpectralObject.instEpiGCokernelSequenceCyclesE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Epi (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g

noncomputable def CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).RightHomologyData

E^n₁(f₁, f₂, f₃) identifies to the kernel of δFromOpcycles : opZ^{n₁}(f₂, f₃) ⟶ H^{n₂}(f₁).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_p {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).p = X.pOpcycles f₂ f₃ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_ι {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).ι = Limits.kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_Q {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).Q = X.opcycles f₂ f₃ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_H {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).H = Limits.kernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_g' {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g' = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂

noncomputable def CategoryTheory.Abelian.SpectralObject.opcyclesIso {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).opcycles ≅ X.opcycles f₂ f₃ n₁

The opcycles of the short complex shortComplex at E^{n₁}(f₁, f₂, f₃) identifies to opZ^{n₁}(f₂, f₃).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_hom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom = X.pOpcycles f₂ f₃ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_hom_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.opcycles f₂ f₃ n₁ ⟶ Z) : CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles (CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom h) = CategoryStruct.comp (X.pOpcycles f₂ f₃ n₁) h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.pOpcycles f₂ f₃ n₁) (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv = (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).opcycles ⟶ Z) : CategoryStruct.comp (X.pOpcycles f₂ f₃ n₁) (CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv h) = CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles h

noncomputable def CategoryTheory.Abelian.SpectralObject.ιE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.opcycles f₂ f₃ n₁

The monomorphism E^{n₁}(f₁, f₂, f₃) ⟶ opZ^{n₁}(f₂, f₃) ⟶ .

@[implicit_reducible]

instance CategoryTheory.Abelian.SpectralObject.instMonoιE {C : Type u_2} {ι : Type u_4} [Category.{u_1, u_2} C] [Category.{u_3, u_4} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Mono (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) = (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : 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.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom (CategoryStruct.comp (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) h) = CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : 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.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.πE_ιE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) = CategoryStruct.comp (X.iCycles f₁ f₂ n₁) (X.pOpcycles f₂ f₃ n₁)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.πE_ιE_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.opcycles f₂ f₃ n₁ ⟶ Z) : CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (X.iCycles f₁ f₂ n₁) (CategoryStruct.comp (X.pOpcycles f₂ f₃ n₁) h)

noncomputable def CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : ShortComplex C

The (exact) sequence 0 ⟶ E^n(f₁, f₂, f₃) ⟶ opZ^n(f₂, f₃) ⟶ H^{n+1}(f₁).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_X₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = X.opcycles f₂ f₃ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = (X.H n₂).obj (ComposableArrows.mk₁ f₁)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f = X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

noncomputable def CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≅ { X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology, X₂ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).opcycles, X₃ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃, f := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyι, g := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles, zero := ⋯ }

The short complex E^n(f₁, f₂, f₃) ⟶ opZ^n(f₂, f₃) ⟶ H^{n+1}(f₁) identifies to the kernel sequence of the definition of the homology of the short complex shortComplex as a kernel of ShortComplex.fromOpcycles.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₁ = CategoryStruct.id (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₁ = CategoryStruct.id (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₃ = CategoryStruct.id ((X.H n₂).obj (ComposableArrows.mk₁ f₁))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₂ = (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₃ = CategoryStruct.id ((X.H n₂).obj (ComposableArrows.mk₁ f₁))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₂ = (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_exact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).Exact

instance CategoryTheory.Abelian.SpectralObject.instMonoFKernelSequenceOpcyclesE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Mono (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f

noncomputable def CategoryTheory.Abelian.SpectralObject.cokernelSequenceE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : ShortComplex C

The (exact) sequence H^n(f₁) ⊞ H^{n-1}(f₃) ⟶ H^n(f₁ ≫ f₂) ⟶ E^n(f₁, f₂, f₃) ⟶ 0.

@[simp]

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f = Limits.biprod.desc ((X.H n₁).map (ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) (X.δ f₁₂ f₃ n₀ n₁ ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁ = ((X.H n₁).obj (ComposableArrows.mk₁ f₁) ⊞ (X.H n₀).obj (ComposableArrows.mk₁ f₃))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₃ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

instance CategoryTheory.Abelian.SpectralObject.instEpiGCokernelSequenceE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Epi (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_exact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).Exact

noncomputable def CategoryTheory.Abelian.SpectralObject.descE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) {A : C} (x : (X.H n₁).obj (ComposableArrows.mk₁ f₁₂) ⟶ A) (h : CategoryStruct.comp ((X.H n₁).map (ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) x = 0) (hn₁ : n₀ + 1 = n₁) (h' : CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) x = 0) (hn₂ : n₁ + 1 = n₂ := by lia) : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ A

Constructor for morphisms for E^{n₁}(f₁, f₂, f₃).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.toCycles_πE_descE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) {A : C} (x : (X.H n₁).obj (ComposableArrows.mk₁ f₁₂) ⟶ A) (h : CategoryStruct.comp ((X.H n₁).map (ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) x = 0) (hn₁ : n₀ + 1 = n₁) (h' : CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) x = 0) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.descE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ x h hn₁ h' hn₂)) = x

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.toCycles_πE_descE_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) {A : C} (x : (X.H n₁).obj (ComposableArrows.mk₁ f₁₂) ⟶ A) (h : CategoryStruct.comp ((X.H n₁).map (ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) x = 0) (hn₁ : n₀ + 1 = n₁) (h' : CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) x = 0) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h✝ : A ⟶ Z) : CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.descE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ x h hn₁ h' hn₂) h✝)) = CategoryStruct.comp x h✝

noncomputable def CategoryTheory.Abelian.SpectralObject.kernelSequenceE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : ShortComplex C

The (exact) sequence 0 ⟶ E^n(f₁, f₂, f₃) ⟶ H^n(f₂ ≫ f₃) ⟶ H^n(f₃) ⊞ H^{n+1}(f₁).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceE_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceE_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f = CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceE_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = ((X.H n₁).obj (ComposableArrows.mk₁ f₃) ⊞ (X.H n₂).obj (ComposableArrows.mk₁ f₁))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceE_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g = Limits.biprod.lift ((X.H n₁).map (ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)

@[simp]

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

instance CategoryTheory.Abelian.SpectralObject.instMonoFKernelSequenceE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Mono (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceE_exact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact

noncomputable def CategoryTheory.Abelian.SpectralObject.liftE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) {A : C} (x : A ⟶ (X.H n₁).obj (ComposableArrows.mk₁ f₂₃)) (h : CategoryStruct.comp x ((X.H n₁).map (ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) = 0) (hn₂ : n₁ + 1 = n₂) (h' : CategoryStruct.comp x (X.δ f₁ f₂₃ n₁ n₂ hn₂) = 0) (hn₁ : n₀ + 1 = n₁ := by lia) : A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

Constructor for morphisms to E^{n₁}(f₁, f₂, f₃).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.liftE_ιE_fromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) {A : C} (x : A ⟶ (X.H n₁).obj (ComposableArrows.mk₁ f₂₃)) (h : CategoryStruct.comp x ((X.H n₁).map (ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) = 0) (hn₂ : n₁ + 1 = n₂) (h' : CategoryStruct.comp x (X.δ f₁ f₂₃ n₁ n₂ hn₂) = 0) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.liftE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ x h hn₂ h' hn₁) (CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁)) = x

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.liftE_ιE_fromOpcycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) {A : C} (x : A ⟶ (X.H n₁).obj (ComposableArrows.mk₁ f₂₃)) (h : CategoryStruct.comp x ((X.H n₁).map (ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) = 0) (hn₂ : n₁ + 1 = n₂) (h' : CategoryStruct.comp x (X.δ f₁ f₂₃ n₁ n₂ hn₂) = 0) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h✝ : (X.H n₁).obj (ComposableArrows.mk₁ f₂₃) ⟶ Z) : CategoryStruct.comp (X.liftE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ x h hn₂ h' hn₁) (CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) h✝)) = CategoryStruct.comp x h✝

theorem CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_cyclesMap {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (β : ComposableArrows.mk₂ f₁ f₂ ⟶ ComposableArrows.mk₂ f₁' f₂') (hβ : β = ComposableArrows.homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv (ShortComplex.cyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)) = CategoryStruct.comp (X.cyclesMap f₁ f₂ f₁' f₂' β n₁) (X.cyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).inv

theorem CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_cyclesMap_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (β : ComposableArrows.mk₂ f₁ f₂ ⟶ ComposableArrows.mk₂ f₁' f₂') (hβ : β = ComposableArrows.homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : (X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯).cycles ⟶ Z) : CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv (CategoryStruct.comp (ShortComplex.cyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)) h) = CategoryStruct.comp (X.cyclesMap f₁ f₂ f₁' f₂' β n₁) (CategoryStruct.comp (X.cyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).inv h)

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMap_opcyclesIso_hom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (γ : ComposableArrows.mk₂ f₂ f₃ ⟶ ComposableArrows.mk₂ f₂' f₃') (hγ : γ = ComposableArrows.homMk₂ (α.app 1) (α.app 2) (α.app 3) ⋯ ⋯ := by cat_disch) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (ShortComplex.opcyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)) (X.opcyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).hom = CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom (X.opcyclesMap f₂ f₃ f₂' f₃' γ n₁)

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMap_opcyclesIso_hom_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (γ : ComposableArrows.mk₂ f₂ f₃ ⟶ ComposableArrows.mk₂ f₂' f₃') (hγ : γ = ComposableArrows.homMk₂ (α.app 1) (α.app 2) (α.app 3) ⋯ ⋯ := by cat_disch) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.opcycles f₂' f₃' n₁ ⟶ Z) : CategoryStruct.comp (ShortComplex.opcyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)) (CategoryStruct.comp (X.opcyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).hom h) = CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom (CategoryStruct.comp (X.opcyclesMap f₂ f₃ f₂' f₃' γ n₁) h)

theorem CategoryTheory.Abelian.SpectralObject.πE_map {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (β : ComposableArrows.mk₂ f₁ f₂ ⟶ ComposableArrows.mk₂ f₁' f₂') (n₀ n₁ n₂ : ℤ) (hβ : β = ComposableArrows.homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯ := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) = CategoryStruct.comp (X.cyclesMap f₁ f₂ f₁' f₂' β n₁) (X.πE f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.πE_map_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (β : ComposableArrows.mk₂ f₁ f₂ ⟶ ComposableArrows.mk₂ f₁' f₂') (n₀ n₁ n₂ : ℤ) (hβ : β = ComposableArrows.homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯ := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.E f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (X.cyclesMap f₁ f₂ f₁' f₂' β n₁) (CategoryStruct.comp (X.πE f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂) h)

theorem CategoryTheory.Abelian.SpectralObject.map_ιE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (γ : ComposableArrows.mk₂ f₂ f₃ ⟶ ComposableArrows.mk₂ f₂' f₃') (n₀ n₁ n₂ : ℤ) (hγ : γ = ComposableArrows.homMk₂ (α.app 1) (α.app 2) (α.app 3) ⋯ ⋯ := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) (X.ιE f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂) = CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.opcyclesMap f₂ f₃ f₂' f₃' γ n₁)

theorem CategoryTheory.Abelian.SpectralObject.map_ιE_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (γ : ComposableArrows.mk₂ f₂ f₃ ⟶ ComposableArrows.mk₂ f₂' f₃') (n₀ n₁ n₂ : ℤ) (hγ : γ = ComposableArrows.homMk₂ (α.app 1) (α.app 2) (α.app 3) ⋯ ⋯ := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.opcycles f₂' f₃' n₁ ⟶ Z) : CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.ιE f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.opcyclesMap f₂ f₃ f₂' f₃' γ n₁) h)

noncomputable def CategoryTheory.Abelian.SpectralObject.opcyclesToE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.opcycles f₁₂ f₃ n₁ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

The map opZ^n(f₁ ≫ f₂, f₃) ⟶ E^n(f₁, f₂, f₃).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_opcyclesToE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.pOpcycles f₁₂ f₃ n₁) (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) = CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_opcyclesToE_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X.pOpcycles f₁₂ f₃ n₁) (CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesToE_ιE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) = X.opcyclesMap f₁₂ f₃ f₂ f₃ (ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesToE_ιE_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.opcycles f₂ f₃ n₁ ⟶ Z) : CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (X.opcyclesMap f₁₂ f₃ f₂ f₃ (ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₁) h

instance CategoryTheory.Abelian.SpectralObject.instEpiOpcyclesToE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Epi (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)

noncomputable def CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : ShortComplex C

The (exact) sequence H^n(f₁) ⟶ opZ^n(f₁ ≫ f₂, f₃) ⟶ E^n(f₁, f₂, f₃) ⟶ 0.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f = CategoryStruct.comp ((X.H n₁).map (ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) (X.pOpcycles f₁₂ f₃ n₁)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₃ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁ = (X.H n₁).obj (ComposableArrows.mk₁ f₁)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_X₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₂ = X.opcycles f₁₂ f₃ n₁

instance CategoryTheory.Abelian.SpectralObject.instEpiGCokernelSequenceOpcyclesE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Epi (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_exact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).Exact

noncomputable def CategoryTheory.Abelian.SpectralObject.EToCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.cycles f₁ f₂₃ n₁

The map E^n(f₁, f₂, f₃) ⟶ Z^n(f₁, f₂ ≫ f₃).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.EToCycles_i {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂) (X.iCycles f₁ f₂₃ n₁) = CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.EToCycles_i_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (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.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.iCycles f₁ f₂₃ n₁) h) = CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.πE_EToCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂) = X.cyclesMap f₁ f₂ f₁ f₂₃ (ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.πE_EToCycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.cycles f₁ f₂₃ n₁ ⟶ Z) : CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (X.cyclesMap f₁ f₂ f₁ f₂₃ (ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) h

instance CategoryTheory.Abelian.SpectralObject.instMonoEToCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Mono (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂)

noncomputable def CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : ShortComplex C

The (exact) sequence 0 ⟶ E^n(f₁, f₂, f₃) ⟶ Z^n(f₁, f₂ ≫ f₃) ⟶ H^n(f₃).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = (X.H n₁).obj (ComposableArrows.mk₁ f₃)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_X₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = X.cycles f₁ f₂₃ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g = CategoryStruct.comp (X.iCycles f₁ f₂₃ n₁) ((X.H n₁).map (ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f = X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂

instance CategoryTheory.Abelian.SpectralObject.instMonoFKernelSequenceCyclesE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Mono (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_exact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact

noncomputable def CategoryTheory.Abelian.SpectralObject.homologyDataIdId {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex (CategoryStruct.id i) f (CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂).HomologyData

An homology data for X.shortComplex n₀ n₁ n₂ hn₁ hn₂ (𝟙 i) f (𝟙 j), expressing H^n₁(f) as the homology of this short complex, see EIsoH.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_p {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.p = CategoryStruct.id ((X.H n₁).obj (ComposableArrows.mk₁ f))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.homologyDataIdId_iso_hom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).iso.hom = CategoryStruct.id ((X.H n₁).obj (ComposableArrows.mk₁ f))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_Q {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.Q = (X.H n₁).obj (ComposableArrows.mk₁ f)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_ι {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.ι = CategoryStruct.id ((X.H n₁).obj (ComposableArrows.mk₁ f))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_π {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.π = CategoryStruct.id ((X.H n₁).obj (ComposableArrows.mk₁ f))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.homologyDataIdId_iso_inv {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).iso.inv = CategoryStruct.id ((X.H n₁).obj (ComposableArrows.mk₁ f))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_H {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.H = (X.H n₁).obj (ComposableArrows.mk₁ f)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_H {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.H = (X.H n₁).obj (ComposableArrows.mk₁ f)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_i {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.i = CategoryStruct.id ((X.H n₁).obj (ComposableArrows.mk₁ f))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_K {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.K = (X.H n₁).obj (ComposableArrows.mk₁ f)

noncomputable def CategoryTheory.Abelian.SpectralObject.EIsoH {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.E (CategoryStruct.id i) f (CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂ ≅ (X.H n₁).obj (ComposableArrows.mk₁ f)

For any morphism f : i ⟶ j, this is the isomorphism from E^n₁(𝟙 i, f, 𝟙 j) to H^n₁(f).

theorem CategoryTheory.Abelian.SpectralObject.EIsoH_hom_naturality {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j : ι} (f : i ⟶ j) {i' j' : ι} (f' : i' ⟶ j') (α : ComposableArrows.mk₁ f ⟶ ComposableArrows.mk₁ f') (β : ComposableArrows.mk₃ (CategoryStruct.id i) f (CategoryStruct.id j) ⟶ ComposableArrows.mk₃ (CategoryStruct.id i') f' (CategoryStruct.id j')) (n₀ n₁ n₂ : ℤ) (hβ : β = ComposableArrows.homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯ := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.map (CategoryStruct.id i) f (CategoryStruct.id j) (CategoryStruct.id i') f' (CategoryStruct.id j') β n₀ n₁ n₂ hn₁ hn₂) (X.EIsoH f' n₀ n₁ n₂ hn₁ hn₂).hom = CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ((X.H n₁).map α)

noncomputable def CategoryTheory.Abelian.SpectralObject.cyclesIsoH {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : X.cycles (CategoryStruct.id i₀) f n₀ ≅ (X.H n₀).obj (ComposableArrows.mk₁ f)

The isomorphism Z^n(𝟙 _, f) ≅ H^n(f).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.cyclesIsoH f n₀ n₁ hn₁).inv = X.toCycles (CategoryStruct.id i₀) f f ⋯ n₀

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.cyclesIsoH f n₀ n₁ hn₁).hom (X.toCycles (CategoryStruct.id i₀) f f ⋯ n₀) = CategoryStruct.id (X.cycles (CategoryStruct.id i₀) f n₀)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : X.cycles (CategoryStruct.id i₀) f n₀ ⟶ Z) : CategoryStruct.comp (X.cyclesIsoH f n₀ n₁ hn₁).hom (CategoryStruct.comp (X.toCycles (CategoryStruct.id i₀) f f ⋯ n₀) h) = h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.toCycles (CategoryStruct.id i₀) f f ⋯ n₀) (X.cyclesIsoH f n₀ n₁ hn₁).hom = CategoryStruct.id ((X.H n₀).obj (ComposableArrows.mk₁ f))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : (X.H n₀).obj (ComposableArrows.mk₁ f) ⟶ Z) : CategoryStruct.comp (X.toCycles (CategoryStruct.id i₀) f f ⋯ n₀) (CategoryStruct.comp (X.cyclesIsoH f n₀ n₁ hn₁).hom h) = h

noncomputable def CategoryTheory.Abelian.SpectralObject.opcyclesIsoH {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : X.opcycles f (CategoryStruct.id i₁) n₁ ≅ (X.H n₁).obj (ComposableArrows.mk₁ f)

The isomorphism opZ^n(f, 𝟙 _) ≅ H^n(f).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.opcyclesIsoH f n₀ n₁ hn₁).hom = X.fromOpcycles f (CategoryStruct.id i₁) f ⋯ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.fromOpcycles f (CategoryStruct.id i₁) f ⋯ n₁) (X.opcyclesIsoH f n₀ n₁ hn₁).inv = CategoryStruct.id (X.opcycles f (CategoryStruct.id i₁) n₁)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : X.opcycles f (CategoryStruct.id i₁) n₁ ⟶ Z) : CategoryStruct.comp (X.fromOpcycles f (CategoryStruct.id i₁) f ⋯ n₁) (CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv h) = h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_id {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv (X.fromOpcycles f (CategoryStruct.id i₁) f ⋯ n₁) = CategoryStruct.id ((X.H n₁).obj (ComposableArrows.mk₁ f))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_id_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : (X.H n₁).obj (ComposableArrows.mk₁ f) ⟶ Z) : CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv (CategoryStruct.comp (X.fromOpcycles f (CategoryStruct.id i₁) f ⋯ n₁) h) = h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι} (f : i ⟶ j) : CategoryStruct.comp (X.cyclesIsoH f n₁ n₂ hn₂).hom (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).inv = X.πE (CategoryStruct.id i) f (CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι} (f : i ⟶ j) {Z : C} (h : X.E (CategoryStruct.id i) f (CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X.cyclesIsoH f n₁ n₂ hn₂).hom (CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).inv h) = CategoryStruct.comp (X.πE (CategoryStruct.id i) f (CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂) h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι} (f : i ⟶ j) : CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom (X.opcyclesIsoH f n₀ n₁ hn₁).inv = X.ιE (CategoryStruct.id i) f (CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι} (f : i ⟶ j) {Z : C} (h : X.opcycles f (CategoryStruct.id j) n₁ ⟶ Z) : CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom (CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv h) = CategoryStruct.comp (X.ιE (CategoryStruct.id i) f (CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂) h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (ComposableArrows.threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁) (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (ComposableArrows.threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁) (CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : ShortComplex C

The short exact sequence 0 ⟶ opZ^(f₁, f₂ ≫ f₃) ⟶ opZ^n(f₁ ≫ f₂, f₃) ⟶ H^n(f₁, f₂, f₃) ⟶ 0.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = X.opcycles f₁ f₂₃ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f = X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (ComposableArrows.threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_X₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = X.opcycles f₁₂ f₃ n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g = X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂

instance CategoryTheory.Abelian.SpectralObject.instMonoFShortComplexOpcyclesThreeδ₂Toδ₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Mono (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

instance CategoryTheory.Abelian.SpectralObject.instEpiGShortComplexOpcyclesThreeδ₂Toδ₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : Epi (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g

theorem CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_exact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact

theorem CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_shortExact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).ShortExact

theorem CategoryTheory.Abelian.SpectralObject.opcyclesToE_map {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (f₁₂' : i₀' ⟶ i₂') (h₁₂' : CategoryStruct.comp f₁' f₂' = f₁₂') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (β : ComposableArrows.mk₂ f₁₂ f₃ ⟶ ComposableArrows.mk₂ f₁₂' f₃') (n₀ n₁ n₂ : ℤ) (h₀ : β.app 0 = α.app 0 := by cat_disch) (h₁ : β.app 1 = α.app 2 := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) = CategoryStruct.comp (X.opcyclesMap f₁₂ f₃ f₁₂' f₃' β n₁) (X.opcyclesToE f₁' f₂' f₃' f₁₂' h₁₂' n₀ n₁ n₂ hn₁ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.opcyclesToE_map_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (f₁₂' : i₀' ⟶ i₂') (h₁₂' : CategoryStruct.comp f₁' f₂' = f₁₂') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') (β : ComposableArrows.mk₂ f₁₂ f₃ ⟶ ComposableArrows.mk₂ f₁₂' f₃') (n₀ n₁ n₂ : ℤ) (h₀ : β.app 0 = α.app 0 := by cat_disch) (h₁ : β.app 1 = α.app 2 := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.E f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯ ⟶ Z) : CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) h) = CategoryStruct.comp (X.opcyclesMap f₁₂ f₃ f₁₂' f₃' β n₁) (CategoryStruct.comp (X.opcyclesToE f₁' f₂' f₃' f₁₂' h₁₂' n₀ n₁ n₂ hn₁ hn₂) h)