# Commit 2022-03-16 13:40 d495afdd

View on Github →feat(category_theory/abelian/injective_resolution): descents of a morphism (#12703)
This pr dualise `src/category_theory/preadditive/projective_resolution.lean`

. The reason that it is moved to `abelian`

folder is because we want `exact f g`

from `exact g.op f.op`

instance.
This pr is splitted from #12545. This pr contains the following:
Given `I : InjectiveResolution X`

and `J : InjectiveResolution Y`

, any morphism `X ⟶ Y`

admits a descent to a chain map `J.cocomplex ⟶ I.cocomplex`

. It is a descent in the sense that `I.ι`

intertwine the descent and the original morphism, see `category_theory.InjectiveResolution.desc_commutes`

.
(Docstring contains more than what is currently in the file, but everything else will come soon)