Skip to content

Commit

Permalink
feat(CategoryTheory): right derived functors (#12788)
Browse files Browse the repository at this point in the history
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 <[email protected]>
  • Loading branch information
2 people authored and grunweg committed Jun 7, 2024
1 parent c81bb7a commit 7bd8cf3
Show file tree
Hide file tree
Showing 5 changed files with 233 additions and 4 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 10 additions & 0 deletions Mathlib/CategoryTheory/Abelian/LeftDerived.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 10 additions & 0 deletions Mathlib/CategoryTheory/Abelian/RightDerived.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
212 changes: 212 additions & 0 deletions Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
Original file line number Diff line number Diff line change
@@ -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
4 changes: 0 additions & 4 deletions Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 7bd8cf3

Please sign in to comment.