Hom complex

Stream: homology

[Joël Riou]

In #6701, I am starting the construction of the complex of morphisms from a cochain complex to another. If F and G are cochain complexes (indexed by the integers), a term of type Cochain F G n consists of morphisms F.X p ⟶ G.X q whenever p + n = q. I also introduce the composition of cochains. (When the differential is introduced, the subtype of Cochain F G 0 consisting of cocycles will identify to morphisms F ⟶ G.)

This complex shall be a crucial tool in the construction and study of the derived category of an abelian category, especially for the construction of the triangulated structure on the homotopy category of an additive category. Indeed, when we introduce the mapping cone of a morphism φ : F ⟶ G (which in degree n is F.X (n+1) ⊞ G.X n, the degreewise left/right inclusions and projections are not all morphisms of complexes, but they can all be interpreted as cochains, e.g. inl φ : Cochain F (mappingCone φ) (-1), and these cochains satisfy similar relations as inl/inr/fst/snd do in the situation of categorical biproducts. I intend to study morphisms from and to mapping cones through the identification of morphisms with 0-cocycles, and then "the mapping cone will sort of behave like a biproduct".

[Johan Commelin]

Very nice!

[Johan Commelin]

Since this is already battle-tested by your follow-up work, and it all looks well-written, let's get it in mathlib asap.

[Johan Commelin]