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(andFunctor.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}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
:
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 α
Instances
theorem
CategoryTheory.Functor.IsRightDerivedFunctor.isLeftKanExtension'
{C : Type u_1}
{D : Type u_2}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
{RF : CategoryTheory.Functor D H}
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
{α : F ⟶ L.comp RF}
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[self : RF.IsRightDerivedFunctor α W]
:
RF.IsLeftKanExtension α
theorem
CategoryTheory.Functor.IsRightDerivedFunctor.isLeftKanExtension
{C : Type u_1}
{D : Type u_2}
{H : Type u_5}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Category.{u_6, u_5} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
:
RF.IsLeftKanExtension α
theorem
CategoryTheory.Functor.isRightDerivedFunctor_iff_isLeftKanExtension
{C : Type u_1}
{D : Type u_2}
{H : Type u_5}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Category.{u_6, u_5} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(W : CategoryTheory.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}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_6} D]
[CategoryTheory.Category.{u_2, u_3} H]
{RF : CategoryTheory.Functor D H}
{RF' : CategoryTheory.Functor D H}
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α' : F ⟶ L.comp RF')
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
(e : RF ≅ RF')
(comm : CategoryTheory.CategoryStruct.comp α (CategoryTheory.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}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
(G : CategoryTheory.Functor D H)
(β : F ⟶ L.comp G)
:
RF ⟶ G
Constructor for natural transformations from a right derived functor.
Equations
- RF.rightDerivedDesc α W G β = let_fun this := ⋯; RF.descOfIsLeftKanExtension α G β
Instances For
@[simp]
theorem
CategoryTheory.Functor.rightDerived_fac_assoc
{C : Type u_5}
{D : Type u_3}
{H : Type u_4}
[CategoryTheory.Category.{u_6, u_5} C]
[CategoryTheory.Category.{u_1, u_3} D]
[CategoryTheory.Category.{u_2, u_4} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
(G : CategoryTheory.Functor D H)
(β : F ⟶ L.comp G)
{Z : CategoryTheory.Functor C H}
(h : L.comp G ⟶ Z)
:
CategoryTheory.CategoryStruct.comp α
(CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L (RF.rightDerivedDesc α W G β)) h) = CategoryTheory.CategoryStruct.comp β h
@[simp]
theorem
CategoryTheory.Functor.rightDerived_fac
{C : Type u_5}
{D : Type u_3}
{H : Type u_4}
[CategoryTheory.Category.{u_6, u_5} C]
[CategoryTheory.Category.{u_1, u_3} D]
[CategoryTheory.Category.{u_2, u_4} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
(G : CategoryTheory.Functor D H)
(β : F ⟶ L.comp G)
:
CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L (RF.rightDerivedDesc α W G β)) = β
@[simp]
theorem
CategoryTheory.Functor.rightDerived_fac_app_assoc
{C : Type u_5}
{D : Type u_3}
{H : Type u_4}
[CategoryTheory.Category.{u_6, u_5} C]
[CategoryTheory.Category.{u_1, u_3} D]
[CategoryTheory.Category.{u_2, u_4} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
(G : CategoryTheory.Functor D H)
(β : F ⟶ L.comp G)
(X : C)
{Z : H}
(h : G.obj (L.obj X) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (α.app X)
(CategoryTheory.CategoryStruct.comp ((RF.rightDerivedDesc α W G β).app (L.obj X)) h) = CategoryTheory.CategoryStruct.comp (β.app X) h
@[simp]
theorem
CategoryTheory.Functor.rightDerived_fac_app
{C : Type u_5}
{D : Type u_3}
{H : Type u_4}
[CategoryTheory.Category.{u_6, u_5} C]
[CategoryTheory.Category.{u_1, u_3} D]
[CategoryTheory.Category.{u_2, u_4} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
(G : CategoryTheory.Functor D H)
(β : F ⟶ L.comp G)
(X : C)
:
CategoryTheory.CategoryStruct.comp (α.app X) ((RF.rightDerivedDesc α W G β).app (L.obj X)) = β.app X
theorem
CategoryTheory.Functor.rightDerived_ext
{C : Type u_5}
{D : Type u_3}
{H : Type u_4}
[CategoryTheory.Category.{u_6, u_5} C]
[CategoryTheory.Category.{u_1, u_3} D]
[CategoryTheory.Category.{u_2, u_4} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
(G : CategoryTheory.Functor D H)
(γ₁ : RF ⟶ G)
(γ₂ : RF ⟶ G)
(hγ : CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L γ₁) = CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L γ₂))
:
γ₁ = γ₂
noncomputable def
CategoryTheory.Functor.rightDerivedNatTrans
{C : Type u_1}
{D : Type u_2}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
(RF : CategoryTheory.Functor D H)
(RF' : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{F' : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α' : F' ⟶ L.comp RF')
(W : CategoryTheory.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 τ α')
Instances For
@[simp]
theorem
CategoryTheory.Functor.rightDerivedNatTrans_fac_assoc
{C : Type u_1}
{D : Type u_6}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_6} D]
[CategoryTheory.Category.{u_2, u_3} H]
(RF : CategoryTheory.Functor D H)
(RF' : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{F' : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α' : F' ⟶ L.comp RF')
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
(τ : F ⟶ F')
{Z : CategoryTheory.Functor C H}
(h : L.comp RF' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp α
(CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L (RF.rightDerivedNatTrans RF' α α' W τ)) h) = CategoryTheory.CategoryStruct.comp τ (CategoryTheory.CategoryStruct.comp α' h)
@[simp]
theorem
CategoryTheory.Functor.rightDerivedNatTrans_fac
{C : Type u_1}
{D : Type u_6}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_6} D]
[CategoryTheory.Category.{u_2, u_3} H]
(RF : CategoryTheory.Functor D H)
(RF' : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{F' : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α' : F' ⟶ L.comp RF')
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
(τ : F ⟶ F')
:
CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L (RF.rightDerivedNatTrans RF' α α' W τ)) = CategoryTheory.CategoryStruct.comp τ α'
@[simp]
theorem
CategoryTheory.Functor.rightDerivedNatTrans_app_assoc
{C : Type u_1}
{D : Type u_6}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_6} D]
[CategoryTheory.Category.{u_2, u_3} H]
(RF : CategoryTheory.Functor D H)
(RF' : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{F' : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α' : F' ⟶ L.comp RF')
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
(τ : F ⟶ F')
(X : C)
{Z : H}
(h : RF'.obj (L.obj X) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (α.app X)
(CategoryTheory.CategoryStruct.comp ((RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X)) h) = CategoryTheory.CategoryStruct.comp (τ.app X) (CategoryTheory.CategoryStruct.comp (α'.app X) h)
@[simp]
theorem
CategoryTheory.Functor.rightDerivedNatTrans_app
{C : Type u_1}
{D : Type u_6}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_6} D]
[CategoryTheory.Category.{u_2, u_3} H]
(RF : CategoryTheory.Functor D H)
(RF' : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{F' : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α' : F' ⟶ L.comp RF')
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
(τ : F ⟶ F')
(X : C)
:
CategoryTheory.CategoryStruct.comp (α.app X) ((RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X)) = CategoryTheory.CategoryStruct.comp (τ.app X) (α'.app X)
@[simp]
theorem
CategoryTheory.Functor.rightDerivedNatTrans_id
{C : Type u_5}
{D : Type u_1}
{H : Type u_3}
[CategoryTheory.Category.{u_6, u_5} C]
[CategoryTheory.Category.{u_4, u_1} D]
[CategoryTheory.Category.{u_2, u_3} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
:
RF.rightDerivedNatTrans RF α α W (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id RF
@[simp]
theorem
CategoryTheory.Functor.rightDerivedNatTrans_comp_assoc
{C : Type u_1}
{D : Type u_5}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_6, u_5} D]
[CategoryTheory.Category.{u_2, u_3} H]
(RF : CategoryTheory.Functor D H)
(RF' : CategoryTheory.Functor D H)
(RF'' : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{F' : CategoryTheory.Functor C H}
{F'' : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α' : F' ⟶ L.comp RF')
(α'' : F'' ⟶ L.comp RF'')
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
[RF'.IsRightDerivedFunctor α' W]
(τ : F ⟶ F')
(τ' : F' ⟶ F'')
{Z : CategoryTheory.Functor D H}
(h : RF'' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (RF.rightDerivedNatTrans RF' α α' W τ)
(CategoryTheory.CategoryStruct.comp (RF'.rightDerivedNatTrans RF'' α' α'' W τ') h) = CategoryTheory.CategoryStruct.comp (RF.rightDerivedNatTrans RF'' α α'' W (CategoryTheory.CategoryStruct.comp τ τ')) h
@[simp]
theorem
CategoryTheory.Functor.rightDerivedNatTrans_comp
{C : Type u_1}
{D : Type u_5}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_6, u_5} D]
[CategoryTheory.Category.{u_2, u_3} H]
(RF : CategoryTheory.Functor D H)
(RF' : CategoryTheory.Functor D H)
(RF'' : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{F' : CategoryTheory.Functor C H}
{F'' : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α' : F' ⟶ L.comp RF')
(α'' : F'' ⟶ L.comp RF'')
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
[RF'.IsRightDerivedFunctor α' W]
(τ : F ⟶ F')
(τ' : F' ⟶ F'')
:
CategoryTheory.CategoryStruct.comp (RF.rightDerivedNatTrans RF' α α' W τ) (RF'.rightDerivedNatTrans RF'' α' α'' W τ') = RF.rightDerivedNatTrans RF'' α α'' W (CategoryTheory.CategoryStruct.comp τ τ')
@[simp]
theorem
CategoryTheory.Functor.rightDerivedNatIso_hom
{C : Type u_1}
{D : Type u_2}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
(RF : CategoryTheory.Functor D H)
(RF' : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{F' : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α' : F' ⟶ L.comp RF')
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
[RF'.IsRightDerivedFunctor α' W]
(τ : F ≅ F')
:
(RF.rightDerivedNatIso RF' α α' W τ).hom = RF.rightDerivedNatTrans RF' α α' W τ.hom
@[simp]
theorem
CategoryTheory.Functor.rightDerivedNatIso_inv
{C : Type u_1}
{D : Type u_2}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
(RF : CategoryTheory.Functor D H)
(RF' : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{F' : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α' : F' ⟶ L.comp RF')
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
[RF'.IsRightDerivedFunctor α' W]
(τ : F ≅ F')
:
(RF.rightDerivedNatIso RF' α α' W τ).inv = RF'.rightDerivedNatTrans RF α' α W τ.inv
noncomputable def
CategoryTheory.Functor.rightDerivedNatIso
{C : Type u_1}
{D : Type u_2}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
(RF : CategoryTheory.Functor D H)
(RF' : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{F' : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α' : F' ⟶ L.comp RF')
(W : CategoryTheory.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 := ⋯ }
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Functor.rightDerivedUnique
{C : Type u_1}
{D : Type u_2}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
(RF : CategoryTheory.Functor D H)
(RF' : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(α'₂ : F ⟶ L.comp RF')
(W : CategoryTheory.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)
Instances For
theorem
CategoryTheory.Functor.isRightDerivedFunctor_iff_isIso_rightDerivedDesc
{C : Type u_5}
{D : Type u_3}
{H : Type u_4}
[CategoryTheory.Category.{u_6, u_5} C]
[CategoryTheory.Category.{u_1, u_3} D]
[CategoryTheory.Category.{u_2, u_4} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[RF.IsRightDerivedFunctor α W]
(G : CategoryTheory.Functor D H)
(β : F ⟶ L.comp G)
:
G.IsRightDerivedFunctor β W ↔ CategoryTheory.IsIso (RF.rightDerivedDesc α W G β)
class
CategoryTheory.Functor.HasRightDerivedFunctor
{C : Type u_1}
{H : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} H]
(F : CategoryTheory.Functor C H)
(W : CategoryTheory.MorphismProperty C)
:
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
Instances
theorem
CategoryTheory.Functor.HasRightDerivedFunctor.hasLeftKanExtension'
{C : Type u_1}
{H : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} H]
{F : CategoryTheory.Functor C H}
{W : CategoryTheory.MorphismProperty C}
[self : F.HasRightDerivedFunctor W]
:
W.Q.HasLeftKanExtension F
theorem
CategoryTheory.Functor.hasRightDerivedFunctor_iff
{C : Type u_1}
{D : Type u_5}
{H : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_6, u_5} D]
[CategoryTheory.Category.{u_4, u_2} H]
(F : CategoryTheory.Functor C H)
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.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}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} H]
{F : CategoryTheory.Functor C H}
{F' : CategoryTheory.Functor C H}
(e : F ≅ F')
(W : CategoryTheory.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}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_6, u_5} D]
[CategoryTheory.Category.{u_4, u_2} H]
(F : CategoryTheory.Functor C H)
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.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}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
(RF : CategoryTheory.Functor D H)
{F : CategoryTheory.Functor C H}
{L : CategoryTheory.Functor C D}
(α : F ⟶ L.comp RF)
{W : CategoryTheory.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}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
{F : CategoryTheory.Functor C H}
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[F.HasRightDerivedFunctor 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.
Equations
- CategoryTheory.Functor.totalRightDerived L W = let_fun this := ⋯; L.leftKanExtension F
Instances For
noncomputable def
CategoryTheory.Functor.totalRightDerivedUnit
{C : Type u_1}
{D : Type u_2}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
{F : CategoryTheory.Functor C H}
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[F.HasRightDerivedFunctor W]
:
F ⟶ L.comp (CategoryTheory.Functor.totalRightDerived L W)
The canonical natural transformation F ⟶ L ⋙ F.totalRightDerived L W.
Equations
- CategoryTheory.Functor.totalRightDerivedUnit L W = let_fun this := ⋯; L.leftKanExtensionUnit F
Instances For
instance
CategoryTheory.Functor.instIsRightDerivedFunctorTotalRightDerivedTotalRightDerivedUnit
{C : Type u_1}
{D : Type u_2}
{H : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, u_3} H]
{F : CategoryTheory.Functor C H}
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[F.HasRightDerivedFunctor W]
:
(CategoryTheory.Functor.totalRightDerived L W).IsRightDerivedFunctor (CategoryTheory.Functor.totalRightDerivedUnit L W)
W
Equations
- ⋯ = ⋯