Theorems · Definition · category theory

CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData

{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 r' : ℤ) →
                      (hrr' : r + 1 = r') →
                        (hr : r₀ ≤ r) →
                          (pq pq' pq'' : κ) →
                            (c r).prev pq' = pq →
                              (c r).next pq' = pq'' →
                                (i₀' i₀ i₁ i₂ i₃ i₃' : ι) →
                                  i₀' = data.i₀ r' pq' ⋯ →
                                    i₀ = data.i₀ r pq' ⋯ →
                                      i₁ = data.i₁ pq' →
                                        i₂ = data.i₂ pq' →
                                          i₃ = data.i₃ r pq' ⋯ →
                                            i₃' = data.i₃ r' pq' ⋯ →
                                              (n₀ n₁ n₂ : ℤ) →
                                                n₁ = data.deg pq' →
                                                  [X.HasSpectralSequence data] →
                                                    autoParam (n₀ + 1 = n₁)
                                                        CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1 →
                                                      autoParam (n₁ + 1 = n₂)
                                                          CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3 →
                                                        ((CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X
                                                                data r hr).sc'
                                                            pq pq' pq'').HomologyData

The homology data for the short complex given by differentials on the rth page of the spectral sequence which shows that the homology identifies to an object on the next page.

Defined in

Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Cited by

11 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianPreorderCategoryTheory.Abelian.SpectralObject.HasSpectralSequence