mathlib documentation


Injective resolutions #

A injective resolution I : InjectiveResolution Z of an object Z : C consists of a -indexed cochain complex I.cocomplex of injective objects, along with a cochain map I.ι from cochain complex consisting just of Z in degree zero to C, so that the augmented cochain complex is exact.

Z ----> 0 ----> ... ----> 0 ----> ...
|       |                 |
|       |                 |
v       v                 v
I⁰ ---> I¹ ---> ... ----> Iⁿ ---> ...

An InjectiveResolution Z consists of a bundled -indexed cochain complex of injective objects, along with a quasi-isomorphism to the complex consisting of just Z supported in degree 0.

Except in situations where you want to provide a particular injective resolution (for example to compute a derived functor), you will not typically need to use this bundled object, and will instead use

  • injective_resolution Z: the -indexed cochain complex (equipped with injective and exact instances)
  • injective_resolution.ι Z: the cochain map from (single C _ 0).obj Z to injective_resolution Z (all the components are equipped with mono instances, and when the category is abelian we will show ι is a quasi-iso).
Instances for category_theory.InjectiveResolution
  • category_theory.InjectiveResolution.has_sizeof_inst

You will rarely use this typeclass directly: it is implied by the combination [enough_injectives C] and [abelian C].

Instances of this typeclass