The homology of the differentials of a spectral object

Let X be a spectral object indexed by a category ι in an abelian category C. Assume we have seven composable arrows f₁, f₂, f₃, f₄, f₅, f₆, f₇ in ι. In this file, we compute the homology of the differentials, i.e. the homology of the short complex E^{n - 1}(f₅, f₆, f₇) ⟶ E^n(f₃, f₄, f₅) ⟶ E^{n + 1}(f₁, f₂, f₃). The main definition for this is dHomologyData which is a homology data for this short complex where:

• the cycles are E^n(f₂ ≫ f₃, f₄, f₅);
• the opcycles are E^n(f₃, f₄, f₅ ≫ f₆);
• the homology is E^n(f₂ ≫ f₃, f₄, f₅ ≫ f₆).

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

The exact sequence expressing E^n(f₁, f₂, f₃ ≫ f₄) as the cokernel of the differential E^{n-1}(f₃, f₄, f₅) ⟶ E^n(f₁, f₂, f₃)

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance CategoryTheory.Abelian.SpectralObject.instEpiGDCokernelSequence {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ) (x✝ : n₀ + 1 = n₁) (x✝¹ : n₁ + 1 = n₂) (x✝² : n₂ + 1 = n₃) : Epi (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ x✝ x✝¹ x✝²).g

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

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

The exact sequence expressing E^n(f₂ ≫ f₃, f₄, f₅) as the kernel of the differential E^n(f₃, f₄, f₅) ⟶ E^{n+1}(f₁, f₂, f₃)

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance CategoryTheory.Abelian.SpectralObject.instMonoFDKernelSequence {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ) (x✝ : n₀ + 1 = n₁) (x✝¹ : n₁ + 1 = n₂) (x✝² : n₂ + 1 = n₃) : Mono (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ x✝ x✝¹ x✝²).f

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

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

The short complex E^{n-1}(f₅, f₆, f₇) ⟶ E^{n}(f₃, f₄, f₅) ⟶ E^{n+1}(f₁, f₂, f₃) given by the differentials of a spectral object.

Equations

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dShortComplex_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).f = X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dShortComplex_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).X₁ = X.E f₅ f₆ f₇ n₀ n₁ n₂ ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dShortComplex_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).g = X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dShortComplex_X₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).X₂ = X.E f₃ f₄ f₅ n₁ n₂ n₃ ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dShortComplex_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).X₃ = X.E f₁ f₂ f₃ n₂ n₃ n₄ ⋯ ⋯

theorem CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₁ i₂ i₃ i₄ i₅ i₆ : ι} (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (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.map f₂₃ f₄ f₅ f₃ f₄ f₅ (ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯) (X.map f₃ f₄ f₅ f₃ f₄ f₅₆ (ComposableArrows.fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯) = CategoryStruct.comp (X.map f₂₃ f₄ f₅ f₂₃ f₄ f₅₆ (ComposableArrows.fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯) (X.map f₂₃ f₄ f₅₆ f₃ f₄ f₅₆ (ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯)

theorem CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₁ i₂ i₃ i₄ i₅ i₆ : ι} (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (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₃ ⋯ ⋯ ⟶ Z) : CategoryStruct.comp (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯) (CategoryStruct.comp (X.map f₃ f₄ f₅ f₃ f₄ f₅₆ (ComposableArrows.fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯) h) = CategoryStruct.comp (X.map f₂₃ f₄ f₅ f₂₃ f₄ f₅₆ (ComposableArrows.fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯) (CategoryStruct.comp (X.map f₂₃ f₄ f₅₆ f₃ f₄ f₅₆ (ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯) h)

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

The homology data of the short complex E^{n-1}(f₅, f₆, f₇) ⟶ E^{n}(f₃, f₄, f₅) ⟶ E^{n+1}(f₁, f₂, f₃) for which

• the cycles are E^n(f₂ ≫ f₃, f₄, f₅);
• the opcycles are E^n(f₃, f₄, f₅ ≫ f₆);
• the homology is E^n(f₂ ≫ f₃, f₄, f₅ ≫ f₆).

Equations

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dHomologyData_right_H {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆) (h₅₆ : CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).right.H = X.E f₂₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dHomologyData_iso_hom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆) (h₅₆ : CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).iso.hom = CategoryStruct.id (X.E f₂₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dHomologyData_left_i {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆) (h₅₆ : CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).left.i = X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₁ n₂ n₃ ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dHomologyData_iso_inv {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆) (h₅₆ : CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).iso.inv = CategoryStruct.id (X.E f₂₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dHomologyData_left_K {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆) (h₅₆ : CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).left.K = X.E f₂₃ f₄ f₅ n₁ n₂ n₃ ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dHomologyData_right_p {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆) (h₅₆ : CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).right.p = X.map f₃ f₄ f₅ f₃ f₄ f₅₆ (ComposableArrows.fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ h₅₆) n₁ n₂ n₃ ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dHomologyData_left_H {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆) (h₅₆ : CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).left.H = X.E f₂₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dHomologyData_left_π {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆) (h₅₆ : CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).left.π = X.map f₂₃ f₄ f₅ f₂₃ f₄ f₅₆ (ComposableArrows.fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dHomologyData_right_ι {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆) (h₅₆ : CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).right.ι = X.map f₂₃ f₄ f₅₆ f₃ f₄ f₅₆ (ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.dHomologyData_right_Q {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆) (h₅₆ : CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).right.Q = X.E f₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯

noncomputable def CategoryTheory.Abelian.SpectralObject.dHomologyIso {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆) (h₅₆ : CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) (hn₄ : n₃ + 1 = n₄ := by lia) : (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ ⋯ ⋯ ⋯ ⋯).homology ≅ X.E f₂₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯

The homology of the short complex E^{n-1}(f₅, f₆, f₇) ⟶ E^{n}(f₃, f₄, f₅) ⟶ E^{n+1}(f₁, f₂, f₃) identifies to E^n(f₂ ≫ f₃, f₄, f₅ ≫ f₆).

Equations

• X.dHomologyIso f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄ = (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ ⋯ ⋯ ⋯ ⋯).left.homologyIso