Theorems · Definition · category theory

CategoryTheory.Abelian.SpectralObject.dHomologyIso

{C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] →
          (X : CategoryTheory.Abelian.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₃) →
                              CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃ →
                                (f₅₆ : i₄ ⟶ i₆) →
                                  CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆ →
                                    (n₀ n₁ n₂ n₃ n₄ : ℤ) →
                                      (hn₁ :
                                          autoParam (n₀ + 1 = n₁)
                                            CategoryTheory.Abelian.SpectralObject.dHomologyIso._auto_1) →
                                        (hn₂ :
                                            autoParam (n₁ + 1 = n₂)
                                              CategoryTheory.Abelian.SpectralObject.dHomologyIso._auto_3) →
                                          (hn₃ :
                                              autoParam (n₂ + 1 = n₃)
                                                CategoryTheory.Abelian.SpectralObject.dHomologyIso._auto_5) →
                                            (hn₄ :
                                                autoParam (n₃ + 1 = n₄)
                                                  CategoryTheory.Abelian.SpectralObject.dHomologyIso._auto_7) →
                                              (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₆).

Defined in

Mathlib.Algebra.Homology.SpectralObject.Homology

Cited by

0 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.Category