21 lines
963 B
Markdown
21 lines
963 B
Markdown
# Spectral Sequences
|
|
|
|
Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.
|
|
|
|
Currently in the project: Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Egbert Rijke, Mike Shulman.
|
|
|
|
## Resources
|
|
- We learned about the Serre spectral sequence from [Hatcher's chapter about spectral sequences](https://www.math.cornell.edu/~hatcher/SSAT/SSATpage.html).
|
|
- Lang's algebra (revised 3rd edition) contains a chapter on general homology theory, with a section on spectral sequences. Thus, we can use this book at least as an outline for the algebraic part of the project.
|
|
|
|
## Things to do for Lean spectral sequences project
|
|
|
|
###To Do:
|
|
- R-modules, vector spaces,
|
|
- some basic theory: product, tensor, hom, projective,
|
|
- categories of algebras, abelian categories,
|
|
- snake lemma (Jeremy)
|
|
|
|
###Already Done:
|
|
- definition of algebraic structures such as groups, rings, fields,
|
|
- some algebra: quotient, product, free.
|