Theorems · Inductive type · category theory

CategoryTheory.SpectralSequence

(C : Type u_1) →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [CategoryTheory.Abelian C] → {κ : Type u_2} → (ℤ → ComplexShape κ) → ℤ → Type (max (max u_1 u_2) u_3)

Given an abelian category C, a sequence of complex shapes c : ℤ → ComplexShape κ and a starting page r₀ : ℤ, a spectral sequence involves pages which are homological complexes and isomorphisms saying that the homology of a page identifies to the next page.

Defined in

Mathlib.Algebra.Homology.SpectralSequence.Basic

Cited by

22 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian