feat/refactor: redefinition of homology + derived categories

[joelriou]

This PR contains a redefinition of homology, theorems about localization of categories, including triangulated categories, a construction of the derived category of an abelian category, derived functors, spectral sequences, etc. (This is made a PR only to facilitate navigation in the code of this branch.)

This formalization is outlined in the paper Formalization of derived categories in Lean/mathlib https://hal.science/hal-04546712

The homology of ShortComplex C (diagrams of two composable morphisms whose composition is zero) is developed in Algebra.Homology.ShortComplex. The files in that folder have been added one by one in separate PRs, and then, the current definition of homology has been replaced by this new definition in a refactor PR.

Homology refactor:

• [Merged by Bors] - feat: Algebra.Homology.ShortComplex.Basic #4203
• [Merged by Bors] - feat: basic definitions for Algebra.Homology.ShortComplex.Homology #4204
• [Merged by Bors] - feat: basic definitions for Algebra.Homology.ShortComplex.LeftHomology #4388
• [Merged by Bors] - feat: basic API for the left homology of short complexes #4609
• [Merged by Bors] - feat: more API for the left homology of short complexes #4645
• [Merged by Bors] - feat: more substantial API for the left homology of short complexes #4787
• [Merged by Bors] - feat: completion of ShortComplex.LeftHomology #4853
• [Merged by Bors] - feat: basic API for the right homology of short complexes #5250
• [Merged by Bors] - feat: left and right homology data are dual notions #5674
• [Merged by Bors] - feat: basic right homology API of short complexes #6008
• [Merged by Bors] - feat: the short complexes attached to homological complexes #6039
• [Merged by Bors] - feat: more API for the right homology of short complexes #6089
• [Merged by Bors] - feat: duality results for the right homology of short complexes #6227
• [Merged by Bors] - feat: developing the API of right homology of short complexes #6230
• [Merged by Bors] - feat: sufficient condition for a cycle map to be an isomorphism #6231
• [Merged by Bors] - feat: short complexes in functor categories #6245
• [Merged by Bors] - feat: the category of short complexes has limits #6267
• [Merged by Bors] - feat: basic results about preservation of kernels/cokernels #6279
• [Merged by Bors] - feat: the category of short complexes has colimits #6324
• [Merged by Bors] - feat: first definitions in the API for the homology of short complexes #6443
• [Merged by Bors] - feat: abelian categories have homology #6586
• [Merged by Bors] - feat: definition of the homology of a short complex #6994
• [Merged by Bors] - feat: maps induced on the homology of short complexes #7042
• [Merged by Bors] - feat: the category of short complexes is preadditive #7047
• [Merged by Bors] - feat: exactness of short complexes #7052
• [Merged by Bors] - feat: study of the left/right homology comparison morphism #7192
• [Merged by Bors] - feat: more API for the homology of short complexes #7193
• [Merged by Bors] - feat: relations between cycles, opcycles and homology of short complexes #7194
• [Merged by Bors] - feat: completion of the basic ShortComplex.Homology API #7195
• [Merged by Bors] - feat: functors which preserve homology #7197
• [Merged by Bors] - feat: functors which preserves right homology #7256
• [Merged by Bors] - feat: quasi-isomorphisms of short complexes #7262
• [Merged by Bors] - [Merged by Bors] - feat: exactness for short complexes coincides with CategoryTheory.Exact #7280
• [Merged by Bors] - feat: homology isomorphism for a functor which preserves homology #7623
• [Merged by Bors] - feat: naturality of the isomorphisms induced by functors which preserves homology #7624
• [Merged by Bors] - feat: various criteria for the exactness of short complexes #7806
• [Merged by Bors] - feat: a split short complex is exact #7816
• [Merged by Bors] - feat: more properties of homology in preadditive categories #7817
• [Merged by Bors] - feat(CategoryTheory): allow diagram chases by arguing up to refinements #7821
• [Merged by Bors] - refactor: introduce the new homology API for homological complex and rename the old one #7954
• [Merged by Bors] - feat: the homology of short complexes of abelian groups #7966
• [Merged by Bors] - feat: quasi-isomorphisms are preserved by functors which preserve homology #7993
• [Merged by Bors] - feat: more API for split short complexes #7995
• [Merged by Bors] - feat: exactness of short complexes in balanced categories #7996
• [Merged by Bors] - feat: completion of the file Algebra.Homology.ShortComplex.Exact #7997
• [Merged by Bors] - feat: short exact short complexes #8058
• [Merged by Bors] - feat: exactness of short complexes in concrete categories #8060
• [Merged by Bors] - feat: more API for homotopies of short complexes #8069
• [Merged by Bors] - feat: two homotopic maps of short complexes induce the same map in homology #8079
• [Merged by Bors] - feat: introducing the input data of the snake lemma #8081
• [Merged by Bors] - feat: the snake lemma #8084
• [Merged by Bors] - feat: more API for cycles and opcycles of homological complexes #8091
• [Merged by Bors] - feat: functoriality of the homology of homological complexes #8113
• [Merged by Bors] - feat: comparison isomorphism for the two homology APIs #8114
• [Merged by Bors] - feat(CategoryTheory): exact sequences #8152
• [Merged by Bors] - feat(CategoryTheory): more properties of exact sequences #8159
• [Merged by Bors] - feat: homology of short complexes of modules #8174
• [Merged by Bors] - feat(CategoryTheory): more API for limit kernel forks #8200
• [Merged by Bors] - feat: quasi-isomorphisms of homological complexes #8206
• [Merged by Bors] - refactor(Algebra/Homology): remove single₀ #8208
• [Merged by Bors] - feat: limits and colimits in the category of homological complexes #8472
• [Merged by Bors] - feat: the homology sequence of a short exact sequence of complexes #8468
• [Merged by Bors] - feat(CategoryTheory): more constructors for ComposableArrows #8475
• [Merged by Bors] - feat(CategoryTheory): naturality of the connecting homomorphism of the snake lemma #8490
• [Merged by Bors] - feat(CategoryTheory): more on the naturality of the connecting homomorphism of the snake lemma #8491
• [Merged by Bors] - feat(CategoryTheory): description of products and pullbacks in concrete categories #8507
• [Merged by Bors] - feat: computation of the connecting homomorphism of the snake lemma in concrete categories #8512
• [Merged by Bors] - refactor: use the new homology API for right derived functors #8593
• [Merged by Bors] - feat: the homology functor on the homotopy category for the new API #8595
• [Merged by Bors] - refactor(Algebra/Homology): use the new homology API #8706
• [Merged by Bors] - feat(Algebra/Homology): preliminary definitions for the homology sequence #8765
• [Merged by Bors] - feat(Algebra/Homology): computation of the connecting morphism of the snake lemma #8766
• [Merged by Bors] - feat(Algebra/Homology): API for the computation of the homology of homological complexes #8845
• [Merged by Bors] - refactor: use the new homology API for the four and the five lemmas #9022
• [Merged by Bors] - feat(CategoryTheory/Abelian): "three" lemmas #12649
• [Merged by Bors] - feat(Algebra/Homology): consequences of the homology sequence #12638

Homological complexes:

• [Merged by Bors] - refactor(Algebra/Homology): the category of bicomplexes #9333
• [Merged by Bors] - feat(Algebra/Homology): signs for the construction of the total complex #9335
• [Merged by Bors] - feat(Algebra/Homology): the total complex of a bicomplex #9331

Localization of categories:

• [Merged by Bors] - feat: 2-commutative squares #6233
• [Merged by Bors] - feat: localization of adjunctions between categories #6235
• [Merged by Bors] - feat: localization functors are preserved through equivalences #6236
• [Merged by Bors] - feat: uniqueness of the localized category up to equivalence #6867
• [Merged by Bors] - feat(CategoryTheory): morphisms of localizers #6869
• [Merged by Bors] - feat(CategoryTheory): misc lemmas about morphism properties #6887
• [Merged by Bors] - feat: composition of localization functors #6882
• [Merged by Bors] - feat(CategoryTheory): calculus of fractions #8041
• [Merged by Bors] - feat(CategoryTheory/Localization): equivalence relation on left fractions #8055
• [Merged by Bors] - feat: more API for homotopies of short complexes #8069
• [Merged by Bors] - feat(CategoryTheory): the localized category of a product category #8516
• [Merged by Bors] - feat(CategoryTheory): localization of product categories #8864
• [Merged by Bors] - feat(CategoryTheory): more API for product categories #8865
• [Merged by Bors] - feat(CategoryTheory): prerequisites for the existence of finite products in localized categories #9702
• [Merged by Bors] - feat(CategoryTheory/Localization): the localized category has finite products #9692
• [Merged by Bors] - feat(CategoryTheory/Localization): construction of a localized category using left fractions #10606
• [Merged by Bors] - feat(CategoryTheory/Localization): main results on left calculus of fractions #10607
• [Merged by Bors] - feat(CategoryTheory/Localization): dualize results for right calculus of fractions #11721
• [Merged by Bors] - feat(CategoryTheory/Localization): the localized category is preadditive #11728
• [Merged by Bors] - feat(CategoryTheory): more lemmas for the calculus of fractions #11737
• feat(CategoryTheory): the localized category is monoidal #12728

