Theorems · Definition · category theory

CategoryTheory.Abelian.SpectralObject.dShortComplex

{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} ι] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} →
              (i₀ ⟶ i₁) →
                (i₁ ⟶ i₂) →
                  (i₂ ⟶ i₃) →
                    (i₃ ⟶ i₄) →
                      (i₄ ⟶ i₅) →
                        (i₅ ⟶ i₆) →
                          (i₆ ⟶ i₇) →
                            (n₀ n₁ n₂ n₃ n₄ : ℤ) →
                              autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_1 →
                                autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_3 →
                                  autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_5 →
                                    autoParam (n₃ + 1 = n₄)
                                        CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_7 →
                                      CategoryTheory.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.

Defined in

Mathlib.Algebra.Homology.SpectralObject.Homology

Cited by

15 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.Category