2015-12-04 00:59:03 +00:00
# Spectral Sequences
2015-11-18 22:09:18 +00:00
2015-12-04 00:59:03 +00:00
Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.
2015-11-18 22:09:18 +00:00
2015-12-04 21:57:32 +00:00
#### Participants
Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman.
2015-12-04 00:59:03 +00:00
2015-12-04 16:57:56 +00:00
## Resources
2015-12-04 21:53:35 +00:00
- [Mike's blog post ](http://homotopytypetheory.org/2013/08/08/spectral-sequences/ ) at the HoTT blog.
- [Mike's blog post ](https://golem.ph.utexas.edu/category/2013/08/what_is_a_spectral_sequence.html ) at the n-category café.
2015-12-04 22:00:38 +00:00
- The [Licata-Finster article ](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf ) about Eilenberg-Mac Lane spaces.
2015-12-04 16:57:56 +00:00
- 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.
2015-12-07 08:20:54 +00:00
- Mac Lane's Homology contains a lot of homological algebra and a chapter on spectral sequences, including exact couples.
2015-12-04 00:55:16 +00:00
2015-12-04 16:57:56 +00:00
## Things to do for Lean spectral sequences project
2015-12-04 00:55:16 +00:00
2015-12-04 17:25:18 +00:00
### Algebra To Do:
2015-12-06 22:38:55 +00:00
- [R-modules ](http://ncatlab.org/nlab/show/module ), [vector spaces ](http://ncatlab.org/nlab/show/vector+space ),
2015-12-04 00:55:16 +00:00
- some basic theory: product, tensor, hom, projective,
2015-12-06 22:38:55 +00:00
- categories of algebras, [abelian categories ](http://ncatlab.org/nlab/show/abelian+category ),
2015-12-04 17:25:18 +00:00
- exact sequences, short and long
2015-12-06 22:38:55 +00:00
- [snake lemma ](http://ncatlab.org/nlab/show/snake+lemma )
- [5-lemma ](http://ncatlab.org/nlab/show/five+lemma )
- [chain complexes ](http://ncatlab.org/nlab/show/chain+complex ) and [homology ](http://ncatlab.org/nlab/show/homology )
- [exact couples ](http://ncatlab.org/nlab/show/exact+couple ), probably just of Z-graded objects, and derived exact couples
2015-12-04 17:25:18 +00:00
- spectral sequence of an exact couple
2015-12-06 22:38:55 +00:00
- [convergence of spectral sequences ](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences )
2015-12-04 00:55:16 +00:00
2015-12-04 17:25:18 +00:00
### Topology To Do:
2015-12-06 22:38:55 +00:00
- fiber and cofiber sequences (is this in the library already?)
2015-12-06 23:00:19 +00:00
- [prespectra ](http://ncatlab.org/nlab/show/spectrum+object ) and [spectra ](http://ncatlab.org/nlab/show/spectrum ), suspension
2015-12-06 22:38:55 +00:00
- [spectrification ](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification )
- [parametrized spectra ](http://ncatlab.org/nlab/show/parametrized+spectrum ), parametrized smash and hom between types and spectra
2015-12-04 17:25:18 +00:00
- fiber and cofiber sequences of spectra, stability
- long exact sequences from (co)fiber sequences of spectra
2015-12-06 22:38:55 +00:00
- [Eilenberg-MacLane spaces ](http://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space ) and spectra
2015-12-04 17:25:18 +00:00
- Postnikov towers of spectra
- exact couple of a tower of spectra
### Already Done:
2015-12-06 22:38:55 +00:00
- pointed types
2015-12-04 00:55:16 +00:00
- definition of algebraic structures such as groups, rings, fields,
- some algebra: quotient, product, free.
