feat: definition of Ext-groups in abelian categories

[joelriou]

This PR defines Ext-groups in general abelian categories by shrinking types of morphisms in the derived category.

(When this API is developed further, it shall replace the current definition which applies only to categories with enough projectives.)

---

• [x] depends on: #13742
• [x] depends on: #13675
• [x] depends on: #13926
• [x] depends on: #13757
• [x] depends on: #13956
• [x] depends on: #13639
• [x] depends on: #13876

[github-actions[bot]]

PR summary 3c4c02692d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence	1084	1093	+9 (+0.83%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence	9
Mathlib.Algebra.Homology.DerivedCategory.Ext	1136

---

Declarations diff

+ Ext + comp + comp_assoc + comp_hom + ext + hasExt_iff + hasExt_of_hasDerivedCategory + hasSmallLocalizedShiftedHom_iff + homEquiv + instance : (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ + quasiIsoAt_shift_iff + quasiIso_shift_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13742~~
• ~~leanprover-community/mathlib4#13675~~
• ~~leanprover-community/mathlib4#13926~~
• ~~leanprover-community/mathlib4#13757~~
• ~~leanprover-community/mathlib4#13956~~
• ~~leanprover-community/mathlib4#13639~~
• ~~leanprover-community/mathlib4#13876~~ By Dependent Issues (🤖). Happy coding!

[erdOne]

Thanks! maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[kim-em]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style