Theorems · Theorem · category theory

CategoryTheory.Functor.leftDerived_map_eq

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) {X Y : C}
  (f : X ⟶ Y) {P : CategoryTheory.ProjectiveResolution X} {Q : CategoryTheory.ProjectiveResolution Y}
  (g : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f) →
    (F.leftDerived n).map f =
      CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom
        (CategoryTheory.CategoryStruct.comp
          (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp
                (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map
            g)
          (Q.isoLeftDerivedObj F n).inv)

We can compute a left derived functor on a morphism using a descent of that morphism to a chain map between chosen projective resolutions.

Defined in

Mathlib.CategoryTheory.Abelian.LeftDerived

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.HasProjectiveResolutionsCategoryTheory.AbelianCategoryTheory.Functor.Additive