Theorems · Definition · category theory

CategoryTheory.Abelian.SpectralObject.SpectralSequence.shortComplexIso

{C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r : ℤ) →
                      (hr : r₀ ≤ r) →
                        (pq pq' pq'' : κ) →
                          (hpq : (c r).Rel pq pq') →
                            (hpq' : (c r).Rel pq' pq'') →
                              (n₀ n₁ n₂ n₃ n₄ : ℤ) →
                                (hn₁ : n₀ + 1 = n₁) →
                                  (hn₂ : n₁ + 1 = n₂) →
                                    (hn₃ : n₂ + 1 = n₃) →
                                      (hn₄ : n₃ + 1 = n₄) →
                                        n₂ = data.deg pq' →
                                          ((CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data r hr).sc'
                                              pq pq' pq'' ≅
                                            X.dShortComplex (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
                                              (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
                                              (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
                                              (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄)

The short complex of the rth page of the spectral sequence on position pq' identifies to the short complex given by the differentials of the spectral object. Then, the homology of this short complex can be computed using SpectralSequence.dHomologyIso. (This only applies in the favourable case when there are pq and pq'' such that (c r).Rel pq pq' and (c r).Rel pq' pq'' hold.)

Defined in

Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianPreorder