New API for Ext and projective/injective resolutions

Stream: homology

[Joël Riou]

Currently, in mathlib, we still have two definitions of Ext-groups:

• the old one https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Abelian/Ext.html using projective resolutions;
• the new one https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.html

I have made a series of PR to mathlib so as to allow computations of the new Ext-groups using injective resolutions. When the dual results for projective definitions are added, it will be possible to completely remove the old definition.

[Joël Riou]

• #32105 feat(CategoryTheory): computing Ext-groups using an injective resolution

[Joël Riou]

• #32093 feat(Algebra/Homology): cohomology of HomComplex and morphisms in the homotopy category

[Joël Riou]

• #32091 feat(Algebra/Homology): cohomology of HomComplex

[Joël Riou]

• #32097 feat(Algebra/Homology): cochains/cocycles from/to single complexes

[Joël Riou]

• #31941 feat(Algebra/Homology): K-injective cochain complexes

[Joël Riou]

• #31900 feat(Algebra/Homology): morphisms to K-injective complexes in the derived category

[Joël Riou]

• #31843 feat(CategoryTheory/Triangulated): right orthogonal and localization

[Joël Riou]

• #32003 feat(CategoryTheory): injective resolutions as cochain complexes indexed by the integers

[Joël Riou]

The following #32003 #31843 #31941 #32091 should be ready for review.