From 7bd8cf3b29e7981df34669173376eff2c8ebd4b0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 5 Jun 2024 12:48:17 +0000 Subject: [PATCH] feat(CategoryTheory): right derived functors (#12788) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 <37772949+joelriou@users.noreply.github.com> --- Mathlib.lean | 1 + .../CategoryTheory/Abelian/LeftDerived.lean | 10 + .../CategoryTheory/Abelian/RightDerived.lean | 10 + .../Functor/Derived/RightDerived.lean | 212 ++++++++++++++++++ .../Functor/KanExtension/Basic.lean | 4 - 5 files changed, 233 insertions(+), 4 deletions(-) create mode 100644 Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean diff --git a/Mathlib.lean b/Mathlib.lean index b59a3fcca8eb18..b8c8dfe0115e8d 100644 --- 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 index 6db19d0499d68c..05c1296eb71e66 100644 --- 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 index 3c90f4e76929c8..2453494b9665b1 100644 --- 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 new file mode 100644 index 00000000000000..b91985f18fa9b2 --- /dev/null +++ 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 index fce847ee26cf2a..4e26c9a1ab9609 100644 --- 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