[Merged by Bors] - feat(Algebra/Homology): the mapping cocone

[joelriou]

Given a morphism φ : K ⟶ L of cochain complexes, the mapping cone allows to obtain a triangle K ⟶ L ⟶ mappingCone φ ⟶ .... In this PR, we define the mapping cocone, which fits in a rotated triangle:
mappingCocone φ ⟶ K ⟶ L ⟶ ....

---

[github-actions]

PR summary 6fcaafd481

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (new file)	1279

---

Declarations diff

+ desc
+ descCochain
+ descCocycle
+ fst
+ id_X
+ inl
+ inl_comp_descCochain
+ inl_v_descCochain_v
+ inl_v_desc_f
+ inl_v_fst_f
+ inl_v_snd_v
+ inr
+ inr_comp_descCochain
+ inr_v_descCochain_v
+ inr_v_desc_f
+ inr_v_fst_f
+ inr_v_snd_v
+ lift
+ liftCochain
+ liftCochain_comp_fst
+ liftCochain_comp_snd
+ liftCochain_v_fst_f
+ liftCochain_v_snd_v
+ liftCocycle
+ lift_f_fst_f
+ lift_f_snd_v
+ lift_fst
+ mappingCocone
+ ofHom_desc
+ ofHom_lift
+ rotateTriangleIso
+ snd
+ triangle
+ δ_descCochain
+ δ_liftCochain

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (12.00, 0.00)

Current number	Change	Type
10883	12	backward.isDefEq

Current commit c6d733cc8e
Reference commit 6fcaafd481

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[robin-carlier]

Rest looks good, so,

Thanks!

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

[mattrobball]

Nice work on the signs!

bors delegate+

[mathlib-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.

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Build failed (retrying...):

• ci (staging) / Build

[mathlib-bors]

Canceled.

[joelriou]

Retrying...
bors merge

[mathlib-bors]

Build failed (retrying...):

• ci (staging) / Build

[joelriou]

bors cancel

[mathlib-bors]

Canceled.

[joelriou]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job