Theorems · Inductive type · category theory

CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt

{C : Type u₁} →
  {H : Type u₃} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} H] →
        CategoryTheory.Functor C H → CategoryTheory.MorphismProperty C → C → Prop

Given F : C ⥤ H, W : MorphismProperty C and X : C, we say that F has a pointwise left derived functor at X if F has a right Kan extension at L.obj X for any localization functor L : C ⥤ D for W. In the definition, this is stated for L := W.Q, see hasPointwiseLeftDerivedFunctorAt_iff for the more general equivalence.

Defined in

Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Cited by

4 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category