Theorems · Definition · category theory

CategoryTheory.SpectralSequence.page

{C : Type u_1} →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        {c : ℤ → ComplexShape κ} →
          {r₀ : ℤ} →
            CategoryTheory.SpectralSequence C c r₀ →
              (r : ℤ) → autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_1 → HomologicalComplex C (c r)

the rth page of a spectral sequence is an homological complex

Defined in

Mathlib.Algebra.Homology.SpectralSequence.Basic

Cited by

42 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian