Theorems · Definition · category theory

CategoryTheory.SpectralSequence.pageFunctor

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

The functor SpectralSequence C c r₀ ⥤ HomologicalComplex C (c r) which sends a spectral sequence to its rth page.

Defined in

Mathlib.Algebra.Homology.SpectralSequence.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian