Theorems · Theorem · category theory

HomotopyCategory.homologyFunctor_shiftMap

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} {n : ℤ}
  (f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (a a' : ℤ) (h : n + a = a'),
  (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap
      (CategoryTheory.ShiftedHom.map f (HomotopyCategory.quotient C (ComplexShape.up ℤ))) a a' h =
    CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a).hom.app K)
      (CategoryTheory.CategoryStruct.comp
        ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
        ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a').inv.app L))

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.CategoryWithHomology