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} [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) [F.Additive] : 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

• F.rightDerivedToHomotopyCategory = (CategoryTheory.injectiveResolutions C).comp (F.mapHomotopyCategory (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) [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_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) [F.Additive] {Z : HomotopyCategory D (ComplexShape.up ℕ)} (h : (HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj F).hom h) = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).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) [F.Additive] : CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) (J.isoRightDerivedToHomotopyCategoryObj F).hom = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).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) [F.Additive] {Z : HomotopyCategory D (ComplexShape.up ℕ)} (h : F.rightDerivedToHomotopyCategory.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv (CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)) (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj 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) [F.Additive] : CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv (F.rightDerivedToHomotopyCategory.map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).map φ) (J.isoRightDerivedToHomotopyCategoryObj 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) [F.Additive] (n : ℕ) : CategoryTheory.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} [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) [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_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) [F.Additive] (n : ℕ) {Z : D} (h : (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.rightDerived n).map f) (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedObj F n).hom h) = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).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) [F.Additive] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((F.rightDerived n).map f) (J.isoRightDerivedObj F n).hom = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).hom (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).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) [F.Additive] (n : ℕ) {Z : D} (h : (F.rightDerived n).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).inv (CategoryTheory.CategoryStruct.comp ((F.rightDerived n).map f) h) = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)) (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedObj 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) [F.Additive] (n : ℕ) : CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).inv ((F.rightDerived n).map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map φ) (J.isoRightDerivedObj 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) [F.Additive] (n : ℕ) (X : C) [CategoryTheory.Injective X] : CategoryTheory.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} [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) [F.Additive] (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).map f) Q.ι) : (F.rightDerived n).map f = CategoryTheory.CategoryStruct.comp (P.isoRightDerivedObj F n).hom (CategoryTheory.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} [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} [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} [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} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : CategoryTheory.InjectiveResolution X) : (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α).app X = CategoryTheory.CategoryStruct.comp (P.isoRightDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) (P.isoRightDerivedToHomotopyCategoryObj 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) [F.Additive] : CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.rightDerivedToHomotopyCategory

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) [F.Additive] [G.Additive] [H.Additive] {Z : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.up ℕ))} (h : H.rightDerivedToHomotopyCategory ⟶ 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) [F.Additive] [G.Additive] [H.Additive] : 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} [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} [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) [F.Additive] (n : ℕ) : CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.id F) n = CategoryTheory.CategoryStruct.id (F.rightDerived 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} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) {Z : CategoryTheory.Functor C D} (h : H.rightDerived 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} [F.Additive] [G.Additive] [H.Additive] (α : 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} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : CategoryTheory.InjectiveResolution X) (n : ℕ) : (CategoryTheory.NatTrans.rightDerived α n).app X = CategoryTheory.CategoryStruct.comp (P.isoRightDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map ((CategoryTheory.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} [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) [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_assoc {D : Type u_1} [CategoryTheory.Category.{u_4, u_1} D] [CategoryTheory.Abelian D] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] {X : C} (P : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] {Z : D} (h : ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F) (CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).iCycles 0) h) = CategoryTheory.CategoryStruct.comp (F.map (P.ι.f 0)) h

@[simp]

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

theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc {D : Type u_1} [CategoryTheory.Category.{u_4, u_1} D] [CategoryTheory.Abelian D] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] {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) [F.Additive] {Z : D} (h : ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj Q.cocomplex).cycles 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (Q.toRightDerivedZero' F) h) = CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0) h)

theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality {D : Type u_1} [CategoryTheory.Category.{u_4, u_1} D] [CategoryTheory.Abelian D] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] {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) [F.Additive] : CategoryTheory.CategoryStruct.comp (F.map f) (Q.toRightDerivedZero' F) = CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F) (HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0)

instance CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self {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) [F.Additive] (X : C) [CategoryTheory.Injective X] : CategoryTheory.IsIso ((CategoryTheory.InjectiveResolution.self X).toRightDerivedZero' F)

Equations

• ⋯ = ⋯

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

instance CategoryTheory.instIsIsoAppToRightDerivedZeroOfInjective {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) [F.Additive] (X : C) [CategoryTheory.Injective X] : CategoryTheory.IsIso (F.toRightDerivedZero.app X)

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsIsoToRightDerivedZero' {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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] {X : C} (P : CategoryTheory.InjectiveResolution X) : CategoryTheory.IsIso (P.toRightDerivedZero' F)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[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) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] : F.rightDerivedZeroIsoSelf.inv = F.toRightDerivedZero

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