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.

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.

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

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

noncomputable def CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {X : C} (I : InjectiveResolution X) (F : Functor C D) [F.Additive] : F.rightDerivedToHomotopyCategory.obj X ≅ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).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

• I.isoRightDerivedToHomotopyCategoryObj F = (F.mapHomotopyCategory (ComplexShape.up ℕ)).mapIso I.iso ≪≫ (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).app I.cocomplex

theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) (F : Functor C D) [F.Additive] : CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) (J.isoRightDerivedToHomotopyCategoryObj F).hom = CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).map φ)

theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) (F : Functor C D) [F.Additive] {Z : HomotopyCategory D (ComplexShape.up ℕ)} (h : (HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) ⟶ Z) : CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) (CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj F).hom h) = CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom (CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)) h)

theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) (F : Functor C D) [F.Additive] : CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv (F.rightDerivedToHomotopyCategory.map f) = CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).map φ) (J.isoRightDerivedToHomotopyCategoryObj F).inv

theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) (F : Functor C D) [F.Additive] {Z : HomotopyCategory D (ComplexShape.up ℕ)} (h : F.rightDerivedToHomotopyCategory.obj Y ⟶ Z) : CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv (CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) h) = CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)) (CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj F).inv h)

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

The right derived functors of an additive functor.

Equations

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

noncomputable def CategoryTheory.InjectiveResolution.isoRightDerivedObj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {X : C} (I : InjectiveResolution X) (F : Functor C D) [F.Additive] (n : ℕ) : (F.rightDerived n).obj X ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).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 {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) (F : Functor C D) [F.Additive] (n : ℕ) : CategoryStruct.comp ((F.rightDerived n).map f) (J.isoRightDerivedObj F n).hom = CategoryStruct.comp (I.isoRightDerivedObj F n).hom (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map φ)

theorem CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) (F : Functor C D) [F.Additive] (n : ℕ) {Z : D} (h : (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) ⟶ Z) : CategoryStruct.comp ((F.rightDerived n).map f) (CategoryStruct.comp (J.isoRightDerivedObj F n).hom h) = CategoryStruct.comp (I.isoRightDerivedObj F n).hom (CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)) h)

theorem CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) (F : Functor C D) [F.Additive] (n : ℕ) : CategoryStruct.comp (I.isoRightDerivedObj F n).inv ((F.rightDerived n).map f) = CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map φ) (J.isoRightDerivedObj F n).inv

theorem CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) (F : Functor C D) [F.Additive] (n : ℕ) {Z : D} (h : (F.rightDerived n).obj Y ⟶ Z) : CategoryStruct.comp (I.isoRightDerivedObj F n).inv (CategoryStruct.comp ((F.rightDerived n).map f) h) = CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)) (CategoryStruct.comp (J.isoRightDerivedObj F n).inv h)

theorem CategoryTheory.Functor.isZero_rightDerived_obj_injective_succ {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] (n : ℕ) (X : C) [Injective X] : Limits.IsZero ((F.rightDerived (n + 1)).obj X)

The higher derived functors vanish on injective objects.

theorem CategoryTheory.Functor.rightDerived_map_eq {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] (n : ℕ) {X Y : C} (f : X ⟶ Y) {P : InjectiveResolution X} {Q : InjectiveResolution Y} (g : P.cocomplex ⟶ Q.cocomplex) (w : CategoryStruct.comp P.ι g = CategoryStruct.comp ((CochainComplex.single₀ C).map f) Q.ι) : (F.rightDerived n).map f = CategoryStruct.comp (P.isoRightDerivedObj F n).hom (CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map g) (Q.isoRightDerivedObj 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} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {F G : Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) : F.rightDerivedToHomotopyCategory ⟶ G.rightDerivedToHomotopyCategory

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} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {F G : Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : InjectiveResolution X) : (NatTrans.rightDerivedToHomotopyCategory α).app X = CategoryStruct.comp (P.isoRightDerivedToHomotopyCategoryObj F).hom (CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) (P.isoRightDerivedToHomotopyCategoryObj G).inv)

@[simp]

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

@[simp]

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

theorem CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {F G H : Functor C D} (α : F ⟶ G) (β : G ⟶ H) [F.Additive] [G.Additive] [H.Additive] {Z : Functor C (HomotopyCategory D (ComplexShape.up ℕ))} (h : H.rightDerivedToHomotopyCategory ⟶ Z) : CategoryStruct.comp (rightDerivedToHomotopyCategory (CategoryStruct.comp α β)) h = CategoryStruct.comp (rightDerivedToHomotopyCategory α) (CategoryStruct.comp (rightDerivedToHomotopyCategory β) h)

noncomputable def CategoryTheory.NatTrans.rightDerived {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {F G : Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) (n : ℕ) : F.rightDerived n ⟶ G.rightDerived 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} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] (n : ℕ) : rightDerived (CategoryStruct.id F) n = CategoryStruct.id (F.rightDerived n)

@[simp]

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

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

theorem CategoryTheory.InjectiveResolution.rightDerived_app_eq {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {F G : Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : InjectiveResolution X) (n : ℕ) : (NatTrans.rightDerived α n).app X = CategoryStruct.comp (P.isoRightDerivedObj F n).hom (CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) (P.isoRightDerivedObj 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} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [Abelian D] {X : C} (P : InjectiveResolution X) (F : Functor C D) [F.Additive] : F.obj X ⟶ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).cycles 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

• P.toRightDerivedZero' F = ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).liftCycles (F.map (P.ι.f 0)) 1 CategoryTheory.InjectiveResolution.toRightDerivedZero'.proof_3 ⋯

@[simp]

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

@[simp]

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

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

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

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

noncomputable def CategoryTheory.Functor.toRightDerivedZero {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] : F ⟶ F.rightDerived 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} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] {X : C} (I : InjectiveResolution X) (F : Functor C D) [F.Additive] : F.toRightDerivedZero.app X = CategoryStruct.comp (I.toRightDerivedZero' F) (CategoryStruct.comp (CochainComplex.isoHomologyπ₀ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)).hom (I.isoRightDerivedObj F 0).inv)

instance CategoryTheory.instIsIsoAppToRightDerivedZeroOfInjective {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] (X : C) [Injective X] : IsIso (F.toRightDerivedZero.app X)

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

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

instance CategoryTheory.instIsIsoFunctorToRightDerivedZero {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] : IsIso F.toRightDerivedZero

noncomputable def CategoryTheory.Functor.rightDerivedZeroIsoSelf {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] : F.rightDerived 0 ≅ F

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

Equations

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

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] : F.rightDerivedZeroIsoSelf.inv = F.toRightDerivedZero

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] : CategoryStruct.comp F.rightDerivedZeroIsoSelf.hom F.toRightDerivedZero = CategoryStruct.id (F.rightDerived 0)

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] {Z : Functor C D} (h : F.rightDerived 0 ⟶ Z) : CategoryStruct.comp F.rightDerivedZeroIsoSelf.hom (CategoryStruct.comp F.toRightDerivedZero h) = h

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] : CategoryStruct.comp F.toRightDerivedZero F.rightDerivedZeroIsoSelf.hom = CategoryStruct.id F

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] {Z : Functor C D} (h : F ⟶ Z) : CategoryStruct.comp F.toRightDerivedZero (CategoryStruct.comp F.rightDerivedZeroIsoSelf.hom h) = h

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] (X : C) : CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) (F.toRightDerivedZero.app X) = CategoryStruct.id ((F.rightDerived 0).obj X)

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_app_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] (X : C) {Z : D} (h : (F.rightDerived 0).obj X ⟶ Z) : CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) (CategoryStruct.comp (F.toRightDerivedZero.app X) h) = h

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] (X : C) : CategoryStruct.comp (F.toRightDerivedZero.app X) (F.rightDerivedZeroIsoSelf.hom.app X) = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_app_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasInjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (F.toRightDerivedZero.app X) (CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) h) = h