Theorems · Definition · category theory

CategoryTheory.SpectralSequence.iso

{C : Type u_1} →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        {c : ℤ → ComplexShape κ} →
          {r₀ : ℤ} →
            (self : CategoryTheory.SpectralSequence C c r₀) →
              (r r' : ℤ) →
                (pq : κ) →
                  (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence._auto_3) →
                    (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_5) →
                      (self.page r ⋯).homology pq ≅ (self.page r' ⋯).X pq

the isomorphism between the homology of the r-th page at an object pq : κ and the corresponding object on the next page

Defined in

Mathlib.Algebra.Homology.SpectralSequence.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian