Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(CategoryTheory): right derived functors #12788

Closed
wants to merge 11 commits into from
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1281,6 +1281,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.)
joelriou marked this conversation as resolved.
Show resolved Hide resolved

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
Loading