Commit 2022-03-16 13:40 d495afdd

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)