Documentation

Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Left derived functors #

In this file, given a functor F : C ⥤ H, and L : C ⥤ D that is a localization functor for W : MorphismProperty C, we define F.totalLeftDerived L W : D ⥤ H as the right Kan extension of F along L: it is defined if the type class F.HasLeftDerivedFunctor W asserting the existence of a right Kan extension is satisfied. (The name totalLeftDerived is to avoid name-collision with Functor.leftDerived which are the left derived functors in the context of abelian categories.)

Given LF : D ⥤ H and α : L ⋙ RF ⟶ F, we also introduce a type class F.IsLeftDerivedFunctor α W saying that α is a right Kan extension of F along the localization functor L.

(This file was obtained by dualizing the results in the file Mathlib.CategoryTheory.Functor.Derived.RightDerived.)

References #

https://ncatlab.org/nlab/show/derived+functor

class CategoryTheory.Functor.IsLeftDerivedFunctor {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] :

A functor LF : D ⥤ H is a left derived functor of F : C ⥤ H if it is equipped with a natural transformation α : L ⋙ LF ⟶ F which makes it a right Kan extension of F along L, where L : C ⥤ D is a localization functor for W : MorphismProperty C.

isRightKanExtension : LF.IsRightKanExtension α

Instances

theorem CategoryTheory.Functor.isLeftDerivedFunctor_iff_isRightKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_5} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Category.{u_6, u_5} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] :

LF.IsLeftDerivedFunctor α W ↔ LF.IsRightKanExtension α

theorem CategoryTheory.Functor.isLeftDerivedFunctor_iff_of_iso {C : Type u_1} {D : Type u_6} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_6} D] [Category.{u_2, u_3} H] (LF' LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (α' : L.comp LF' ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] (e : LF ≅ LF') (comm : CategoryStruct.comp (whiskerLeft L e.hom) α' = α) :

LF.IsLeftDerivedFunctor α W ↔ LF'.IsLeftDerivedFunctor α' W

noncomputable def CategoryTheory.Functor.leftDerivedLift {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) :

G ⟶ LF

Constructor for natural transformations to a left derived functor.

Equations

LF.leftDerivedLift α W G β = LF.liftOfIsRightKanExtension α G β

Instances For

@[simp]

theorem CategoryTheory.Functor.leftDerived_fac {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) :

CategoryStruct.comp (whiskerLeft L (LF.leftDerivedLift α W G β)) α = β

@[simp]

theorem CategoryTheory.Functor.leftDerived_fac_assoc {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) {Z : Functor C H} (h : F ⟶ Z) :

CategoryStruct.comp (whiskerLeft L (LF.leftDerivedLift α W G β)) (CategoryStruct.comp α h) = CategoryStruct.comp β h

@[simp]

theorem CategoryTheory.Functor.leftDerived_fac_app {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) (X : C) :

CategoryStruct.comp ((LF.leftDerivedLift α W G β).app (L.obj X)) (α.app X) = β.app X

@[simp]

theorem CategoryTheory.Functor.leftDerived_fac_app_assoc {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) (X : C) {Z : H} (h : F.obj X ⟶ Z) :

CategoryStruct.comp ((LF.leftDerivedLift α W G β).app (L.obj X)) (CategoryStruct.comp (α.app X) h) = CategoryStruct.comp (β.app X) h

theorem CategoryTheory.Functor.leftDerived_ext {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (γ₁ γ₂ : G ⟶ LF) (hγ : CategoryStruct.comp (whiskerLeft L γ₁) α = CategoryStruct.comp (whiskerLeft L γ₂) α) :

γ₁ = γ₂

noncomputable def CategoryTheory.Functor.leftDerivedNatTrans {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) :

LF' ⟶ LF

The natural transformation LF' ⟶ LF on left derived functors that is induced by a natural transformation F' ⟶ F.

Equations

LF'.leftDerivedNatTrans LF α' α W τ = LF.leftDerivedLift α W LF' (CategoryTheory.CategoryStruct.comp α' τ)

Instances For

@[simp]

theorem CategoryTheory.Functor.leftDerivedNatTrans_fac {C : Type u_1} {D : Type u_6} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_6} D] [Category.{u_2, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) :

CategoryStruct.comp (whiskerLeft L (LF'.leftDerivedNatTrans LF α' α W τ)) α = CategoryStruct.comp α' τ

@[simp]

theorem CategoryTheory.Functor.leftDerivedNatTrans_fac_assoc {C : Type u_1} {D : Type u_6} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_6} D] [Category.{u_2, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) {Z : Functor C H} (h : F ⟶ Z) :

CategoryStruct.comp (whiskerLeft L (LF'.leftDerivedNatTrans LF α' α W τ)) (CategoryStruct.comp α h) = CategoryStruct.comp α' (CategoryStruct.comp τ h)

@[simp]

theorem CategoryTheory.Functor.leftDerivedNatTrans_app {C : Type u_1} {D : Type u_6} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_6} D] [Category.{u_2, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) (X : C) :

CategoryStruct.comp ((LF'.leftDerivedNatTrans LF α' α W τ).app (L.obj X)) (α.app X) = CategoryStruct.comp (α'.app X) (τ.app X)

@[simp]

theorem CategoryTheory.Functor.leftDerivedNatTrans_app_assoc {C : Type u_1} {D : Type u_6} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_6} D] [Category.{u_2, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) (X : C) {Z : H} (h : F.obj X ⟶ Z) :

CategoryStruct.comp ((LF'.leftDerivedNatTrans LF α' α W τ).app (L.obj X)) (CategoryStruct.comp (α.app X) h) = CategoryStruct.comp (α'.app X) (CategoryStruct.comp (τ.app X) h)

@[simp]

theorem CategoryTheory.Functor.leftDerivedNatTrans_id {C : Type u_5} {D : Type u_1} {H : Type u_3} [Category.{u_6, u_5} C] [Category.{u_4, u_1} D] [Category.{u_2, u_3} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] :

LF.leftDerivedNatTrans LF α α W (CategoryStruct.id F) = CategoryStruct.id LF

@[simp]

theorem CategoryTheory.Functor.leftDerivedNatTrans_comp {C : Type u_1} {D : Type u_5} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_6, u_5} D] [Category.{u_2, u_3} H] (LF'' LF' LF : Functor D H) {F F' F'' : Functor C H} {L : Functor C D} (α'' : L.comp LF'' ⟶ F'') (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α' W] (τ' : F'' ⟶ F') (τ : F' ⟶ F) :

