Spectral/README.md

Spectral Sequences

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

Participants

Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman.

Resources

• 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.

Things to do for Lean spectral sequences project

Algebra To Do:

• 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

Topology To Do:

• HoTT Book sections 8.7, 8.8.
• 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 f cofiber sequences, then X^A → X^B → X^(coker f) is a fiber sequence.
• 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
• Eilenberg-MacLane spaces and spectra
• 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

Already Done:

• Most things in the HoTT Book up to Section 8.6 (see this file)
• pointed types, maps, homotopies and equivalences
• definition of algebraic structures such as groups, rings, fields
• some algebra: quotient, product, free groups.