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.
The definition is
injectiveResolutions C ⋙ F.mapHomotopyCategory _ ⋙ HomotopyCategory.homologyFunctor 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 #
CategoryTheory.Functor.rightDerivedObj_injective_zero
: the0
-th derived functor ofF
on an injective objectX
is isomorphic toF.obj X
.CategoryTheory.Functor.rightDerivedObj_injective_succ
: injective objects have no higher right derived functor.CategoryTheory.NatTrans.rightDerived
: the natural isomorphism between right derived functors induced by natural transformation.
Now, we assume PreservesFiniteLimits F
, then
CategoryTheory.Abelian.Functor.preserves_exact_of_preservesFiniteLimits_of_mono
: iff
is mono andExact f g
, thenExact (F.map f) (F.map g)
.CategoryTheory.Abelian.Functor.rightDerivedZeroIsoSelf
: if there are enough injectives, then there is a natural isomorphism(F.rightDerived 0) ≅ F
.
The right derived functors of an additive functor.
Instances For
We can compute a right derived functor using a chosen injective resolution.
Instances For
The 0-th derived functor of F
on an injective object X
is just F.obj X
.
Instances For
The higher derived functors vanish on injective objects.
Instances For
We can compute a right derived functor on a morphism using a descent of that morphism to a cochain map between chosen injective resolutions.
The natural transformation between right-derived functors induced by a natural transformation.
Instances For
A component of the natural transformation between right-derived functors can be computed using a chosen injective resolution.
If PreservesFiniteLimits F
and Mono f
, then Exact (F.map f) (F.map g)
if
Exact f g
.
Given P : InjectiveResolution X
, a morphism (F.rightDerived 0).obj X ⟶ F.obj X
given
PreservesFiniteLimits F
.
Instances For
Given P : InjectiveResolution X
, a morphism F.obj X ⟶ (F.rightDerived 0).obj X
.
Instances For
Given P : InjectiveResolution X
, the isomorphism (F.rightDerived 0).obj X ≅ F.obj X
if
PreservesFiniteLimits F
.
Instances For
Given P : InjectiveResolution X
and Q : InjectiveResolution Y
and a morphism f : X ⟶ Y
,
naturality of the square given by rightDerivedZeroToSelf_natural
.
Given PreservesFiniteLimits F
, the natural isomorphism (F.rightDerived 0) ≅ F
.