Pointwise left derived functors

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

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

Note: this file was obtained by dualizing the definitions in the file Functor.Derived.PointwiseRightDerived. These two files should be kept in sync.

class CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt {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 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.

• hasLimit' : W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj X)

  Use the more general hasLimit lemma instead, see also hasPointwiseLeftDerivedFunctorAt_iff

@[reducible, inline]

abbrev CategoryTheory.Functor.HasPointwiseLeftDerivedFunctor {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 left derived functor with respect to W : MorphismProperty C if it has a pointwise left derived functor at X for any X : C.

Equations

• F.HasPointwiseLeftDerivedFunctor W = ∀ (X : C), F.HasPointwiseLeftDerivedFunctorAt W X

theorem CategoryTheory.Functor.hasPointwiseLeftDerivedFunctorAt_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.HasPointwiseLeftDerivedFunctorAt W X ↔ L.HasPointwiseRightKanExtensionAt F (L.obj X)

theorem CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt.hasLimit {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.HasPointwiseLeftDerivedFunctorAt W X] : L.HasPointwiseRightKanExtensionAt F (L.obj X)

theorem CategoryTheory.Functor.hasPointwiseLeftDerivedFunctorAt_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.HasPointwiseLeftDerivedFunctorAt W X ↔ F.HasPointwiseLeftDerivedFunctorAt W Y

theorem CategoryTheory.Functor.hasPointwiseRightKanExtension_of_hasPointwiseLeftDerivedFunctor {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.HasPointwiseLeftDerivedFunctor W] [L.IsLocalization W] : L.HasPointwiseRightKanExtension F

instance CategoryTheory.Functor.hasLeftDerivedFunctor_of_hasPointwiseLeftDerivedFunctor {C : Type u₁} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₃, u₃} H] (F : Functor C H) (W : MorphismProperty C) [F.HasPointwiseLeftDerivedFunctor W] : F.HasLeftDerivedFunctor W

noncomputable def CategoryTheory.Functor.isPointwiseRightKanExtensionOfHasPointwiseLeftDerivedFunctor {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} (α : L.comp F' ⟶ F) (W : MorphismProperty C) [F.HasPointwiseLeftDerivedFunctor W] [L.IsLocalization W] [F'.IsLeftDerivedFunctor α W] : (RightExtension.mk F' α).IsPointwiseRightKanExtension

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

Equations

• F'.isPointwiseRightKanExtensionOfHasPointwiseLeftDerivedFunctor α W = CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsRightKanExtension F' α

def CategoryTheory.Functor.isPointwiseRightKanExtensionAtOfIsoOfIsLocalization {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) : (RightExtension.mk G e.inv).IsPointwiseRightKanExtensionAt (L.obj Y)

If L : C ⥤ D is a localization functor for W and e : F ≅ L ⋙ G is an isomorphism, then e.inv makes G a pointwise right 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.isPointwiseRightKanExtensionOfIsoOfIsLocalization {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] : (RightExtension.mk G e.inv).IsPointwiseRightKanExtension

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

Equations

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

noncomputable def CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionOfIsIsoOfIsLocalization {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.RightExtension F) [IsIso E.hom] [L.IsLocalization W] : E.IsPointwiseRightKanExtension

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 : L ⋙ E.right ⟶ F is an isomorphism, then E is a pointwise right Kan extension.

Equations

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

theorem CategoryTheory.Functor.hasPointwiseLeftDerivedFunctor_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.HasPointwiseLeftDerivedFunctor W

theorem CategoryTheory.Functor.isLeftDerivedFunctor_of_inverts {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] (F' : Functor D H) (e : L.comp F' ≅ F) : F'.IsLeftDerivedFunctor e.hom W

instance CategoryTheory.Functor.instIsLeftDerivedFunctorLiftHomFac {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] (hF : W.IsInvertedBy F) : (Localization.lift F hF L).IsLeftDerivedFunctor (Localization.fac F hF L).hom W

theorem CategoryTheory.Functor.isIso_of_isLeftDerivedFunctor_of_inverts {C : Type u₁} {D : Type u₂} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} H] {L : Functor C D} {W : MorphismProperty C} [L.IsLocalization W] {F : Functor C H} (LF : Functor D H) (α : L.comp LF ⟶ F) (hF : W.IsInvertedBy F) [LF.IsLeftDerivedFunctor α W] : IsIso α

theorem CategoryTheory.Functor.isLeftDerivedFunctor_iff_of_inverts {C : Type u₁} {D : Type u₂} {H : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} H] {L : Functor C D} {W : MorphismProperty C} [L.IsLocalization W] {F : Functor C H} (LF : Functor D H) (α : L.comp LF ⟶ F) (hF : W.IsInvertedBy F) : LF.IsLeftDerivedFunctor α W ↔ IsIso α