The triangle of mapping cones of two monomorphisms, up to quasi-isomorphism

For composable morphisms a : X ⟶ Y and b : Y ⟶ Z of cochain complexes in an abelian category, Mathlib's triangle of mapping cones cone a ⟶ cone (a ≫ b) ⟶ cone b ⟶ (cone a)⟦1⟧ (mappingConeCompTriangle a b) is compared with the sequence of cokernels cokernel a ⟶ cokernel (a ≫ b) ⟶ cokernel b through the canonical maps mappingCone.descShortComplex from the mapping cones to the cokernels. When b is a monomorphism, the latter sequence is short exact, and the map in cohomology induced by the third morphism of the triangle is the connecting map of that short exact sequence (CochainComplex.mappingCone.shiftMap_mappingConeCompTriangle_mor₃). This extends Mathlib's mappingCone.homologySequenceδ_triangleh, which is the case a = 0.

theorem CochainComplex.mappingCone.shiftMap_mappingConeCompTriangle_mor₃ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y Z : CochainComplex C ℤ} (a : X ⟶ Y) (b : Y ⟶ Z) [CategoryTheory.Mono b] (n₀ n₁ : ℤ) (h : 1 + n₀ = n₁) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap (mappingConeCompTriangle a b).mor₃ n₀ n₁ h) (HomologicalComplex.homologyMap (descShortComplex (CategoryTheory.ShortComplex.cokernelSequence a)) n₁) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (descShortComplex (CategoryTheory.ShortComplex.cokernelSequence b)) n₀) (⋯.δ n₀ n₁ ⋯)

The map in cohomology induced by the third morphism cone b ⟶ (cone a)⟦1⟧ of the triangle of mapping cones of a and b, read through the canonical maps cone a ⟶ cokernel a and cone b ⟶ cokernel b (the latter a quasi-isomorphism, as b is a monomorphism), is the connecting map of the short exact sequence cokernel a ⟶ cokernel (a ≫ b) ⟶ cokernel b.