feat: the (covariant) long exact sequence of Ext

[joelriou]

Given a short exact short complex S in an abelian category C and A : C, we construct a long exact sequence LargeExact A S.X₁ n₀ ⟶ LargeExact A S.X₂ n₀ ⟶ LargeExact A S.X₃ n₀ → LargeExact A S.X₁ n₁ ⟶ ... when n₀ + 1 = n₁.

---

• [ ] depends on: #13963
• [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 67a4d065db

Import changes

Dependency changes

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

---

Declarations diff

+ CommShift + 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 + 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 + 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 (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 + postcomp + postcompFunctor + postcompIsoOfIso + postcompPostcompIso + preadditiveYoneda_map_distinguished + precomp + preservesColimitsOfShapeOfIsZero + preservesLimitsOfShapeOfIsZero + quasiIso_descShortComplex + 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#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]

This PR is refactored as #14515.