feat: the homological functor on the homotopy category of cochain complexes in an abelian category

[joelriou]

The homology functors on the homotopy category of cochain complexes in an abelian category are homological functors (in the sense that they send distinguished triangles to exact sequences). This PR also shows that the category of homological complexes in an abelian category is an abelian category.

---

This is a draft.

• [ ] depends on: #11740
• [ ] depends on: #11759

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#11740~~
• ~~leanprover-community/mathlib4#11759~~ By Dependent Issues (🤖). Happy coding!

[jcommelin]

Thanks :tada:

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style