Spectral Sequences

Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.

Currently in the project: Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Egbert Rijke, Mike Shulman.

Resources

• Mike's blog post
• We learned about the Serre spectral sequence from Hatcher's chapter about spectral sequences.
• 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.

Things to do for Lean spectral sequences project

###To Do:

• 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,
• some algebra: quotient, product, free.