Commit 2024-06-24 10:09 85a75afa

feat: the mapping cone of a monomorphism, up to a quasi-isomorphism (#13675) In this PR, given a short exact sequence S in the category of cochain complexes in an abelian category, we compare the homology sequence of S, and the homology sequence of the homological functor on the homotopy category applied to the distinguished triangle of the mapping cone of the monomorphism S.f. In particular, up to a quasi-isomorphism, the mapping cone of S.f identifies to S.X₃. In future PRs, this shall be used in order to attach a distinguished triangle in the derived category to S (#13742), and compare the homology sequence of S and the homology sequence attached to this distinguished triangle.