Theorems · Definition · category theory

DerivedCategory.homologyFunctorFactorsh

(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        (n : ℤ) →
          DerivedCategory.Qh.comp (DerivedCategory.homologyFunctor C n) ≅
            HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n

The homology functor on the derived category is induced by the homology functor on the homotopy category of cochain complexes.

Defined in

Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Cited by

9 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategory