Theorems · Theorem · category theory

DerivedCategory.shiftMap_homologyFunctor_map_Qh

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : HomotopyCategory C (ComplexShape.up ℤ)} {n : ℤ}
  (f : K ⟶ (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj L) (a a' : ℤ)
  (h : autoParam (n + a = a') DerivedCategory.shiftMap_homologyFunctor_map_Qh._auto_1),
  (DerivedCategory.homologyFunctor C 0).shiftMap (CategoryTheory.ShiftedHom.map f DerivedCategory.Qh) a a' h =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactorsh C a).hom.app K)
      (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
        ((DerivedCategory.homologyFunctorFactorsh C a').inv.app L))

Defined in

Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategory