Theorems · Definition · category theory

CategoryTheory.Abelian.SpectralObject.H

{C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι → ℤ → CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C

A sequence of functors from ComposableArrows ι 1 to the abelian category. The image of mk₁ f will be referred to as H^n(f) in the documentation.

Defined in

Mathlib.Algebra.Homology.SpectralObject.Basic

Cited by

284 results in Mathlib

Foundations

Depth 26 from the axioms, rests on 277 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Abelian