Theorems · Inductive type · category theory

CategoryTheory.SpectralSequence.Hom

{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₀ → CategoryTheory.SpectralSequence C c r₀ → Type (max u_2 u_3)

A morphism of spectral sequences is a sequence of morphisms between the pages which commutes with the isomorphisms in homology.

Defined in

Mathlib.Algebra.Homology.SpectralSequence.Basic

Cited by

10 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian