feat: the (contravariant) long exact sequence of Ext

[joelriou]

Given a short exact short complex S in an abelian category C and B : C, we construct the contravariant (exact) sequence of LargeExt LargeExact S.X₃ B n₀ ⟶ LargeExact S.X₂ B n₀ ⟶ LargeExact S.X₁ B n₀ → LargeExact S.X₃ B n₁ ⟶ ... when n₀ + 1 = n₁.

---

This PR shall probably be split into two later.

• [ ] depends on: #13963
• [ ] depends on: #13879
• [x] depends on: #13599
• [x] depends on: #13876
• [x] depends on: #13875
• [x] depends on: #13742
• [x] depends on: #13675
• [x] depends on: #13757

[github-actions[bot]]

PR summary 1dd45cf8ea

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Triangulated.Opposite	959	1037	+78 (+8.13%)

---

Declarations diff

+ CommShift + Hom.opEquiv + IsColimit.ofIsZero + IsLimit.ofIsZero + LargeExt + LargeExtFunctor + LargeExtFunctor.obj + ShortComplex.eq_liftCycles_homologyπ_up_to_refinements + about + addEquiv + add_comp + add_hom + app_shift + comm + commShiftIso_comp_hom_app + commShiftIso_comp_inv_app + comm_app + comp_add + comp_assoc + comp_largeExtClass + comp_ofHom_id + contravariantSequence + contravariantSequenceIso + contravariantSequence_exact + contravariant_sequence_exact₁ + contravariant_sequence_exact₂ + contravariant_sequence_exact₃ + covariantSequence + covariantSequenceIso + covariantSequence_exact + covariant_sequence_exact₁ + covariant_sequence_exact₂ + covariant_sequence_exact₃ + decomp_from + decomp_to + descShortComplex + eq_liftCycles_homologyπ_up_to_refinements + equiv + homFromEquiv + homToEquiv + homologyFunctor_shift + homologyFunctor_shiftMap + homologySequenceComposableArrows₅ + homologySequenceComposableArrows₅_exact + homologySequenceδ_quotient_mapTriangle_obj + homologySequenceδ_triangleh + id + induced_shiftMap + inl_v_descShortComplex_f + inr_descShortComplex + inr_f_descShortComplex_f + instance (A : Cᵒᵖ) : (preadditiveCoyoneda.obj A).IsHomological + instance (A : Cᵒᵖ) : (preadditiveCoyoneda.obj A).ShiftSequence ℤ + instance (B : C) : (preadditiveYoneda.obj B).IsHomological + instance (B : C) : (preadditiveYoneda.obj B).ShiftSequence ℤ + instance (n : ℤ) : (singleFunctor C n).Additive := by + instance : (Q (C := C)).CommShift ℤ + instance : AddCommGroup (LargeExt X Y n) := (equiv X Y n).addCommGroup + instance : NatTrans.CommShift (quotientCompQhIso C).hom ℤ + instance : PreservesColimitsOfShape J (single C c i) + instance : PreservesFiniteColimits (single C c i) := ⟨by intros; infer_instance⟩ + instance : PreservesFiniteLimits (single C c i) := ⟨by intros; infer_instance⟩ + instance : PreservesLimitsOfShape J (single C c i) + instance {K L : CochainComplex C ℤ} (f : K ⟶ L) [QuasiIso f] : + isZero_single_comp_eval + largeExtClass + largeExtClass_comp + liftCycles_shift_homologyπ + mapTriangleCompIso + mapTriangleIso + map_distinguished_op_exact + mem_distTriang_iff + mk₀_comp_mk₀ + neg_hom + ofHom + ofHom_comp + ofHom_id_comp + ofIso + ofIso_compatibility + of_isIso + of_iso_inv + opEquiv + opEquiv' + opEquiv'_add_symm + opEquiv'_apply + opEquiv'_symm_add + opEquiv'_symm_apply + opEquiv'_symm_comp + opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift + opEquiv'_zero_add_symm + opEquiv_symm_add + opEquiv_symm_apply + opShiftFunctorEquivalence_add'_unitIso_inv_app + opShiftFunctorEquivalence_zero_unitIso_inv_app + postcomp + postcompFunctor + postcompIsoOfIso + postcompPostcompIso + preadditiveYoneda_map_distinguished + precomp + preservesColimitsOfShapeOfIsZero + preservesLimitsOfShapeOfIsZero + quasiIso_descShortComplex + shiftFunctorCompIsoId_add'_inv_app + shiftFunctorCompIsoId_zero_zero_hom_app + shiftFunctorCompIsoId_zero_zero_inv_app + shiftFunctorOpIso_add_neg_self + shiftFunctor_op + shift_app + singleCompEvalIsoSelf + singleFunctors + singleFunctorsPostcompQIso + singleFunctorsPostcompQhIso + singleTriangle + singleTriangleIso + singleTriangle_distinguished + singleδ + sub_hom + triangleOfSES + triangleOfSESIso + triangleOfSES_distinguished + triangleOfSESδ + whiskerLeft + whiskerRight + zero_hom + zsmul_hom +++ comp

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13963~~
• ~~leanprover-community/mathlib4#13879~~
• ~~leanprover-community/mathlib4#13599~~
• ~~leanprover-community/mathlib4#13876~~
• ~~leanprover-community/mathlib4#13875~~
• ~~leanprover-community/mathlib4#13742~~
• ~~leanprover-community/mathlib4#13675~~
• ~~leanprover-community/mathlib4#13757~~ By Dependent Issues (🤖). Happy coding!

[joelriou]

Refactored in #15092