Theorems · Theorem · category theory

HomotopyCategory.homologyShiftIso_hom_app

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

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.CategoryWithHomology