Theorems · Theorem · category theory

CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality_assoc

∀ {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] {X Y : CochainComplex C₁ ℤ} (f : X ⟶ Y)
  {Z : DerivedCategory C₂} (h : DerivedCategory.Q.obj ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapDerivedCategory.map (DerivedCategory.Q.map f))
      (CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app Y) h) =
    CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app X)
      (CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map f))
        h)

Defined in

Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor

Cited by

1 results in Mathlib

Foundations

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

Assumes

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