Pointwise right derived functors

We define the pointwise right derived functors using the notion of pointwise left Kan extensions.

We show that if F : C ⥤ H inverts W : MorphismProperty C, then it has a pointwise right derived functor.

class CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt {C : Type u₁} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₃, u₃} H] (F : Functor C H) (W : MorphismProperty C) (X : C) : Prop

Given F : C ⥤ H, W : MorphismProperty C and X : C, we say that F has a pointwise right derived functor at X if F has a left 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 hasPointwiseRightDerivedFunctorAt_iff for the more general equivalence.

• hasColimit' : W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X)

  Use the more general hasColimit lemma instead, see also hasPointwiseRightDerivedFunctorAt_iff

@[reducible, inline]

abbrev CategoryTheory.Functor.HasPointwiseRightDerivedFunctor {C : Type u₁} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₃, u₃} H] (F : Functor C H) (W : MorphismProperty C) : Prop

A functor F : C ⥤ H has a pointwise right derived functor with respect to W : MorphismProperty C if it has a pointwise right derived functor at X for any X : C.

Equations

• F.HasPointwiseRightDerivedFunctor W = ∀ (X : C), F.HasPointwiseRightDerivedFunctorAt W X

theorem CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff {C : Type u₁} {D : Type u₂} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (X : C) : F.HasPointwiseRightDerivedFunctorAt W X ↔ L.HasPointwiseLeftKanExtensionAt F (L.obj X)

theorem CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt.hasColimit {C : Type u₁} {D : Type u₂} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (X : C) [F.HasPointwiseRightDerivedFunctorAt W X] : L.HasPointwiseLeftKanExtensionAt F (L.obj X)

theorem CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff_of_mem {C : Type u₁} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₃, u₃} H] (F : Functor C H) (W : MorphismProperty C) {X Y : C} (w : X ⟶ Y) (hw : W w) : F.HasPointwiseRightDerivedFunctorAt W X ↔ F.HasPointwiseRightDerivedFunctorAt W Y

theorem CategoryTheory.Functor.hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor {C : Type u₁} {D : Type u₂} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [F.HasPointwiseRightDerivedFunctor W] [L.IsLocalization W] : L.HasPointwiseLeftKanExtension F

instance CategoryTheory.Functor.hasRightDerivedFunctor_of_hasPointwiseRightDerivedFunctor {C : Type u₁} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₃, u₃} H] (F : Functor C H) (W : MorphismProperty C) [F.HasPointwiseRightDerivedFunctor W] : F.HasRightDerivedFunctor W

noncomputable def CategoryTheory.Functor.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor {C : Type u₁} {D : Type u₂} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} H] (F' : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp F') (W : MorphismProperty C) [F.HasPointwiseRightDerivedFunctor W] [L.IsLocalization W] [F'.IsRightDerivedFunctor α W] : (LeftExtension.mk F' α).IsPointwiseLeftKanExtension

A right derived functor is a pointwise right derived functor when there exists a pointwise right derived functor.

Equations

• F'.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor α W = CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension F' α

def CategoryTheory.Functor.isPointwiseLeftKanExtensionAtOfIsoOfIsLocalization {C : Type u₁} {D : Type u₂} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} H] {F : Functor C H} {L : Functor C D} (W : MorphismProperty C) {G : Functor D H} (e : F ≅ L.comp G) [L.IsLocalization W] (Y : C) : (LeftExtension.mk G e.hom).IsPointwiseLeftKanExtensionAt (L.obj Y)

If L : C ⥤ D is a localization functor for W and e : F ≅ L ⋙ G is an isomorphism, then e.hom makes G a pointwise left Kan extension of F along L at L.obj Y for any Y : C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsoOfIsLocalization {C : Type u₁} {D : Type u₂} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} H] {F : Functor C H} {L : Functor C D} (W : MorphismProperty C) {G : Functor D H} (e : F ≅ L.comp G) [L.IsLocalization W] : (LeftExtension.mk G e.hom).IsPointwiseLeftKanExtension

If L is a localization functor for W and e : F ≅ L ⋙ G is an isomorphism, then e.hom makes G a poinwise left Kan extension of F along L.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionOfIsIsoOfIsLocalization {C : Type u₁} {D : Type u₂} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} H] {F : Functor C H} {L : Functor C D} (W : MorphismProperty C) (E : L.LeftExtension F) [IsIso E.hom] [L.IsLocalization W] : E.IsPointwiseLeftKanExtension

Let L : C ⥤ D be a localization functor for W, if an extension E of F : C ⥤ H along L is such that the natural transformation E.hom : F ⟶ L ⋙ E.right is an isomorphism, then E is a pointwise left Kan extension.

Equations

• CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionOfIsIsoOfIsLocalization W E = CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsoOfIsLocalization W (CategoryTheory.asIso E.hom)

theorem CategoryTheory.Functor.hasPointwiseRightDerivedFunctor_of_inverts {C : Type u₁} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₃, u₃} H] (F : Functor C H) {W : MorphismProperty C} (hF : W.IsInvertedBy F) : F.HasPointwiseRightDerivedFunctor W