Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.
Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman.
- Mike's blog post at the HoTT blog.
- Mike's blog post at the n-category café.
- The Licata-Finster article about Eilenberg-Mac Lane spaces.
- 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.
- Mac Lane's Homology contains a lot of homological algebra and a chapter on spectral sequences, including exact couples.
- R-modules, vector spaces,
- some basic theory: product, tensor, hom, projective,
- categories of algebras, abelian categories,
- exact sequences, short and long
- snake lemma
- 5-lemma
- chain complexes and homology
- exact couples, probably just of Z-graded objects, and derived exact couples
- spectral sequence of an exact couple
- convergence of spectral sequences
- fiber sequence
- already have the LES
- need shift isomorphism
- Hom'ing into a fiber sequence gives another fiber sequence.
- cofiber sequences
- Hom'ing out gives a fiber sequence: if
A → B → coker fcofiber sequences, thenX^A → X^B → X^(coker f)is a fiber sequence.
- Hom'ing out gives a fiber sequence: if
- prespectra and spectra, suspension
- try indexing on arbitrary successor structure
- think about equivariant spectra indexed by representations of
G
- spectrification
- adjoint to forgetful
- as sequential colimit, prove induction principle (if useful)
- connective spectrum:
is_conn n.-2 Eₙ
- parametrized spectra, parametrized smash and hom between types and spectra
- fiber and cofiber sequences of spectra, stability
- limits are levelwise
- colimits need to be spectrified
- long exact sequences from (co)fiber sequences of spectra
- indexed on ℤ, need to splice together LES's
- Postnikov towers of spectra
- basic definition already there
- fibers of Postnikov sequence unstably and stably
- exact couple of a tower of spectra
- need to splice together LES's
- Most things in the HoTT Book up to Section 8.9 (see this file)
- pointed types, maps, homotopies and equivalences
- definition of algebraic structures such as groups, rings, fields
- some algebra: quotient, product, free groups.
- Eilenberg-MacLane spaces and EM-spectrum