Differentials of a spectral object

Let X be a spectral object in an abelian category C indexed by a category ι. In this file, we construct the differentials d : E^{n}(f₃, f₄, f₅) ⟶ E^{n+1}(f₁, f₂, f₃) that are attached to families of five composable morphisms f₁, f₂, f₃, f₄, f₅ in ι. We show that d ≫ d = 0. The homology of these differentials is computed in the file Mathlib/Algebra/Homology/SpectralObject/Homology.lean (TODO).

References

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

noncomputable def CategoryTheory.Abelian.SpectralObject.d {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₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (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 differential E^{n}(f₃, f₄, f₅) ⟶ E^{n+1}(f₁, f₂, f₃) that is attached to a family of five composable morphisms f₁, f₂, f₃, f₄, f₅.

Equations

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

theorem CategoryTheory.Abelian.SpectralObject.toCycles_πE_d {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₃ 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₃ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (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.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)) = CategoryStruct.comp (X.δ f₁₂ f₃₄ n₁ n₂ hn₂) (CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₂) (X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃))

theorem CategoryTheory.Abelian.SpectralObject.toCycles_πE_d_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₃ 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₃ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (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₃₄ h₃₄ n₁) (CategoryStruct.comp (X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) h)) = CategoryStruct.comp (X.δ f₁₂ f₃₄ n₁ n₂ hn₂) (CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₂) (CategoryStruct.comp (X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) h))

theorem CategoryTheory.Abelian.SpectralObject.d_ι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₀ 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₃₄) (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) : CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) (CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₂)) = CategoryStruct.comp (X.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.fromOpcycles f₄ f₅ f₄₅ h₄₅ n₁) (X.δ f₂₃ f₄₅ n₁ n₂ hn₂))

theorem CategoryTheory.Abelian.SpectralObject.d_ι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₀ 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₃₄) (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) {Z : C} (h : (X.H n₂).obj (ComposableArrows.mk₁ f₂₃) ⟶ Z) : CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ 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.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.fromOpcycles f₄ f₅ f₄₅ h₄₅ n₁) (CategoryStruct.comp (X.δ f₂₃ f₄₅ n₁ n₂ hn₂) h))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.d_d {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₃ 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) : CategoryStruct.comp (X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) (X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.d_d_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₃ 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) {Z : C} (h : X.E f₁ f₂ f₃ n₂ n₃ n₄ hn₃ hn₄ ⟶ Z) : CategoryStruct.comp (X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) (CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄) h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Abelian.SpectralObject.Ψ {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₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : X.cycles f₂ f₃ n₀ ⟶ X.opcycles f₁ f₂ n₁

When f₁, f₂ and f₃ are composable morphisms, this is the canonical morphism Z^n(f₂, f₃) ⟶ opZ^{n+1}(f₁, f₂) that is induced both by δ : H^n(f₂ ≫ f₃) ⟶ H^{n+1}(f₁) (see toCycles_Ψ) and by δ : H^n(f₃) ⟶ H^{n+1}(f₁ ≫ f₂) (see Ψ_fromOpcycles). See the lemma πE_d_ιE for the relation between this definition and the differentials d.

Equations

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.toCycles_Ψ {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₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.toCycles f₂ f₃ f₂₃ h₂₃ n₀) (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) = CategoryStruct.comp (X.δ f₁ f₂₃ n₀ n₁ hn₁) (X.pOpcycles f₁ f₂ n₁)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.toCycles_Ψ_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₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : X.opcycles f₁ f₂ n₁ ⟶ Z) : CategoryStruct.comp (X.toCycles f₂ f₃ f₂₃ h₂₃ n₀) (CategoryStruct.comp (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) h) = CategoryStruct.comp (X.δ f₁ f₂₃ n₀ n₁ hn₁) (CategoryStruct.comp (X.pOpcycles f₁ f₂ n₁) h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.Ψ_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₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) (X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁) = CategoryStruct.comp (X.iCycles f₂ f₃ n₀) (X.δ f₁₂ f₃ n₀ n₁ hn₁)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.Ψ_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₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : (X.H n₁).obj (ComposableArrows.mk₁ f₁₂) ⟶ Z) : CategoryStruct.comp (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) (CategoryStruct.comp (X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁) h) = CategoryStruct.comp (X.iCycles f₂ f₃ n₀) (CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.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 j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.cyclesMap f₁₂ f₃ f₂ f₃ (ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀) (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.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 j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : X.opcycles f₁ f₂ n₁ ⟶ Z) : CategoryStruct.comp (X.cyclesMap f₁₂ f₃ f₂ f₃ (ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀) (CategoryStruct.comp (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) h) = CategoryStruct.comp 0 h

theorem CategoryTheory.Abelian.SpectralObject.Ψ_opcyclesMap {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₁₂) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) (X.opcyclesMap f₁ f₂ f₁ f₂₃ (ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) = 0

noncomputable def CategoryTheory.Abelian.SpectralObject.sequenceΨ {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₁₂) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : ComposableArrows C 3

When f₁, f₂ and f₃ are composable morphisms, this is the exact sequence Z^n(f₁ ≫ f₂, f₃) ⟶ Z^n(f₂, f₃) ⟶ opZ^{n+1}(f₁, f₂) ⟶ opZ^{n+1}(f₁, f₂ ≫ f₃).

Equations

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

theorem CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ_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₁₂) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁, f := X.cyclesMap f₁₂ f₃ f₂ f₃ (ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.Exact

theorem CategoryTheory.Abelian.SpectralObject.Ψ_opcyclesMap_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₁₂) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.Exact

theorem CategoryTheory.Abelian.SpectralObject.sequenceΨ_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₁₂) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sequenceΨ f₁ f₂ f₃ f₁₂ h₁₂ f₂₃ h₂₃ n₀ n₁ hn₁).Exact

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.πE_d_ι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₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) : CategoryStruct.comp (X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃)) = X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.πE_d_ι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₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (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.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) (CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) h)) = CategoryStruct.comp (X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂) h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.πE_EIsoH_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₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X.πE (CategoryStruct.id i₀) f₁ (CategoryStruct.id i₁) n₀ n₁ n₂ hn₁ hn₂) (X.EIsoH f₁ n₀ n₁ n₂ hn₁ hn₂).hom = (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.πE_EIsoH_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₁ : ι} (f₁ : i₀ ⟶ i₁) (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 (CategoryStruct.id i₀) f₁ (CategoryStruct.id i₁) n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.EIsoH f₁ n₀ n₁ n₂ hn₁ hn₂).hom h) = CategoryStruct.comp (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom h

theorem CategoryTheory.Abelian.SpectralObject.d_EIsoH_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₂ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) : CategoryStruct.comp (X.d (CategoryStruct.id i₀) f₁ (CategoryStruct.id i₁) f₂ (CategoryStruct.id i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom = CategoryStruct.comp (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom (X.δ f₁ f₂ n₁ n₂ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.d_EIsoH_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₂ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (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.d (CategoryStruct.id i₀) f₁ (CategoryStruct.id i₁) f₂ (CategoryStruct.id i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) (CategoryStruct.comp (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom h) = CategoryStruct.comp (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom (CategoryStruct.comp (X.δ f₁ f₂ n₁ n₂ hn₂) h)