Theorems · Definition · category theory

CategoryTheory.SpectralSequence.pageHomologyNatIso

(C : Type u_1) →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        (c : ℤ → ComplexShape κ) →
          (r₀ r r' : ℤ) →
            (pq : κ) →
              (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.pageHomologyNatIso._auto_1) →
                (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.pageHomologyNatIso._auto_3) →
                  (CategoryTheory.SpectralSequence.pageFunctor C c r₀ r ⋯).comp
                      (HomologicalComplex.homologyFunctor C (c r) pq) ≅
                    (CategoryTheory.SpectralSequence.pageFunctor C c r₀ r' ⋯).comp (HomologicalComplex.eval C (c r') pq)

The natural isomorphism between the homology of a spectral sequence on the object pq : κ of the rth page and the corresponding object on the next page.

Defined in

Mathlib.Algebra.Homology.SpectralSequence.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian