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

update README

Browse source
This commit is contained in:
Floris van Doorn 2016-06-26 09:25:50 +01:00
parent 4524af4ddc
commit d6d08ccd83
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
README.md
View file

@ -28,7 +28,6 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
- [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences)
### Topology To Do:
- HoTT Book sections 8.7, 8.8.
- fiber sequence
+ already have the LES
+ need shift isomorphism
@ -49,7 +48,6 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
+ colimits need to be spectrified
- long exact sequences from (co)fiber sequences of spectra
+ indexed on ℤ, need to splice together LES's
- [Eilenberg-MacLane spaces](http://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space) and spectra
- Postnikov towers of spectra
+ basic definition already there
+ fibers of Postnikov sequence unstably and stably
@ -57,7 +55,8 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
+ need to splice together LES's
### Already Done:
- Most things in the HoTT Book up to Section 8.6 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md))
- Most things in the HoTT Book up to Section 8.9 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md))
- pointed types, maps, homotopies and equivalences
- definition of algebraic structures such as groups, rings, fields
- some algebra: quotient, product, free groups.
- [Eilenberg-MacLane spaces](http://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space) and EM-spectrum