Right 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.totalRightDerived L W : D ⥤ H as the left Kan extension of F along L: it is defined if the type class F.HasRightDerivedFunctor W asserting the existence of a left Kan extension is satisfied. (The name totalRightDerived is to avoid name-collision with Functor.rightDerived which are the right derived functors in the context of abelian categories.)

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

TODO

• refactor Functor.rightDerived (and Functor.leftDerived) when the necessary material enters mathlib: derived categories, injective/projective derivability structures, existence of derived functors from derivability structures.

References

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

class CategoryTheory.Functor.IsRightDerivedFunctor {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] (RF : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] : Prop

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

• isLeftKanExtension : RF.IsLeftKanExtension α

theorem CategoryTheory.Functor.isRightDerivedFunctor_iff_isLeftKanExtension {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] (RF : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] : RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α

theorem CategoryTheory.Functor.isRightDerivedFunctor_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] {RF RF' : Functor D H} {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α' : F ⟶ L.comp RF') (W : MorphismProperty C) [L.IsLocalization W] (e : RF ≅ RF') (comm : CategoryStruct.comp α (whiskerLeft L e.hom) = α') : RF.IsRightDerivedFunctor α W ↔ RF'.IsRightDerivedFunctor α' W

noncomputable def CategoryTheory.Functor.rightDerivedDesc {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] (RF : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (G : Functor D H) (β : F ⟶ L.comp G) : RF ⟶ G

Constructor for natural transformations from a right derived functor.

Equations

• RF.rightDerivedDesc α W G β = RF.descOfIsLeftKanExtension α G β

@[simp]

theorem CategoryTheory.Functor.rightDerived_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] (RF : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (G : Functor D H) (β : F ⟶ L.comp G) : CategoryStruct.comp α (whiskerLeft L (RF.rightDerivedDesc α W G β)) = β

@[simp]

theorem CategoryTheory.Functor.rightDerived_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] (RF : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (G : Functor D H) (β : F ⟶ L.comp G) {Z : Functor C H} (h : L.comp G ⟶ Z) : CategoryStruct.comp α (CategoryStruct.comp (whiskerLeft L (RF.rightDerivedDesc α W G β)) h) = CategoryStruct.comp β h

@[simp]

theorem CategoryTheory.Functor.rightDerived_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] (RF : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (G : Functor D H) (β : F ⟶ L.comp G) (X : C) : CategoryStruct.comp (α.app X) ((RF.rightDerivedDesc α W G β).app (L.obj X)) = β.app X

@[simp]

theorem CategoryTheory.Functor.rightDerived_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] (RF : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (G : Functor D H) (β : F ⟶ L.comp G) (X : C) {Z : H} (h : G.obj (L.obj X) ⟶ Z) : CategoryStruct.comp (α.app X) (CategoryStruct.comp ((RF.rightDerivedDesc α W G β).app (L.obj X)) h) = CategoryStruct.comp (β.app X) h

theorem CategoryTheory.Functor.rightDerived_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] (RF : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (G : Functor D H) (γ₁ γ₂ : RF ⟶ G) (hγ : CategoryStruct.comp α (whiskerLeft L γ₁) = CategoryStruct.comp α (whiskerLeft L γ₂)) : γ₁ = γ₂

noncomputable def CategoryTheory.Functor.rightDerivedNatTrans {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] (RF RF' : Functor D H) {F F' : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (τ : F ⟶ F') : RF ⟶ RF'

The natural transformation RF ⟶ RF' on right derived functors that is induced by a natural transformation F ⟶ F'.

Equations

• RF.rightDerivedNatTrans RF' α α' W τ = RF.rightDerivedDesc α W RF' (CategoryTheory.CategoryStruct.comp τ α')

@[simp]

theorem CategoryTheory.Functor.rightDerivedNatTrans_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] (RF RF' : Functor D H) {F F' : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (τ : F ⟶ F') : CategoryStruct.comp α (whiskerLeft L (RF.rightDerivedNatTrans RF' α α' W τ)) = CategoryStruct.comp τ α'

@[simp]

theorem CategoryTheory.Functor.rightDerivedNatTrans_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] (RF RF' : Functor D H) {F F' : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (τ : F ⟶ F') {Z : Functor C H} (h : L.comp RF' ⟶ Z) : CategoryStruct.comp α (CategoryStruct.comp (whiskerLeft L (RF.rightDerivedNatTrans RF' α α' W τ)) h) = CategoryStruct.comp τ (CategoryStruct.comp α' h)

@[simp]

theorem CategoryTheory.Functor.rightDerivedNatTrans_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] (RF RF' : Functor D H) {F F' : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (τ : F ⟶ F') (X : C) : CategoryStruct.comp (α.app X) ((RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X)) = CategoryStruct.comp (τ.app X) (α'.app X)

@[simp]

theorem CategoryTheory.Functor.rightDerivedNatTrans_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] (RF RF' : Functor D H) {F F' : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (τ : F ⟶ F') (X : C) {Z : H} (h : RF'.obj (L.obj X) ⟶ Z) : CategoryStruct.comp (α.app X) (CategoryStruct.comp ((RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X)) h) = CategoryStruct.comp (τ.app X) (CategoryStruct.comp (α'.app X) h)

@[simp]

theorem CategoryTheory.Functor.rightDerivedNatTrans_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] (RF : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] : RF.rightDerivedNatTrans RF α α W (CategoryStruct.id F) = CategoryStruct.id RF

@[simp]

theorem CategoryTheory.Functor.rightDerivedNatTrans_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] (RF RF' RF'' : Functor D H) {F F' F'' : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (α'' : F'' ⟶ L.comp RF'') (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] [RF'.IsRightDerivedFunctor α' W] (τ : F ⟶ F') (τ' : F' ⟶ F'') : CategoryStruct.comp (RF.rightDerivedNatTrans RF' α α' W τ) (RF'.rightDerivedNatTrans RF'' α' α'' W τ') = RF.rightDerivedNatTrans RF'' α α'' W (CategoryStruct.comp τ τ')

@[simp]

theorem CategoryTheory.Functor.rightDerivedNatTrans_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] (RF RF' RF'' : Functor D H) {F F' F'' : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (α'' : F'' ⟶ L.comp RF'') (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] [RF'.IsRightDerivedFunctor α' W] (τ : F ⟶ F') (τ' : F' ⟶ F'') {Z : Functor D H} (h : RF'' ⟶ Z) : CategoryStruct.comp (RF.rightDerivedNatTrans RF' α α' W τ) (CategoryStruct.comp (RF'.rightDerivedNatTrans RF'' α' α'' W τ') h) = CategoryStruct.comp (RF.rightDerivedNatTrans RF'' α α'' W (CategoryStruct.comp τ τ')) h

noncomputable def CategoryTheory.Functor.rightDerivedNatIso {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] (RF RF' : Functor D H) {F F' : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] [RF'.IsRightDerivedFunctor α' W] (τ : F ≅ F') : RF ≅ RF'

The natural isomorphism RF ≅ RF' on right derived functors that is induced by a natural isomorphism F ≅ F'.

Equations

• RF.rightDerivedNatIso RF' α α' W τ = { hom := RF.rightDerivedNatTrans RF' α α' W τ.hom, inv := RF'.rightDerivedNatTrans RF α' α W τ.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.rightDerivedNatIso_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] (RF RF' : Functor D H) {F F' : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] [RF'.IsRightDerivedFunctor α' W] (τ : F ≅ F') : (RF.rightDerivedNatIso RF' α α' W τ).inv = RF'.rightDerivedNatTrans RF α' α W τ.inv

@[simp]

theorem CategoryTheory.Functor.rightDerivedNatIso_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] (RF RF' : Functor D H) {F F' : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] [RF'.IsRightDerivedFunctor α' W] (τ : F ≅ F') : (RF.rightDerivedNatIso RF' α α' W τ).hom = RF.rightDerivedNatTrans RF' α α' W τ.hom

@[reducible, inline]

noncomputable abbrev CategoryTheory.Functor.rightDerivedUnique {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] (RF RF' : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (α'₂ : F ⟶ L.comp RF') (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] [RF'.IsRightDerivedFunctor α'₂ W] : RF ≅ RF'

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

Equations

• RF.rightDerivedUnique RF' α α'₂ W = RF.rightDerivedNatIso RF' α α'₂ W (CategoryTheory.Iso.refl F)

theorem CategoryTheory.Functor.isRightDerivedFunctor_iff_isIso_rightDerivedDesc {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] (RF : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) (W : MorphismProperty C) [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] (G : Functor D H) (β : F ⟶ L.comp G) : G.IsRightDerivedFunctor β W ↔ IsIso (RF.rightDerivedDesc α W G β)

class CategoryTheory.Functor.HasRightDerivedFunctor {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) : Prop

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

• hasLeftKanExtension' : W.Q.HasLeftKanExtension F

theorem CategoryTheory.Functor.hasRightDerivedFunctor_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.HasRightDerivedFunctor W ↔ L.HasLeftKanExtension F

theorem CategoryTheory.Functor.hasRightDerivedFunctor_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.HasRightDerivedFunctor W ↔ F'.HasRightDerivedFunctor W

theorem CategoryTheory.Functor.HasRightDerivedFunctor.hasLeftKanExtension {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.HasRightDerivedFunctor W] : L.HasLeftKanExtension F

theorem CategoryTheory.Functor.HasRightDerivedFunctor.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] (RF : Functor D H) {F : Functor C H} {L : Functor C D} (α : F ⟶ L.comp RF) {W : MorphismProperty C} [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] : F.HasRightDerivedFunctor W

noncomputable def CategoryTheory.Functor.totalRightDerived {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.HasRightDerivedFunctor W] : Functor D H

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

Equations

• CategoryTheory.Functor.totalRightDerived L W = L.leftKanExtension F

noncomputable def CategoryTheory.Functor.totalRightDerivedUnit {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.HasRightDerivedFunctor W] : F ⟶ L.comp (totalRightDerived L W)

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

Equations

• CategoryTheory.Functor.totalRightDerivedUnit L W = L.leftKanExtensionUnit F

instance CategoryTheory.Functor.instIsRightDerivedFunctorTotalRightDerivedTotalRightDerivedUnit {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.HasRightDerivedFunctor W] : (totalRightDerived L W).IsRightDerivedFunctor (totalRightDerivedUnit L W) W