Commit 2023-11-30 20:26 41529d1e

refactor(Algebra/Homology): use the new homology API (#8706) This PR refactors the construction of left derived functors using the new homology API: this also affects the dependencies (Ext functors, group cohomology, local cohomology). As a result, the old homology API is no longer used in any significant way in mathlib. Then, with this PR, the homology refactor is essentially complete. The organization of the files was made more coherent: the definition of a projective resolution is in Preadditive.ProjectiveResolution, the existence of resolutions when there are enough projectives is shown in Abelian.ProjectiveResolution, and the left derived functor is constructed in Abelian.LeftDerived; the dual results are in Preadditive.InjectiveResolution, Abelian.InjectiveResolution and Abelian.RightDerived.