# Documentation

Mathlib.CategoryTheory.Abelian.RightDerived

# Right-derived functors #

We define the right-derived functors F.rightDerived n : C ⥤ D for any additive functor F out of a category with injective resolutions.

The definition is

injectiveResolutions C ⋙ F.mapHomotopyCategory _ ⋙ HomotopyCategory.homologyFunctor D _ n


that is, we pick an injective resolution (thought of as an object of the homotopy category), we apply F objectwise, and compute n-th homology.

We show that these right-derived functors can be calculated on objects using any choice of injective resolution, and on morphisms by any choice of lift to a cochain map between chosen injective resolutions.

Similarly we define natural transformations between right-derived functors coming from natural transformations between the original additive functors, and show how to compute the components.

## Main results #

• CategoryTheory.Functor.rightDerivedObj_injective_zero: the 0-th derived functor of F on an injective object X is isomorphic to F.obj X.
• CategoryTheory.Functor.rightDerivedObj_injective_succ: injective objects have no higher right derived functor.
• CategoryTheory.NatTrans.rightDerived: the natural isomorphism between right derived functors induced by natural transformation.

Now, we assume PreservesFiniteLimits F, then

• CategoryTheory.Abelian.Functor.preserves_exact_of_preservesFiniteLimits_of_mono: if f is mono and Exact f g, then Exact (F.map f) (F.map g).
• CategoryTheory.Abelian.Functor.rightDerivedZeroIsoSelf: if there are enough injectives, then there is a natural isomorphism (F.rightDerived 0) ≅ F.
def CategoryTheory.Functor.rightDerived {C : Type u} {D : Type u_1} [] (F : ) (n : ) :

The right derived functors of an additive functor.

Instances For
@[simp]
theorem CategoryTheory.Functor.rightDerivedObjIso_inv {C : Type u} {D : Type u_1} [] (F : ) (n : ) {X : C} :
().inv = ().map (().map (().map ().inv))
@[simp]
theorem CategoryTheory.Functor.rightDerivedObjIso_hom {C : Type u} {D : Type u_1} [] (F : ) (n : ) {X : C} :
().hom = ().map (().map (().map ().hom))
def CategoryTheory.Functor.rightDerivedObjIso {C : Type u} {D : Type u_1} [] (F : ) (n : ) {X : C} :
().obj X ().obj (().obj P.cocomplex)

We can compute a right derived functor using a chosen injective resolution.

Instances For
@[simp]
theorem CategoryTheory.Functor.rightDerivedObjInjectiveZero_hom {C : Type u} {D : Type u_1} [] (F : ) (X : C) :
= CategoryTheory.CategoryStruct.comp (().map (().map (().map ().hom))) (CategoryTheory.CategoryStruct.comp (homology.map (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo (().obj ().cocomplex) 0) (HomologicalComplex.dFrom (().obj ().cocomplex) 0) = 0) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo (().obj (F.obj X)) 0) (HomologicalComplex.dFrom (().obj (F.obj X)) 0) = 0) () () (_ : ().right = ().right)) (.app (F.obj X)))
@[simp]
theorem CategoryTheory.Functor.rightDerivedObjInjectiveZero_inv {C : Type u} {D : Type u_1} [] (F : ) (X : C) :
= CategoryTheory.CategoryStruct.comp (.app (F.obj X)) (CategoryTheory.CategoryStruct.comp (homology.map (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo (().obj (F.obj X)) 0) (HomologicalComplex.dFrom (().obj (F.obj X)) 0) = 0) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo (().obj ().cocomplex) 0) (HomologicalComplex.dFrom (().obj ().cocomplex) 0) = 0) () () (_ : ().right = ().right)) (().map (().map (().map ().inv))))
def CategoryTheory.Functor.rightDerivedObjInjectiveZero {C : Type u} {D : Type u_1} [] (F : ) (X : C) :
().obj X F.obj X

The 0-th derived functor of F on an injective object X is just F.obj X.

Instances For
@[simp]
theorem CategoryTheory.Functor.rightDerivedObjInjectiveSucc_inv {C : Type u} {D : Type u_1} [] (F : ) (n : ) (X : C) :
def CategoryTheory.Functor.rightDerivedObjInjectiveSucc {C : Type u} {D : Type u_1} [] (F : ) (n : ) (X : C) :
().obj X 0

The higher derived functors vanish on injective objects.

Instances For
theorem CategoryTheory.Functor.rightDerived_map_eq {C : Type u} {D : Type u_1} [] (F : ) (n : ) {X : C} {Y : C} (f : Y X) (g : Q.cocomplex P.cocomplex) (w : = CategoryTheory.CategoryStruct.comp (().map f) P) :

We can compute a right derived functor on a morphism using a descent of that morphism to a cochain map between chosen injective resolutions.

@[simp]
theorem CategoryTheory.NatTrans.rightDerived_app {C : Type u} {D : Type u_1} [] {F : } {G : } (α : F G) (n : ) (X : C) :
().app X = ().map (().map (().app (().obj X).as))
def CategoryTheory.NatTrans.rightDerived {C : Type u} {D : Type u_1} [] {F : } {G : } (α : F G) (n : ) :

The natural transformation between right-derived functors induced by a natural transformation.

Instances For
@[simp]
@[simp]
theorem CategoryTheory.NatTrans.rightDerived_comp {C : Type u} {D : Type u_1} [] {F : } {G : } {H : } (α : F G) (β : G H) (n : ) :
theorem CategoryTheory.NatTrans.rightDerived_eq {C : Type u} {D : Type u_1} [] {F : } {G : } (α : F G) (n : ) {X : C} :
().app X = CategoryTheory.CategoryStruct.comp ().hom (CategoryTheory.CategoryStruct.comp (().map (().app P.cocomplex)) ().inv)

A component of the natural transformation between right-derived functors can be computed using a chosen injective resolution.

theorem CategoryTheory.Abelian.Functor.preserves_exact_of_preservesFiniteLimits_of_mono {C : Type u} {D : Type u} (F : ) {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} (ex : ) :
CategoryTheory.Exact (F.map f) (F.map g)

If PreservesFiniteLimits F and Mono f, then Exact (F.map f) (F.map g) if Exact f g.

def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfApp {C : Type u} {D : Type u} (F : ) {X : C} :
().obj X F.obj X

Given P : InjectiveResolution X, a morphism (F.rightDerived 0).obj X ⟶ F.obj X given PreservesFiniteLimits F.

Instances For
def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppInv {C : Type u} {D : Type u} (F : ) {X : C} :
F.obj X ().obj X

Given P : InjectiveResolution X, a morphism F.obj X ⟶ (F.rightDerived 0).obj X.

Instances For
def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppIso {C : Type u} {D : Type u} (F : ) {X : C} :
().obj X F.obj X

Given P : InjectiveResolution X, the isomorphism (F.rightDerived 0).obj X ≅ F.obj X if PreservesFiniteLimits F.

Instances For
theorem CategoryTheory.Abelian.Functor.rightDerivedZeroToSelf_natural {C : Type u} {D : Type u} (F : ) {X : C} {Y : C} (f : X Y) :

Given P : InjectiveResolution X and Q : InjectiveResolution Y and a morphism f : X ⟶ Y, naturality of the square given by rightDerivedZeroToSelf_natural.

Given PreservesFiniteLimits F, the natural isomorphism (F.rightDerived 0) ≅ F.

Instances For