Theorems · Theorem · category theory

DerivedCategory.quotientCompQhIso_inv_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),
  CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map f) ((DerivedCategory.quotientCompQhIso C).inv.app L) =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.quotientCompQhIso C).inv.app K)
      (DerivedCategory.Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f))

Defined in

Mathlib.Algebra.Homology.DerivedCategory.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategory