feat(CategoryTheory): right derived functors (#12788)

joelriou · joelriou · commit 77504eef03e7 · 2024-06-05T12:48:17.000Z
In this PR, 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.



Co-authored-by: Joël Riou &lt;37772949+joelriou@users.noreply.github.com&gt;
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1306,6 +1306,7 @@ import Mathlib.CategoryTheory.Functor.Basic
 import Mathlib.CategoryTheory.Functor.Category
 import Mathlib.CategoryTheory.Functor.Const
 import Mathlib.CategoryTheory.Functor.Currying
+import Mathlib.CategoryTheory.Functor.Derived.RightDerived
 import Mathlib.CategoryTheory.Functor.EpiMono
 import Mathlib.CategoryTheory.Functor.Flat
 import Mathlib.CategoryTheory.Functor.FullyFaithful
diff --git a/Mathlib/CategoryTheory/Abelian/LeftDerived.lean b/Mathlib/CategoryTheory/Abelian/LeftDerived.lean
@@ -37,6 +37,16 @@ and show how to compute the components.
 * `Functor.fromLeftDerivedZero`: the natural transformation `F.leftDerived 0 ⟶ F`,
   which is an isomorphism when `F` is right exact (i.e. preserves finite colimits),
   see also `Functor.leftDerivedZeroIsoSelf`.
+
+## TODO
+
+* refactor `Functor.leftDerived` (and `Functor.rightDerived`) when the necessary
+material enters mathlib: derived categories, injective/projective derivability
+structures, existence of derived functors from derivability structures.
+Eventually, we shall get a right derived functor
+`F.leftDerivedFunctorMinus : DerivedCategory.Minus C ⥤ DerivedCategory.Minus D`,
+and `F.leftDerived` shall be redefined using `F.leftDerivedFunctorMinus`.
+
 -/
 
 universe v u
diff --git a/Mathlib/CategoryTheory/Abelian/RightDerived.lean b/Mathlib/CategoryTheory/Abelian/RightDerived.lean
@@ -37,6 +37,16 @@ and show how to compute the components.
 * `Functor.toRightDerivedZero`: the natural transformation `F ⟶ F.rightDerived 0`,
   which is an isomorphism when `F` is left exact (i.e. preserves finite limits),
   see also `Functor.rightDerivedZeroIsoSelf`.
+
+## 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.
+Eventually, we shall get a right derived functor
+`F.rightDerivedFunctorPlus : DerivedCategory.Plus C ⥤ DerivedCategory.Plus D`,
+and `F.rightDerived` shall be redefined using `F.rightDerivedFunctorPlus`.
+
 -/
 
 universe v u
diff --git a/Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean b/Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
@@ -0,0 +1,212 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Functor.KanExtension.Basic
+import Mathlib.CategoryTheory.Localization.Predicate
+
+/-!
+# 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
+
+-/
+
+namespace CategoryTheory
+
+namespace Functor
+
+variable {C C' D D' H H' : Type _} [Category C] [Category C']
+  [Category D] [Category D'] [Category H] [Category H']
+  (RF RF' RF'' : D ⥤ H) {F F' F'' : C ⥤ H} (e : F ≅ F') {L : C ⥤ D}
+  (α : F ⟶ L ⋙ RF) (α' : F' ⟶ L ⋙ RF') (α'' : F'' ⟶ L ⋙ RF'') (α'₂ : F ⟶ L ⋙ RF')
+  (W : MorphismProperty C)
+
+/-- 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`. -/
+class IsRightDerivedFunctor [L.IsLocalization W] : Prop where
+  isLeftKanExtension' : RF.IsLeftKanExtension α
+
+lemma IsRightDerivedFunctor.isLeftKanExtension
+    [L.IsLocalization W] [RF.IsRightDerivedFunctor α W] :
+    RF.IsLeftKanExtension α :=
+  IsRightDerivedFunctor.isLeftKanExtension' W
+
+lemma isRightDerivedFunctor_iff_isLeftKanExtension [L.IsLocalization W] :
+    RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α := by
+  constructor
+  · exact fun _ => IsRightDerivedFunctor.isLeftKanExtension RF α W
+  · exact fun h => ⟨h⟩
+
+variable {RF RF'} in
+lemma isRightDerivedFunctor_iff_of_iso (α' : F ⟶ L ⋙ RF') (W : MorphismProperty C)
+    [L.IsLocalization W] (e : RF ≅ RF') (comm : α ≫ whiskerLeft L e.hom = α') :
+    RF.IsRightDerivedFunctor α W ↔ RF'.IsRightDerivedFunctor α' W := by
+  simp only [isRightDerivedFunctor_iff_isLeftKanExtension]
+  exact isLeftKanExtension_iff_of_iso e _ _ comm
+
+section
+
+variable [L.IsLocalization W] [RF.IsRightDerivedFunctor α W]
+  [RF'.IsRightDerivedFunctor α' W] [RF''.IsRightDerivedFunctor α'' W]
+
+/-- Constructor for natural transformations from a right derived functor. -/
+noncomputable def rightDerivedDesc (G : D ⥤ H) (β : F ⟶ L ⋙ G) : RF ⟶ G :=
+  have := IsRightDerivedFunctor.isLeftKanExtension RF α W
+  RF.descOfIsLeftKanExtension α G β
+
+@[reassoc (attr := simp)]
+lemma rightDerived_fac (G : D ⥤ H) (β : F ⟶ L ⋙ G) :
+    α ≫ whiskerLeft L (RF.rightDerivedDesc α W G β) = β :=
+  have := IsRightDerivedFunctor.isLeftKanExtension RF α W
+  RF.descOfIsLeftKanExtension_fac α G β
+
+@[reassoc (attr := simp)]
+lemma rightDerived_fac_app (G : D ⥤ H) (β : F ⟶ L ⋙ G) (X : C):
+    α.app X ≫ (RF.rightDerivedDesc α W G β).app (L.obj X) = β.app X :=
+  have := IsRightDerivedFunctor.isLeftKanExtension RF α W
+  RF.descOfIsLeftKanExtension_fac_app α G β X
+
+lemma rightDerived_ext (G : D ⥤ H) (γ₁ γ₂ : RF ⟶ G)
+    (hγ : α ≫ whiskerLeft L γ₁ = α ≫ whiskerLeft L γ₂) : γ₁ = γ₂ :=
+  have := IsRightDerivedFunctor.isLeftKanExtension RF α W
+  RF.hom_ext_of_isLeftKanExtension α γ₁ γ₂ hγ
+
+/-- The natural transformation `RF ⟶ RF'` on right derived functors that is
+induced by a natural transformation `F ⟶ F'`.  -/
+noncomputable def rightDerivedNatTrans (τ : F ⟶ F') : RF ⟶ RF' :=
+  RF.rightDerivedDesc α W RF' (τ ≫ α')
+
+@[reassoc (attr := simp)]
+lemma rightDerivedNatTrans_fac (τ : F ⟶ F') :
+    α ≫ whiskerLeft L (rightDerivedNatTrans RF RF' α α' W τ) = τ ≫ α' := by
+  dsimp only [rightDerivedNatTrans]
+  simp
+
+@[reassoc (attr := simp)]
+lemma rightDerivedNatTrans_app (τ : F ⟶ F') (X : C) :
+    α.app X ≫ (rightDerivedNatTrans RF RF' α α' W τ).app (L.obj X) =
+    τ.app X ≫ α'.app X := by
+  dsimp only [rightDerivedNatTrans]
+  simp
+
+@[simp]
+lemma rightDerivedNatTrans_id :
+    rightDerivedNatTrans RF RF α α W (𝟙 F) = 𝟙 RF :=
+  rightDerived_ext RF α W _ _ _ (by aesop_cat)
+
+@[reassoc (attr:= simp)]
+lemma rightDerivedNatTrans_comp (τ : F ⟶ F') (τ' : F' ⟶ F'') :
+    rightDerivedNatTrans RF RF' α α' W τ ≫ rightDerivedNatTrans RF' RF'' α' α'' W τ' =
+    rightDerivedNatTrans RF RF'' α α'' W (τ ≫ τ') :=
+  rightDerived_ext RF α W _ _ _ (by aesop_cat)
+
+/-- The natural isomorphism `RF ≅ RF'` on right derived functors that is
+induced by a natural isomorphism `F ≅ F'`.  -/
+@[simps]
+noncomputable def rightDerivedNatIso (τ : F ≅ F') :
+    RF ≅ RF' where
+  hom := rightDerivedNatTrans RF RF' α α' W τ.hom
+  inv := rightDerivedNatTrans RF' RF α' α W τ.inv
+
+/-- Uniqueness (up to a natural isomorphism) of the right derived functor. -/
+noncomputable abbrev rightDerivedUnique [RF'.IsRightDerivedFunctor α'₂ W] : RF ≅ RF' :=
+  rightDerivedNatIso RF RF' α α'₂ W (Iso.refl F)
+
+lemma isRightDerivedFunctor_iff_isIso_rightDerivedDesc (G : D ⥤ H) (β : F ⟶ L ⋙ G) :
+    G.IsRightDerivedFunctor β W ↔ IsIso (RF.rightDerivedDesc α W G β) := by
+  rw [isRightDerivedFunctor_iff_isLeftKanExtension]
+  have := IsRightDerivedFunctor.isLeftKanExtension _ α W
+  exact isLeftKanExtension_iff_isIso _ α _ (by simp)
+
+end
+
+variable (F)
+
+/-- 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`). -/
+class HasRightDerivedFunctor : Prop where
+  hasLeftKanExtension' : HasLeftKanExtension W.Q F
+
+variable (L)
+variable [L.IsLocalization W]
+
+lemma hasRightDerivedFunctor_iff :
+    F.HasRightDerivedFunctor W ↔ HasLeftKanExtension L F := by
+  have : HasRightDerivedFunctor F W ↔ HasLeftKanExtension W.Q F :=
+    ⟨fun h => h.hasLeftKanExtension', fun h => ⟨h⟩⟩
+  rw [this, hasLeftExtension_iff_postcomp₁ (Localization.compUniqFunctor W.Q L W) F]
+
+variable {F}
+
+lemma hasRightDerivedFunctor_iff_of_iso :
+    HasRightDerivedFunctor F W ↔ HasRightDerivedFunctor F' W := by
+  rw [hasRightDerivedFunctor_iff F W.Q W, hasRightDerivedFunctor_iff F' W.Q W,
+    hasLeftExtension_iff_of_iso₂ W.Q e]
+
+variable (F)
+
+lemma HasRightDerivedFunctor.hasLeftKanExtension [HasRightDerivedFunctor F W] :
+    HasLeftKanExtension L F := by
+  simpa only [← hasRightDerivedFunctor_iff F L W]
+
+variable {F L W}
+
+lemma HasRightDerivedFunctor.mk' [RF.IsRightDerivedFunctor α W] :
+    HasRightDerivedFunctor F W := by
+  have := IsRightDerivedFunctor.isLeftKanExtension RF α W
+  simpa only [hasRightDerivedFunctor_iff F L W] using HasLeftKanExtension.mk RF α
+
+section
+
+variable [F.HasRightDerivedFunctor W] (L W)
+
+/-- 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`. -/
+noncomputable def totalRightDerived : D ⥤ H :=
+  have := HasRightDerivedFunctor.hasLeftKanExtension F L W
+  leftKanExtension L F
+
+/-- The canonical natural transformation `F ⟶ L ⋙ F.totalRightDerived L W`. -/
+noncomputable def totalRightDerivedUnit : F ⟶ L ⋙ F.totalRightDerived L W :=
+  have := HasRightDerivedFunctor.hasLeftKanExtension F L W
+  leftKanExtensionUnit L F
+
+instance : (F.totalRightDerived L W).IsRightDerivedFunctor
+    (F.totalRightDerivedUnit L W) W where
+  isLeftKanExtension' := by
+    dsimp [totalRightDerived, totalRightDerivedUnit]
+    infer_instance
+
+end
+
+end Functor
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
@@ -25,10 +25,6 @@ We also introduce typeclasses `HasRightKanExtension L F` and `HasLeftKanExtensio
 which assert the existence of a right or left Kan extension, and chosen Kan extensions
 are obtained as `leftKanExtension L F` and `rightKanExtension L F`.
 
-## TODO (@joelriou)
-
-* define left/right derived functors as particular cases of Kan extensions
-
 ## References
 * https://ncatlab.org/nlab/show/Kan+extension
 
