Spectral/README.md

17 lines
622 B
Markdown
Raw Normal View History

2015-11-18 22:00:07 +00:00
# Spectral
2015-11-18 22:09:18 +00:00
Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.
2015-12-04 00:55:16 +00:00
## Things to do for Lean SS 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.
###To Do:
- R-modules, vector spaces,
- some basic theory: product, tensor, hom, projective,
- categories of algebras, abelian categories,
###Already Done:
- definition of algebraic structures such as groups, rings, fields,
- some algebra: quotient, product, free.