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: [Merged by Bors] - feat: definition of Ext-types in abelian categories #13963
• depends on: feat: the (covariant) long exact sequence of Ext #13879
• depends on: feat: definition of Ext-groups as morphisms in the derived category #13599
• depends on: [Merged by Bors] - feat: the distinguished triangle attached to a short exact sequence in an abelian category #13876
• depends on: [Merged by Bors] - feat(Algebra/Homology) the single complex functor preserves (co)limits #13875
• depends on: [Merged by Bors] - feat: the distinguished triangle in the derived category associated to a short exact sequence of cochain complexes #13742
• depends on: [Merged by Bors] - feat: the mapping cone of a monomorphism, up to a quasi-isomorphism #13675
• depends on: [Merged by Bors] - feat(CategoryTheory): more API for the commutation of functors with shifts #13757

[github-actions]

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:

• [Merged by Bors] - feat: definition of Ext-types in abelian categories #13963
• feat: the (covariant) long exact sequence of Ext #13879
• feat: definition of Ext-groups as morphisms in the derived category #13599
• [Merged by Bors] - feat: the distinguished triangle attached to a short exact sequence in an abelian category #13876
• [Merged by Bors] - feat(Algebra/Homology) the single complex functor preserves (co)limits #13875
• [Merged by Bors] - feat: the distinguished triangle in the derived category associated to a short exact sequence of cochain complexes #13742
• [Merged by Bors] - feat: the mapping cone of a monomorphism, up to a quasi-isomorphism #13675
• [Merged by Bors] - feat(CategoryTheory): more API for the commutation of functors with shifts #13757
  By Dependent Issues (🤖). Happy coding!

[joelriou]

Refactored in #15092