mathlib3 documentation

category_theory.abelian.right_derived

Right-derived functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Now, we assume preserves_finite_limits F, then

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

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

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

Equations

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.