Shifts on categories:

• [Merged by Bors] - feat: functors which commute with shifts #4429
• [Merged by Bors] - feat: the induced shift on the target category of a functor #6652
• [Merged by Bors] - feat: the shift on a quotient category #6653
• [Merged by Bors] - feat: the shift induced on a localized category #6655
• [Merged by Bors] - feat: the naive shift on the opposite category #7268
• [Merged by Bors] - feat(CategoryTheory): the pullback of a shift by a monoid morphism #7270
• [Merged by Bors] - feat(CategoryTheory/Shift): sequences of functors from a category with a shift #9001
• [Merged by Bors] - feat(CategoryTheory/Shift): the induced shift sequence #11764

Triangulated categories:

• [Merged by Bors] - feat: more basic API for pretriangulated categories #6377
• [Merged by Bors] - feat: the shift on the category of triangles #6688
• [Merged by Bors] - feat: basic results about epi/mono/iso in pretriangulated categories #6815
• [Merged by Bors] - feat(CategoryTheory/Triangulated): shifting distinguished triangles and variations on the five lemma #7053
• [Merged by Bors] - feat: the shift on the opposite category #7324
• [Merged by Bors] - feat: definition of the distinguished triangles in the opposite category #7327
• [Merged by Bors] - feat: the pretriangulated structure on the opposite category #7336
• [Merged by Bors] - [Merged by Bors] - feat: pretriangulated categories have finite biproducts #7626
• [Merged by Bors] - feat(CategoryTheory): a product of distinguished triangles is distinguished #7641
• [Merged by Bors] - feat(CategoryTheory/Triangulated): triangulated functors #9049
• [Merged by Bors] - feat(CategoryTheory/Triangulated): Functor.mapTriangle commutes with the shift #9073
• [Merged by Bors] - feat(CategoryTheory/Triangulated): more API #10527
• [Merged by Bors] - feat(CategoryTheory): localization of pretriangulated categories #11738
• [Merged by Bors] - feat(CategoryTheory): triangulated subcategories #11740
• [Merged by Bors] - feat(CategoryTheory/Triangulated): homological functors #11759
• [Merged by Bors] - feat(CategoryTheory): localization of triangulated categories #11786
• [Merged by Bors] - feat(CategoryTheory): the class of morphisms whose cone belongs to a triangulated subcategory #11789
• [Merged by Bors] - feat(CategoryTheory/Triangulated): the long exact sequence of a homological functor #11805
• [Merged by Bors] - feat(CategoryTheory/Triangulated): t-structures #12619

Construction of the derived category:

• [Merged by Bors] - feat: the shift on the category of cochain complexes #6626
• [Merged by Bors] - feat: cochains of morphisms between cochain complexes #6701
• [Merged by Bors] - feat(Algebra): integer powers of -1 #6720
• [Merged by Bors] - feat: more API for the complex of morphisms between cochain complexes #6894
• [Merged by Bors] - feat: the shift on the homotopy category of cochain complexes #7048
• [Merged by Bors] - feat: the quotient category is preadditive #7049
• [Merged by Bors] - feat: the complex of homomorphisms between two cochain complexes #7050
• [Merged by Bors] - feat: the type of cocycles in the complex of morphisms between cochain complexes #7201
• [Merged by Bors] - [Merged by Bors] - feat: a homotopy of maps of cochain complexes identifies to (-1)-cochains in the complex of homomorphisms #7656
• [Merged by Bors] - feat(Algebra/Homology): right shifting cochains #8937
• [Merged by Bors] - feat(Algebra/Homology): binary biproducts of homological complexes #8966
• [Merged by Bors] - feat(Algebra/Homology): construction of the homotopy cofiber #8969
• [Merged by Bors] - feat(Algebra/Homology): the category of complexes up to quasi-isomorphisms #8970
• [Merged by Bors] - feat(Algebra/Homology): left shifting cochains #9054
• [Merged by Bors] - feat(Algebra/Homology): morphisms from the homotopy cofiber #9447
• [Merged by Bors] - feat(Algebra/Homology): the mapping cone #8951
• [Merged by Bors] - feat(Algebra/Homology): the cylinder of a homological complex #9483
• [Merged by Bors] - feat(Algebra/Homology): definition of the mapping cone #9508
• [Merged by Bors] - feat(Algebra/Homology): morphisms from the mapping cone #9509
• [Merged by Bors] - feat(Algebra/Homology/HomotopyCategory): various prerequisites for the triangulated structure #9592
• [Merged by Bors] - feat(Algebra/Homology/HomotopyCategory): definition of the distinguished triangles #9614
• [Merged by Bors] - feat(Algebra/Homology/HomotopyCategory): rotating and shifting distinguished triangles #9615
• [Merged by Bors] - feat: the homotopy category of cochain complexes is pretriangulated #9032
• [Merged by Bors] - feat(Algebra/Homology/HomotopyCategory): alternative description of distinguished triangles #9370
• [Merged by Bors] - feat(Algebra/Homology): the homotopy category of cochain complexes is triangulated #9550
• [Merged by Bors] - feat(Algebra/Homology): the class of quasi-isomorphisms in the homotopy category #9686
• [Merged by Bors] - feat(Algebra/Homology): two descriptions of the derived category as a localized category #9660
• [Merged by Bors] - feat: the homological functor on the homotopy category of cochain complexes in an abelian category #11760
• [Merged by Bors] - feat(Algebra/Homology): compatibilities of homology and shifts #11782
• [Merged by Bors] - feat: the derived category of an abelian category #11806

Derived functors:

• [Merged by Bors] - feat(CategoryTheory/Functor): definition of Kan extensions #10195
• [Merged by Bors] - feat(CategoryTheory): Guitart exact squares #10270
• [Merged by Bors] - feat(CategoryTheory/Localization): right resolutions #10301
• [Merged by Bors] - feat(CategoryTheory): the typeclass Functor.HasRightKanExtension #10384
• [Merged by Bors] - feat(CategoryTheory/Functor): pointwise left Kan extensions #10413
• [Merged by Bors] - feat(CategoryTheory): the left Kan extension functor #12168
• [Merged by Bors] - feat(CategoryTheory): vertical composition of Guitart exact squares #12627
• [Merged by Bors] - feat(CategoryTheory/Localization): left resolutions for localizer morphisms #12631
• [Merged by Bors] - feat(CategoryTheory): right derivability structures #12633
• [Merged by Bors] - feat(CategoryTheory): transport Kan extensions via equivalences #12785
• [Merged by Bors] - feat(CategoryTheory): right derived functors #12788

Refactor of Ext-groups:

• [Merged by Bors] - feat(CategoryTheory/Shift): functors from a category to a category with a shift #12607

---