CategoryStruct.comp (LF''.leftDerivedNatTrans LF' α'' α' W τ') (LF'.leftDerivedNatTrans LF α' α W τ) = LF''.leftDerivedNatTrans LF α'' α W (CategoryStruct.comp τ' τ)

@[simp]

theorem CategoryTheory.Functor.leftDerivedNatTrans_comp_assoc {C : Type u_1} {D : Type u_5} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_6, u_5} D] [Category.{u_2, u_3} H] (LF'' LF' LF : Functor D H) {F F' F'' : Functor C H} {L : Functor C D} (α'' : L.comp LF'' ⟶ F'') (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α' W] (τ' : F'' ⟶ F') (τ : F' ⟶ F) {Z : Functor D H} (h : LF ⟶ Z) :

CategoryStruct.comp (LF''.leftDerivedNatTrans LF' α'' α' W τ') (CategoryStruct.comp (LF'.leftDerivedNatTrans LF α' α W τ) h) = CategoryStruct.comp (LF''.leftDerivedNatTrans LF α'' α W (CategoryStruct.comp τ' τ)) h

noncomputable def CategoryTheory.Functor.leftDerivedNatIso {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α' W] (τ : F' ≅ F) :

LF' ≅ LF

The natural isomorphism LF' ≅ LF on left derived functors that is induced by a natural isomorphism F' ≅ F.

Equations

