Theorems · Theorem · category theory

DerivedCategory.homologyFunctorFactors_hom_naturality

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ),
  CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctor C n).map (DerivedCategory.Q.map f))
      ((DerivedCategory.homologyFunctorFactors C n).hom.app L) =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n).hom.app K)
      (HomologicalComplex.homologyMap f n)

Defined in

Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategory