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-03-06 13:23:30 -05:00
parent 97d7d0c108
commit 00978587e5
1 changed files with 9 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
README.md
View file

@ -1,8 +1,8 @@
# Spectral Sequences # Spectral Sequences
Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence. Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.
#### Participants #### Participants
Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman. Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman.
## Resources ## Resources
@ -20,7 +20,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
- some basic theory: product, tensor, hom, projective, - some basic theory: product, tensor, hom, projective,
- categories of algebras, [abelian categories](http://ncatlab.org/nlab/show/abelian+category), - categories of algebras, [abelian categories](http://ncatlab.org/nlab/show/abelian+category),
- exact sequences, short and long - exact sequences, short and long
- [snake lemma](http://ncatlab.org/nlab/show/snake+lemma) - [snake lemma](http://ncatlab.org/nlab/show/snake+lemma)
- [5-lemma](http://ncatlab.org/nlab/show/five+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) - [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 - [exact couples](http://ncatlab.org/nlab/show/exact+couple), probably just of Z-graded objects, and derived exact couples
@ -28,8 +28,8 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
- [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences) - [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences)
### Topology To Do: ### Topology To Do:
- HoTT Book chapter 8 - HoTT Book sections 8.7, 8.8.
- fiber and cofiber sequences (is this in the library already?) - cofiber sequences
- [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), suspension - [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), suspension
- [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification) - [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 - [parametrized spectra](http://ncatlab.org/nlab/show/parametrized+spectrum), parametrized smash and hom between types and spectra
@ -40,6 +40,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
- exact couple of a tower of spectra - exact couple of a tower of spectra
### Already Done: ### Already Done:
- pointed types - Most things in the HoTT Book up to Section 8.6 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md))
- definition of algebraic structures such as groups, rings, fields, - pointed types, maps, homotopies and equivalences
- some algebra: quotient, product, free. - definition of algebraic structures such as groups, rings, fields
- some algebra: quotient, product, free groups.