# mathlibdocumentation

category_theory.abelian.right_derived

# Right-derived functors #

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

The definition is

injective_resolutions C ⋙ F.map_homotopy_category _ ⋙ homotopy_category.homology_functor D _ n


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

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

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

## Main results #

• category_theory.functor.right_derived_obj_injective_zero: the 0-th derived functor of F on an injective object X is isomorphic to F.obj X.
• category_theory.functor.right_derived_obj_injective_succ: injective objects have no higher right derived functor.
• category_theory.nat_trans.right_derived: the natural isomorphism between right derived functors induced by natural transformation.

Now, we assume preserves_finite_limits F, then

• category_theory.abelian.functor.preserves_exact_of_preserves_finite_limits_of_mono: if f is mono and exact f g, then exact (F.map f) (F.map g).
• category_theory.abelian.functor.right_derived_zero_iso_self: if there are enough injectives, then there is a natural isomorphism (F.right_derived 0) ≅ F.
noncomputable def category_theory.functor.right_derived {C : Type u} {D : Type u_1} (F : C D) [F.additive] (n : ) :
C D

The right derived functors of an additive functor.

Equations
@[simp]
theorem category_theory.functor.right_derived_obj_iso_hom {C : Type u} {D : Type u_1} (F : C D) [F.additive] (n : ) {X : C}  :
P).hom = (category_theory.functor.right_derived_obj_iso._proof_14.some.homotopy_equiv P).hom))
@[simp]
theorem category_theory.functor.right_derived_obj_iso_inv {C : Type u} {D : Type u_1} (F : C D) [F.additive] (n : ) {X : C}  :
P).inv = (category_theory.functor.right_derived_obj_iso._proof_14.some.homotopy_equiv P).inv))
noncomputable def category_theory.functor.right_derived_obj_iso {C : Type u} {D : Type u_1} (F : C D) [F.additive] (n : ) {X : C}  :

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

Equations
@[simp]
theorem category_theory.functor.right_derived_obj_injective_zero_hom {C : Type u} {D : Type u_1} (F : C D) [F.additive] (X : C)  :
= (category_theory.functor.right_derived_obj_iso._proof_14.some.homotopy_equiv .hom))
@[simp]
theorem category_theory.functor.right_derived_obj_injective_zero_inv {C : Type u} {D : Type u_1} (F : C D) [F.additive] (X : C)  :
= (category_theory.functor.right_derived_obj_iso._proof_14.some.homotopy_equiv .inv))
noncomputable def category_theory.functor.right_derived_obj_injective_zero {C : Type u} {D : Type u_1} (F : C D) [F.additive] (X : C)  :
(F.right_derived 0).obj X F.obj X

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

Equations
noncomputable def category_theory.functor.right_derived_obj_injective_succ {C : Type u} {D : Type u_1} (F : C D) [F.additive] (n : ) (X : C)  :
(F.right_derived (n + 1)).obj X 0

The higher derived functors vanish on injective objects.

Equations
@[simp]
theorem category_theory.functor.right_derived_obj_injective_succ_inv {C : Type u} {D : Type u_1} (F : C D) [F.additive] (n : ) (X : C)  :
.inv = _.iso_zero.inv (F.obj X) _ _ (n + 1)).map (category_theory.functor.right_derived_obj_iso._proof_14.some.homotopy_equiv .inv))
theorem category_theory.functor.right_derived_map_eq {C : Type u} {D : Type u_1} (F : C D) [F.additive] (n : ) {X Y : C} (f : Y X) (g : Q.cocomplex P.cocomplex) (w : Q.ι g = P.ι) :
(F.right_derived n).map f = Q).hom n).map g) P).inv

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

noncomputable def category_theory.nat_trans.right_derived {C : Type u} {D : Type u_1} {F G : C D} [F.additive] [G.additive] (α : F G) (n : ) :

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

Equations
@[simp]
theorem category_theory.nat_trans.right_derived_app {C : Type u} {D : Type u_1} {F G : C D} [F.additive] [G.additive] (α : F G) (n : ) (X : C) :
@[simp]
theorem category_theory.nat_trans.right_derived_id {C : Type u} {D : Type u_1} (F : C D) [F.additive] (n : ) :
@[simp, nolint]
theorem category_theory.nat_trans.right_derived_comp {C : Type u} {D : Type u_1} {F G H : C D} [F.additive] [G.additive] [H.additive] (α : F G) (β : G H) (n : ) :
theorem category_theory.nat_trans.right_derived_eq {C : Type u} {D : Type u_1} {F G : C D} [F.additive] [G.additive] (α : F G) (n : ) {X : C}  :
= P).hom P).inv

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

theorem category_theory.abelian.functor.preserves_exact_of_preserves_finite_limits_of_mono {C : Type u} {D : Type u} (F : C D) {X Y Z : C} {f : X Y} {g : Y Z} [F.additive] (ex : g) :

If preserves_finite_limits F and mono f, then exact (F.map f) (F.map g) if exact f g.

theorem category_theory.abelian.functor.exact_of_map_injective_resolution {C : Type u} {D : Type u} (F : C D) {X : C} [F.additive]  :
noncomputable def category_theory.abelian.functor.right_derived_zero_to_self_app {C : Type u} {D : Type u} (F : C D) [F.additive] {X : C}  :
(F.right_derived 0).obj X F.obj X

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

Equations
noncomputable def category_theory.abelian.functor.right_derived_zero_to_self_app_inv {C : Type u} {D : Type u} (F : C D) [F.additive] {X : C}  :
F.obj X (F.right_derived 0).obj X

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

Equations
theorem category_theory.abelian.functor.right_derived_zero_to_self_app_comp_inv {C : Type u} {D : Type u} (F : C D) [F.additive] {X : C}  :
noncomputable def category_theory.abelian.functor.right_derived_zero_to_self_app_iso {C : Type u} {D : Type u} (F : C D) [F.additive] {X : C}  :
(F.right_derived 0).obj X F.obj X

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

Equations
theorem category_theory.abelian.functor.right_derived_zero_to_self_natural {C : Type u} {D : Type u} (F : C D) [F.additive] {X Y : C} (f : X Y)  :

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

noncomputable def category_theory.abelian.functor.right_derived_zero_iso_self {C : Type u} {D : Type u} (F : C D) [F.additive]  :
F

Given preserves_finite_limits F, the natural isomorphism (F.right_derived 0) ≅ F.

Equations