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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) : CategoryTheory.Functor C D

The right derived functors of an additive functor.

@[simp]

theorem CategoryTheory.Functor.rightDerivedObjIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) {X : C} (P : CategoryTheory.InjectiveResolution X) : (CategoryTheory.Functor.rightDerivedObjIso F n P).inv = (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map (CategoryTheory.InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (CategoryTheory.InjectiveResolution X))) P).inv))

@[simp]

theorem CategoryTheory.Functor.rightDerivedObjIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) {X : C} (P : CategoryTheory.InjectiveResolution X) : (CategoryTheory.Functor.rightDerivedObjIso F n P).hom = (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map (CategoryTheory.InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (CategoryTheory.InjectiveResolution X))) P).hom))

def CategoryTheory.Functor.rightDerivedObjIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) {X : C} (P : CategoryTheory.InjectiveResolution X) : (CategoryTheory.Functor.rightDerived F n).obj X ≅ (homologyFunctor D (ComplexShape.up ℕ) n).obj ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)

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

@[simp]

theorem CategoryTheory.Functor.rightDerivedObjInjectiveZero_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (X : C) [CategoryTheory.Injective X] : (CategoryTheory.Functor.rightDerivedObjInjectiveZero F X).hom = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map (CategoryTheory.InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (CategoryTheory.InjectiveResolution X))) (CategoryTheory.InjectiveResolution.self X)).hom))) (CategoryTheory.CategoryStruct.comp (homology.map (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) 0) (HomologicalComplex.dFrom ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) 0) = 0) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CochainComplex.single₀ D).obj (F.obj X)) 0) (HomologicalComplex.dFrom ((CochainComplex.single₀ D).obj (F.obj X)) 0) = 0) (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).hom.app X) 0) (HomologicalComplex.Hom.sqFrom ((CochainComplex.single₀MapHomologicalComplex F).hom.app X) 0) (_ : (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).hom.app X) 0).right = (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).hom.app X) 0).right)) ((CochainComplex.homologyFunctor0Single₀ D).hom.app (F.obj X)))

@[simp]

theorem CategoryTheory.Functor.rightDerivedObjInjectiveZero_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (X : C) [CategoryTheory.Injective X] : (CategoryTheory.Functor.rightDerivedObjInjectiveZero F X).inv = CategoryTheory.CategoryStruct.comp ((CochainComplex.homologyFunctor0Single₀ D).inv.app (F.obj X)) (CategoryTheory.CategoryStruct.comp (homology.map (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CochainComplex.single₀ D).obj (F.obj X)) 0) (HomologicalComplex.dFrom ((CochainComplex.single₀ D).obj (F.obj X)) 0) = 0) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) 0) (HomologicalComplex.dFrom ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) 0) = 0) (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) 0) (HomologicalComplex.Hom.sqFrom ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) 0) (_ : (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) 0).right = (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) 0).right)) ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map (CategoryTheory.InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (CategoryTheory.InjectiveResolution X))) (CategoryTheory.InjectiveResolution.self X)).inv))))

def CategoryTheory.Functor.rightDerivedObjInjectiveZero {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (X : C) [CategoryTheory.Injective X] : (CategoryTheory.Functor.rightDerived F 0).obj X ≅ F.obj X

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

@[simp]

theorem CategoryTheory.Functor.rightDerivedObjInjectiveSucc_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) (X : C) [CategoryTheory.Injective X] : (CategoryTheory.Functor.rightDerivedObjInjectiveSucc F n X).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsZero.isoZero (_ : CategoryTheory.Limits.IsZero (0.obj (F.obj X)))).inv (CategoryTheory.CategoryStruct.comp ((CochainComplex.homologyFunctorSuccSingle₀ D n).inv.app (F.obj X)) (CategoryTheory.CategoryStruct.comp (homology.map (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CochainComplex.single₀ D).obj (F.obj X)) (n + 1)) (HomologicalComplex.dFrom ((CochainComplex.single₀ D).obj (F.obj X)) (n + 1)) = 0) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) (n + 1)) (HomologicalComplex.dFrom ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj (CategoryTheory.InjectiveResolution.self X).cocomplex) (n + 1)) = 0) (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) (n + 1)) (HomologicalComplex.Hom.sqFrom ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) (n + 1)) (_ : (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) (n + 1)).right = (HomologicalComplex.Hom.sqTo ((CochainComplex.single₀MapHomologicalComplex F).inv.app X) (n + 1)).right)) ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) (n + 1)).map ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map (CategoryTheory.InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (CategoryTheory.InjectiveResolution X))) (CategoryTheory.InjectiveResolution.self X)).inv)))))

def CategoryTheory.Functor.rightDerivedObjInjectiveSucc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) (X : C) [CategoryTheory.Injective X] : (CategoryTheory.Functor.rightDerived F (n + 1)).obj X ≅ 0

The higher derived functors vanish on injective objects.

theorem CategoryTheory.Functor.rightDerived_map_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) {X : C} {Y : C} (f : Y ⟶ X) {P : CategoryTheory.InjectiveResolution X} {Q : CategoryTheory.InjectiveResolution Y} (g : Q.cocomplex ⟶ P.cocomplex) (w : CategoryTheory.CategoryStruct.comp Q.ι g = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) P.ι) : (CategoryTheory.Functor.rightDerived F n).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.rightDerivedObjIso F n Q).hom (CategoryTheory.CategoryStruct.comp ((homologyFunctor D (ComplexShape.up ℕ) n).map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map g)) (CategoryTheory.Functor.rightDerivedObjIso F n P).inv)

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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] (α : F ⟶ G) (n : ℕ) (X : C) : (CategoryTheory.NatTrans.rightDerived α n).app X = (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((CategoryTheory.injectiveResolutions C).obj X).as))

def CategoryTheory.NatTrans.rightDerived {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] (α : F ⟶ G) (n : ℕ) : CategoryTheory.Functor.rightDerived F n ⟶ CategoryTheory.Functor.rightDerived G n

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

@[simp]

theorem CategoryTheory.NatTrans.rightDerived_id {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) : CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.id F) n = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.rightDerived F n)

@[simp]

theorem CategoryTheory.NatTrans.rightDerived_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] [CategoryTheory.Functor.Additive H] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) : CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.comp α β) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived α n) (CategoryTheory.NatTrans.rightDerived β n)

theorem CategoryTheory.NatTrans.rightDerived_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] (α : F ⟶ G) (n : ℕ) {X : C} (P : CategoryTheory.InjectiveResolution X) : (CategoryTheory.NatTrans.rightDerived α n).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.rightDerivedObjIso F n P).hom (CategoryTheory.CategoryStruct.comp ((homologyFunctor D (ComplexShape.up ℕ) n).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) (CategoryTheory.Functor.rightDerivedObjIso G n P).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} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Mono f] (ex : CategoryTheory.Exact f g) : 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.

theorem CategoryTheory.Abelian.Functor.exact_of_map_injectiveResolution {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) {X : C} [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] (P : CategoryTheory.InjectiveResolution X) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Exact (F.map (HomologicalComplex.Hom.f P.ι 0)) (HomologicalComplex.dFrom ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)

def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfApp {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughInjectives C] [CategoryTheory.Limits.PreservesFiniteLimits F] {X : C} (P : CategoryTheory.InjectiveResolution X) : (CategoryTheory.Functor.rightDerived F 0).obj X ⟶ F.obj X

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

def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppInv {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughInjectives C] {X : C} (P : CategoryTheory.InjectiveResolution X) : F.obj X ⟶ (CategoryTheory.Functor.rightDerived F 0).obj X

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

theorem CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfApp_comp_inv {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughInjectives C] [CategoryTheory.Limits.PreservesFiniteLimits F] {X : C} (P : CategoryTheory.InjectiveResolution X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfApp F P) (CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppInv F P) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.rightDerived F 0).obj X)

theorem CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppInv_comp {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughInjectives C] [CategoryTheory.Limits.PreservesFiniteLimits F] {X : C} (P : CategoryTheory.InjectiveResolution X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppInv F P) (CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfApp F P) = CategoryTheory.CategoryStruct.id (F.obj X)

def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppIso {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughInjectives C] [CategoryTheory.Limits.PreservesFiniteLimits F] {X : C} (P : CategoryTheory.InjectiveResolution X) : (CategoryTheory.Functor.rightDerived F 0).obj X ≅ F.obj X

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

theorem CategoryTheory.Abelian.Functor.rightDerivedZeroToSelf_natural {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughInjectives C] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.InjectiveResolution X) (Q : CategoryTheory.InjectiveResolution Y) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppInv F Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppInv F P) ((CategoryTheory.Functor.rightDerived F 0).map f)

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

def CategoryTheory.Abelian.Functor.rightDerivedZeroIsoSelf {C : Type u} [CategoryTheory.Category.{w, u} C] {D : Type u} [CategoryTheory.Category.{w, u} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.Functor.Additive F] [CategoryTheory.EnoughInjectives C] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Functor.rightDerived F 0 ≅ F

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