mathlib3

d495afdd - feat(category_theory/abelian/injective_resolution): descents of a morphism (#12703)

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)