michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update README.md with roadmap based on Mike's blog post

Browse source
This commit is contained in:
Mike Shulman 2015-12-04 09:25:18 -08:00
parent 9e7b0bfae3
commit 35db866a61
1 changed files with 20 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
README.md
View file

@ -11,12 +11,30 @@ Currently in the project: Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris v
## Things to do for Lean spectral sequences project ## Things to do for Lean spectral sequences project
###To Do: ### Algebra To Do:
- R-modules, vector spaces, - R-modules, vector spaces,
- some basic theory: product, tensor, hom, projective, - some basic theory: product, tensor, hom, projective,
- categories of algebras, abelian categories, - categories of algebras, abelian categories,
- exact sequences, short and long
- snake lemma (Jeremy) - snake lemma (Jeremy)
- 5-lemma
- chain complexes and homology
- exact couples, probably just of Z-graded objects
- derived exact couples
- spectral sequence of an exact couple
- convergence of spectral sequences
###Already Done: ### Topology To Do:
- pointed types, fiber and cofiber sequences (is this in the library already?)
- prespectra and spectra, suspension
- spectrification
- parametrized smash and hom between types and spectra
- fiber and cofiber sequences of spectra, stability
- long exact sequences from (co)fiber sequences of spectra
- Eilenberg-MacLane spaces and spectra
- Postnikov towers of spectra
- exact couple of a tower of spectra
### Already Done:
- definition of algebraic structures such as groups, rings, fields, - definition of algebraic structures such as groups, rings, fields,
- some algebra: quotient, product, free. - some algebra: quotient, product, free.