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

Update README.md

Browse source
This commit is contained in:
Egbert Rijke 2015-12-03 19:59:03 -05:00
parent 8d9dd87f3a
commit e0cc495abf
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
README.md
View file

@ -1,8 +1,10 @@
# Spectral
# 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.
## Things to do for Lean SS project
Currently in the project: Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Egbert Rijke, Mike Shulman.
## Things to do for Lean spectral sequences 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.
@ -10,6 +12,7 @@ Lang's algebra (revised 3rd edition) contains a chapter on general homology theo
- R-modules, vector spaces,
- some basic theory: product, tensor, hom, projective,
- categories of algebras, abelian categories,
- snake lemma (Jeremy)
###Already Done:
- definition of algebraic structures such as groups, rings, fields,