[Merged by Bors] - feat: cochains of morphisms between cochain complexes

[joelriou]

This PR starts the construction of the cochain complex of morphisms from a cochain complex to another.

---

(I am sorry this PR is a little bit longer than the norm, but I wanted to include the composition of cochains.)

If F and G are two cochain complexes (indexed by the integers), I roughly define an element in Cochain F G n to be the datum of morphisms F.X p ⟶ G.X q for all integers p and q such that p + n = q. (Before I chose this design, I also experimented with a simpler definition : F.X p ⟶ G.X (p+n) for all p, but this lead to a nightmare of eqToHom popping everywhere.)

These cochains shall play a critical role in the study of the mapping cone of a morphism of cochain complexes, and in the verification of the axioms of triangulated categories for the homotopy category, which is the reason why this PR creates the file Algebra.Homology.HomotopyCategory.HomComplex.

(Note: the composition of cochains would be an example of an instance of the type class of graded heterogeneous multiplications which I attempted to introduce in #6678. I wish that the current API for graded types could be generalized in order to involve three graded types (i.e. some HMul rather than just Mul and SMul), and that the data would involve a multiplication X a → Y b → Z c whenever a + b = c rather than just X a → Y b → Z (a + b)., see the discussion there #6678. However, there is no hurry about a design decision here, because I shall not need more graded heterogeneous multiplications until the construction of the derived category of an abelian category and its triangulated structure is over...)

[jcommelin]

Thanks 🎉 Looking forward to the follow-up work.

bors merge

[bors]

Build failed:

• Build

[fpvandoorn]

This looks like a spurious error

bors r-
bors merge

[fpvandoorn]

also, if this didn't work:
bors d+

[bors]

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style