Theorems · Theorem · category theory

CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app

∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] (K : CochainComplex C₁ ℤ),
  F.mapDerivedCategoryFactorsh.hom.app ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).obj K) =
    CategoryTheory.CategoryStruct.comp (F.mapDerivedCategory.map ((DerivedCategory.quotientCompQhIso C₁).hom.app K))
      (CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app K)
        (CategoryTheory.CategoryStruct.comp
          ((DerivedCategory.quotientCompQhIso C₂).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K))
          (DerivedCategory.Qh.map ((F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).inv.app K))))

Defined in

Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategoryCategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategoryCategoryTheory.Functor.AdditiveCategoryTheory.Limits.PreservesFiniteLimitsCategoryTheory.Limits.PreservesFiniteColimits