Theorems · Theorem · category theory

CategoryTheory.Functor.isLeftDerivedFunctor_of_inverts

∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] (F' : CategoryTheory.Functor D H) (e : L.comp F' ≅ F), F'.IsLeftDerivedFunctor e.hom W

Defined in

Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalization