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.

We first define a functor F.rightDerivedToHomotopyCategory : C ⥤ HomotopyCategory D (ComplexShape.up ℕ) which is injectiveResolutions C ⋙ F.mapHomotopyCategory _. We show that if X : C and I : InjectiveResolution X, then F.rightDerivedToHomotopyCategory.obj X identifies to the image in the homotopy category of the functor F applied objectwise to I.cocomplex (this isomorphism is I.isoRightDerivedToHomotopyCategoryObj F).

Then, the right-derived functors F.rightDerived n : C ⥤ D are obtained by composing F.rightDerivedToHomotopyCategory with the homology functors on the homotopy category.

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

• Functor.isZero_rightDerived_obj_injective_succ: injective objects have no higher right derived functor.
• NatTrans.rightDerived: the natural isomorphism between right derived functors induced by natural transformation.
• 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.

noncomputable def CategoryTheory.Functor.rightDerivedToHomotopyCategory {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] : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.up ℕ))

When F : C ⥤ D is an additive functor, this is the functor C ⥤ HomotopyCategory D (ComplexShape.up ℕ) which sends X : C to F applied to an injective resolution of X.

Equations

• CategoryTheory.Functor.rightDerivedToHomotopyCategory F = CategoryTheory.Functor.comp (CategoryTheory.injectiveResolutions C) (CategoryTheory.Functor.mapHomotopyCategory F (ComplexShape.up ℕ))

noncomputable def CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj {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] {X : C} (I : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : (CategoryTheory.Functor.rightDerivedToHomotopyCategory F).toPrefunctor.obj X ≅ (CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)) (HomotopyCategory.quotient D (ComplexShape.up ℕ))).toPrefunctor.obj I.cocomplex

If I : InjectiveResolution Z and F : C ⥤ D is an additive functor, this is an isomorphism between F.rightDerivedToHomotopyCategory.obj X and the complex obtained by applying F to I.cocomplex.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc {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] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {Z : HomotopyCategory D (ComplexShape.up ℕ)} (h : (HomotopyCategory.quotient D (ComplexShape.up ℕ)).toPrefunctor.obj ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.obj J.cocomplex) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.rightDerivedToHomotopyCategory F).toPrefunctor.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj J F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj I F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).toPrefunctor.map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.map φ)) h)

theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality {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] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.rightDerivedToHomotopyCategory F).toPrefunctor.map f) (CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj J F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj I F).hom ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)) (HomotopyCategory.quotient D (ComplexShape.up ℕ))).toPrefunctor.map φ)

theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc {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] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {Z : HomotopyCategory D (ComplexShape.up ℕ)} (h : (CategoryTheory.Functor.rightDerivedToHomotopyCategory F).toPrefunctor.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj I F).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.rightDerivedToHomotopyCategory F).toPrefunctor.map f) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).toPrefunctor.map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.map φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj J F).inv h)

theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality {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] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj I F).inv ((CategoryTheory.Functor.rightDerivedToHomotopyCategory F).toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)) (HomotopyCategory.quotient D (ComplexShape.up ℕ))).toPrefunctor.map φ) (CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj J F).inv

noncomputable 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.

Equations

• CategoryTheory.Functor.rightDerived F n = CategoryTheory.Functor.comp (CategoryTheory.Functor.rightDerivedToHomotopyCategory F) (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)

noncomputable def CategoryTheory.InjectiveResolution.isoRightDerivedObj {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] {X : C} (I : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) : (CategoryTheory.Functor.rightDerived F n).toPrefunctor.obj X ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).toPrefunctor.obj ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.obj I.cocomplex)

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality_assoc {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] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) {Z : D} (h : (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).toPrefunctor.obj ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.obj J.cocomplex) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.rightDerived F n).toPrefunctor.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedObj J F n).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedObj I F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).toPrefunctor.map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.map φ)) h)

theorem CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality {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] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.rightDerived F n).toPrefunctor.map f) (CategoryTheory.InjectiveResolution.isoRightDerivedObj J F n).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedObj I F n).hom ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).toPrefunctor.map φ)

theorem CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality_assoc {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] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) {Z : D} (h : (CategoryTheory.Functor.rightDerived F n).toPrefunctor.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedObj I F n).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.rightDerived F n).toPrefunctor.map f) h) = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).toPrefunctor.map ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.map φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedObj J F n).inv h)

theorem CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality {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] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedObj I F n).inv ((CategoryTheory.Functor.rightDerived F n).toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).toPrefunctor.map φ) (CategoryTheory.InjectiveResolution.isoRightDerivedObj J F n).inv

theorem CategoryTheory.Functor.isZero_rightDerived_obj_injective_succ {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.Limits.IsZero ((CategoryTheory.Functor.rightDerived F (n + 1)).toPrefunctor.obj X)

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 : X ⟶ Y) {P : CategoryTheory.InjectiveResolution X} {Q : CategoryTheory.InjectiveResolution Y} (g : P.cocomplex ⟶ Q.cocomplex) (w : CategoryTheory.CategoryStruct.comp P.ι g = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).toPrefunctor.map f) Q.ι) : (CategoryTheory.Functor.rightDerived F n).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedObj P F n).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).toPrefunctor.map g) (CategoryTheory.InjectiveResolution.isoRightDerivedObj Q F n).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.

noncomputable def CategoryTheory.NatTrans.rightDerivedToHomotopyCategory {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) : CategoryTheory.Functor.rightDerivedToHomotopyCategory F ⟶ CategoryTheory.Functor.rightDerivedToHomotopyCategory G

The natural transformation F.rightDerivedToHomotopyCategory ⟶ G.rightDerivedToHomotopyCategory induced by a natural transformation F ⟶ G between additive functors.

Equations

• CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α = CategoryTheory.whiskerLeft (CategoryTheory.injectiveResolutions C) (CategoryTheory.NatTrans.mapHomotopyCategory α (ComplexShape.up ℕ))

theorem CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_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) {X : C} (P : CategoryTheory.InjectiveResolution X) : (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj P F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).toPrefunctor.map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) (CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj P G).inv)

@[simp]

theorem CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_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] : CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.rightDerivedToHomotopyCategory F)

theorem CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc {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} (α : F ⟶ G) (β : G ⟶ H) [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] [CategoryTheory.Functor.Additive H] {Z : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.up ℕ))} (h : CategoryTheory.Functor.rightDerivedToHomotopyCategory H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory β) h)

@[simp]

theorem CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_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} (α : F ⟶ G) (β : G ⟶ H) [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] [CategoryTheory.Functor.Additive H] : CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α) (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory β)

noncomputable 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.

Equations

• CategoryTheory.NatTrans.rightDerived α n = CategoryTheory.whiskerRight (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α) (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)

@[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)

theorem CategoryTheory.NatTrans.rightDerived_comp_assoc {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 : ℕ) {Z : CategoryTheory.Functor C D} (h : CategoryTheory.Functor.rightDerived H n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.comp α β) n) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived α n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived β n) h)

@[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.InjectiveResolution.rightDerived_app_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) {X : C} (P : CategoryTheory.InjectiveResolution X) (n : ℕ) : (CategoryTheory.NatTrans.rightDerived α n).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.isoRightDerivedObj P F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).toPrefunctor.map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) (CategoryTheory.InjectiveResolution.isoRightDerivedObj P G n).inv)

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

noncomputable def CategoryTheory.InjectiveResolution.toRightDerivedZero' {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : F.toPrefunctor.obj X ⟶ HomologicalComplex.cycles ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.obj P.cocomplex) 0

If P : InjectiveResolution X and F is an additive functor, this is the canonical morphism from F.obj X to the cycles in degree 0 of (F.mapHomologicalComplex _).obj P.cocomplex.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {Z : D} (h : ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.obj P.cocomplex).X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.toRightDerivedZero' P F) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.obj P.cocomplex) 0) h) = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (P.ι.f 0)) h

@[simp]

theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.toRightDerivedZero' P F) (HomologicalComplex.iCycles ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.obj P.cocomplex) 0) = F.toPrefunctor.map (P.ι.f 0)

theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.InjectiveResolution X) (Q : CategoryTheory.InjectiveResolution Y) (φ : P.cocomplex ⟶ Q.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (P.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (Q.ι.f 0)) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {Z : D} (h : HomologicalComplex.cycles ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.obj Q.cocomplex) 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.toRightDerivedZero' Q F) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.toRightDerivedZero' P F) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.map φ) 0) h)

theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.InjectiveResolution X) (Q : CategoryTheory.InjectiveResolution Y) (φ : P.cocomplex ⟶ Q.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (P.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (Q.ι.f 0)) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (CategoryTheory.InjectiveResolution.toRightDerivedZero' Q F) = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.toRightDerivedZero' P F) (HomologicalComplex.cyclesMap ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.map φ) 0)

instance CategoryTheory.InjectiveResolution.instIsIsoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorCyclesPreadditiveHasZeroMorphismsToPreadditiveNatUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringObjHomologicalComplexPreadditiveHasZeroMorphismsToPreadditiveToQuiverToCategoryStructInstCategoryHomologicalComplexHomologicalComplexToQuiverToCategoryStructInstCategoryHomologicalComplexToPrefunctorMapHomologicalComplexCocomplexHasZeroObjectSelfOfNatInstOfNatNatHasHomologyCategoryWithHomology_of_abelianScToRightDerivedZero' {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (X : C) [CategoryTheory.Injective X] : CategoryTheory.IsIso (CategoryTheory.InjectiveResolution.toRightDerivedZero' (CategoryTheory.InjectiveResolution.self X) F)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.toRightDerivedZero {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] : F ⟶ CategoryTheory.Functor.rightDerived F 0

The natural transformation F ⟶ F.rightDerived 0.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.InjectiveResolution.toRightDerivedZero_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] {X : C} (I : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : (CategoryTheory.Functor.toRightDerivedZero F).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.toRightDerivedZero' I F) (CategoryTheory.CategoryStruct.comp (CochainComplex.isoHomologyπ₀ ((CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).toPrefunctor.obj I.cocomplex)).hom (CategoryTheory.InjectiveResolution.isoRightDerivedObj I F 0).inv)

instance CategoryTheory.instIsIsoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorRightDerivedOfNatNatInstOfNatNatAppToRightDerivedZero {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.IsIso ((CategoryTheory.Functor.toRightDerivedZero F).app X)

Equations

• (_ : CategoryTheory.IsIso ((CategoryTheory.Functor.toRightDerivedZero F).app X)) = (_ : CategoryTheory.IsIso ((CategoryTheory.Functor.toRightDerivedZero F).app X))

instance CategoryTheory.instIsIsoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorCyclesPreadditiveHasZeroMorphismsToPreadditiveNatUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringObjHomologicalComplexPreadditiveHasZeroMorphismsToPreadditiveToQuiverToCategoryStructInstCategoryHomologicalComplexHomologicalComplexToQuiverToCategoryStructInstCategoryHomologicalComplexToPrefunctorMapHomologicalComplexCocomplexHasZeroObjectOfNatInstOfNatNatHasHomologyCategoryWithHomology_of_abelianScToRightDerivedZero' {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteLimits F] {X : C} (P : CategoryTheory.InjectiveResolution X) : CategoryTheory.IsIso (CategoryTheory.InjectiveResolution.toRightDerivedZero' P F)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.InjectiveResolution.toRightDerivedZero' P F)) = (_ : CategoryTheory.IsIso (CategoryTheory.InjectiveResolution.toRightDerivedZero' P F))

instance CategoryTheory.instIsIsoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorRightDerivedOfNatNatInstOfNatNatAppToRightDerivedZero_1 {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] [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) : CategoryTheory.IsIso ((CategoryTheory.Functor.toRightDerivedZero F).app X)

Equations

• (_ : CategoryTheory.IsIso ((CategoryTheory.Functor.toRightDerivedZero F).app X)) = (_ : CategoryTheory.IsIso ((CategoryTheory.Functor.toRightDerivedZero F).app X))

instance CategoryTheory.instIsIsoFunctorCategoryRightDerivedOfNatNatInstOfNatNatToRightDerivedZero {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] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.IsIso (CategoryTheory.Functor.toRightDerivedZero F)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.Functor.toRightDerivedZero F)) = (_ : CategoryTheory.IsIso (CategoryTheory.Functor.toRightDerivedZero F))

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_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] [CategoryTheory.Limits.PreservesFiniteLimits F] : (CategoryTheory.Functor.rightDerivedZeroIsoSelf F).inv = CategoryTheory.Functor.toRightDerivedZero F

noncomputable def CategoryTheory.Functor.rightDerivedZeroIsoSelf {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] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Functor.rightDerived F 0 ≅ F

The canonical isomorphism F.rightDerived 0 ≅ F when F is left exact (i.e. preserves finite limits).

Equations

• CategoryTheory.Functor.rightDerivedZeroIsoSelf F = (CategoryTheory.asIso (CategoryTheory.Functor.toRightDerivedZero F)).symm

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_assoc {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] [CategoryTheory.Limits.PreservesFiniteLimits F] {Z : CategoryTheory.Functor C D} (h : CategoryTheory.Functor.rightDerived F 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.rightDerivedZeroIsoSelf F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.toRightDerivedZero F) h) = h

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_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] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.rightDerivedZeroIsoSelf F).hom (CategoryTheory.Functor.toRightDerivedZero F) = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.rightDerived F 0)

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_assoc {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] [CategoryTheory.Limits.PreservesFiniteLimits F] {Z : CategoryTheory.Functor C D} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.toRightDerivedZero F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.rightDerivedZeroIsoSelf F).hom h) = h

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_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] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.toRightDerivedZero F) (CategoryTheory.Functor.rightDerivedZeroIsoSelf F).hom = CategoryTheory.CategoryStruct.id F

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_app_assoc {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] [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) {Z : D} (h : (CategoryTheory.Functor.rightDerived F 0).toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.rightDerivedZeroIsoSelf F).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.toRightDerivedZero F).app X) h) = h

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_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) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.rightDerivedZeroIsoSelf F).hom.app X) ((CategoryTheory.Functor.toRightDerivedZero F).app X) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.rightDerived F 0).toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_app_assoc {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] [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) {Z : D} (h : F.toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.toRightDerivedZero F).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.rightDerivedZeroIsoSelf F).hom.app X) h) = h

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_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) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.toRightDerivedZero F).app X) ((CategoryTheory.Functor.rightDerivedZeroIsoSelf F).hom.app X) = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)