LF'.leftDerivedNatIso LF α' α W τ = { hom := LF'.leftDerivedNatTrans LF α' α W τ.hom, inv := LF.leftDerivedNatTrans LF' α α' W τ.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.Functor.leftDerivedNatIso_inv {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α' W] (τ : F' ≅ F) :

(LF'.leftDerivedNatIso LF α' α W τ).inv = LF.leftDerivedNatTrans LF' α α' W τ.inv

@[simp]

theorem CategoryTheory.Functor.leftDerivedNatIso_hom {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF' LF : Functor D H) {F F' : Functor C H} {L : Functor C D} (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α' W] (τ : F' ≅ F) :

(LF'.leftDerivedNatIso LF α' α W τ).hom = LF'.leftDerivedNatTrans LF α' α W τ.hom

@[reducible, inline]

noncomputable abbrev CategoryTheory.Functor.leftDerivedUnique {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF' LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (α'₂ : L.comp LF' ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] [LF'.IsLeftDerivedFunctor α'₂ W] :

LF ≅ LF'

Uniqueness (up to a natural isomorphism) of the left derived functor.

Equations

LF'.leftDerivedUnique LF α α'₂ W = LF.leftDerivedNatIso LF' α α'₂ W (CategoryTheory.Iso.refl F)

Instances For

theorem CategoryTheory.Functor.isLeftDerivedFunctor_iff_isIso_leftDerivedLift {C : Type u_5} {D : Type u_3} {H : Type u_4} [Category.{u_6, u_5} C] [Category.{u_1, u_3} D] [Category.{u_2, u_4} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) (W : MorphismProperty C) [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] (G : Functor D H) (β : L.comp G ⟶ F) :

G.IsLeftDerivedFunctor β W ↔ IsIso (LF.leftDerivedLift α W G β)

class CategoryTheory.Functor.HasLeftDerivedFunctor {C : Type u_1} {H : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} H] (F : Functor C H) (W : MorphismProperty C) :

A functor F : C ⥤ H has a left derived functor with respect to W : MorphismProperty C if it has a right Kan extension along W.Q : C ⥤ W.Localization (or any localization functor L : C ⥤ D for W, see hasLeftDerivedFunctor_iff).

hasRightKanExtension' : W.Q.HasRightKanExtension F

Instances

theorem CategoryTheory.Functor.hasLeftDerivedFunctor_iff {C : Type u_1} {D : Type u_5} {H : Type u_2} [Category.{u_3, u_1} C] [Category.{u_6, u_5} D] [Category.{u_4, u_2} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] :

F.HasLeftDerivedFunctor W ↔ L.HasRightKanExtension F

theorem CategoryTheory.Functor.hasLeftDerivedFunctor_iff_of_iso {C : Type u_1} {H : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} H] {F F' : Functor C H} (e : F ≅ F') (W : MorphismProperty C) :

F.HasLeftDerivedFunctor W ↔ F'.HasLeftDerivedFunctor W

theorem CategoryTheory.Functor.HasLeftDerivedFunctor.hasRightKanExtension {C : Type u_1} {D : Type u_5} {H : Type u_2} [Category.{u_3, u_1} C] [Category.{u_6, u_5} D] [Category.{u_4, u_2} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [F.HasLeftDerivedFunctor W] :

L.HasRightKanExtension F

theorem CategoryTheory.Functor.HasLeftDerivedFunctor.mk' {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (LF : Functor D H) {F : Functor C H} {L : Functor C D} (α : L.comp LF ⟶ F) {W : MorphismProperty C} [L.IsLocalization W] [LF.IsLeftDerivedFunctor α W] :

F.HasLeftDerivedFunctor W

noncomputable def CategoryTheory.Functor.totalLeftDerived {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [F.HasLeftDerivedFunctor W] :

Given a functor F : C ⥤ H, and a localization functor L : D ⥤ H for W, this is the left derived functor D ⥤ H of F, i.e. the right Kan extension of F along L.

Equations

F.totalLeftDerived L W = L.rightKanExtension F

Instances For

noncomputable def CategoryTheory.Functor.totalLeftDerivedCounit {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [F.HasLeftDerivedFunctor W] :

L.comp (F.totalLeftDerived L W) ⟶ F

The canonical natural transformation L ⋙ F.totalLeftDerived L W ⟶ F.

Equations

F.totalLeftDerivedCounit L W = L.rightKanExtensionCounit F

Instances For

instance CategoryTheory.Functor.instIsLeftDerivedFunctorTotalLeftDerivedTotalLeftDerivedCounit {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (F : Functor C H) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [F.HasLeftDerivedFunctor W] :

(F.totalLeftDerived L W).IsLeftDerivedFunctor (F.totalLeftDerivedCounit L W) W