mathlib4
mathlib4 copied to clipboard
leanprover-community
feat/refactor: redefinition of homology + derived categories
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.)
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:
- #4203
- #4204
- #4388
- #4609
- #4645
- #4787
- #4853
- #5250
- #5674
- #6008
- #6039
- #6089
- #6227
- #6230
- #6231
- #6245
- #6267
- #6279
- #6324
- #6443
- #6586
- #6994
- #7042
- #7047
- #7052
- #7192
- #7193
- #7194
- #7195
- #7197
- #7256
- #7262
- #7280
- #7623
- #7624
- #7806
- #7816
- #7817
- #7821
- #7954
- #7966
- #7993
- #7995
- #7996
- #7997
- #8058
- #8060
- #8069
- #8079
- #8081
- #8084
- #8091
- #8113
- #8114
- #8152
- #8159
- #8174
- #8200
- #8206
- #8208
- #8472
- #8468
- #8475
- #8490
- #8491
- #8507
- #8512
- #8593
- #8595
- #8706
- #8765
- #8766
- #8845
- #9022
Homological complexes:
* #9333 * #9335 * #9331Localization of categories:
- #6233
- #6235
- #6236
- #6867
- #6869
- #6887
- #6882
- #8041
- #8055
- #8069
- #8516
- #8864
- #8865
- #9702
- #9692
- #10606
- #10607
- #11721
- #11728
- #11737
Shifts on categories:
- #4429
- #6652
- #6653
- #6655
- #7268
- #7270
- #9001
Triangulated categories:
- #6377
- #6688
- #6815
- #7053
- #7324
- #7327
- #7336
- #7626
- #7641
- #9049
- #9073
- #10527
- #11738
- #11740
- #11759
Construction of the derived category:
- #6626
- #6701
- #6720
- #6894
- #7048
- #7049
- #7050
- #7201
- #7656
- #8937
- #8966
- #8969
- #8970
- #9054
- #9447
- #8951
- #9483
- #9508
- #9509
- #9592
- #9614
- #9615
- #9032
- #9370
- #9550
- #9686
- #9660
- #11760
Derived functors:
- #10195
- #10270
- #10301
- #10384
- #10413
Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause lake clean to delete your mathlib folder! If you need to do so, make sure to delete lakefile.olean manually before running any lake commands.
Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause lake clean to delete your mathlib folder! If you need to do so, make sure to delete lakefile.olean manually before running any lake commands.
@joelriou Is it possible to merge master into this branch? How large is the diff wrt current master? I assume that all the conflicts are due to recent PRs being merged, and once those conflicts are resolved the size of the diff will go down a bit?
