Theorems · Theorem · category theory

DerivedCategory.quotientCompQhIso_hom_naturality_assoc

∀ {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) {Z : DerivedCategory C}
  (h : DerivedCategory.Q.obj L ⟶ Z),
  CategoryTheory.CategoryStruct.comp (DerivedCategory.Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f))
      (CategoryTheory.CategoryStruct.comp ((DerivedCategory.quotientCompQhIso C).hom.app L) h) =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.quotientCompQhIso C).hom.app K)
      (CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map f) h)

Defined in

Mathlib.Algebra.Homology.DerivedCategory.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategory