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

Merge branch 'master' of https://github.com/cmu-phil/Spectral

Browse source
This commit is contained in:
Egbert Rijke 2015-12-08 16:17:55 -05:00
commit 633d1f6d46
1 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
README.md
View file

@ -9,36 +9,36 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
- [Mike's blog post](http://homotopytypetheory.org/2013/08/08/spectral-sequences/) at the HoTT blog. - [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é. - [Mike's blog post](https://golem.ph.utexas.edu/category/2013/08/what_is_a_spectral_sequence.html) at the n-category café.
- The [Licata-Finster article](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) about Eilenberg-Mac Lane spaces. - The [Licata-Finster article](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) about Eilenberg-Mac Lane spaces.
- There is an [entry about spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification) on the nlab.
- We learned about the Serre spectral sequence from [Hatcher's chapter about spectral sequences](https://www.math.cornell.edu/~hatcher/SSAT/SSATpage.html). - 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. - 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.
- Mac Lane's Homology contains a lot of homological algebra and a chapter on spectral sequences, including exact couples.
## Things to do for Lean spectral sequences project ## Things to do for Lean spectral sequences project
### Algebra To Do: ### Algebra To Do:
- R-modules, vector spaces, - [R-modules](http://ncatlab.org/nlab/show/module), [vector spaces](http://ncatlab.org/nlab/show/vector+space),
- some basic theory: product, tensor, hom, projective, - some basic theory: product, tensor, hom, projective,
- categories of algebras, abelian categories, - categories of algebras, [abelian categories](http://ncatlab.org/nlab/show/abelian+category),
- exact sequences, short and long - exact sequences, short and long
- snake lemma (Jeremy) - [snake lemma](http://ncatlab.org/nlab/show/snake+lemma)
- 5-lemma - [5-lemma](http://ncatlab.org/nlab/show/five+lemma)
- chain complexes and homology - [chain complexes](http://ncatlab.org/nlab/show/chain+complex) and [homology](http://ncatlab.org/nlab/show/homology)
- exact couples, probably just of Z-graded objects - [exact couples](http://ncatlab.org/nlab/show/exact+couple), probably just of Z-graded objects, and derived exact couples
- derived exact couples
- spectral sequence of an exact couple - spectral sequence of an exact couple
- convergence of spectral sequences - [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences)
### Topology To Do: ### Topology To Do:
- pointed types, fiber and cofiber sequences (is this in the library already?) - fiber and cofiber sequences (is this in the library already?)
- prespectra and spectra, suspension - [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), suspension
- spectrification - [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification)
- 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
- fiber and cofiber sequences of spectra, stability - fiber and cofiber sequences of spectra, stability
- long exact sequences from (co)fiber sequences of spectra - long exact sequences from (co)fiber sequences of spectra
- Eilenberg-MacLane spaces and spectra - [Eilenberg-MacLane spaces](http://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space) and spectra
- Postnikov towers of spectra - Postnikov towers of spectra
- exact couple of a tower of spectra - exact couple of a tower of spectra
### Already Done: ### Already Done:
- pointed types
- 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.