Spectral Sequences in Homotopy Type Theory

Formalization project of the CMU HoTT group to formalize the Serre spectral sequence in Lean 2.

Update July 16, 2017: The construction of the Serre spectral sequence has been completed. The result is serre_convergence in cohomology.serre. The main algebra part is in algebra.exact_couple.

This repository also contains:

• a formalization of colimits which is in progress by Floris van Doorn, Egbert Rijke and Kristina Sojakova.
• a formalization and notes (in progress) about the smash product by Floris van Doorn and Stefano Piceghello.
• a formalization of The real projective spaces in homotopy type theory, Ulrik Buchholtz and Egbert Rijke, LICS 2017.
• a formalization of Higher Groups in Homotopy Type Theory, Ulrik Buchholtz, Floris van Doorn, Egbert Rijke, LICS 2018.
• the contents of the MRC 2017 group on formalizing homology in Lean.

Participants

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

Resources

• Mike's blog posts on ncatlab.
• 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.

Contents for Lean spectral sequences project

Outline

These projects are done

• Given a sequence of spectra and maps, indexed over ℤ, we get an exact couple, indexed over ℤ × ℤ.
• We can derive an exact couple.
• If the exact couple is bounded, we repeat this process to get a convergent spectral sequence.
• We construct the Atiyah-Hirzebruch and Serre spectral sequences for cohomology.

Future directions

• Hurewicz Theorem and Hurewicz theorem modulo a Serre class. There is a proof in Hatcher. Also, this might be useful.
• Homological Serre spectral sequence.
• Interaction between steenrod squares and cup product with spectral sequences
• ...

Algebra

To do

• Constructions: tensor, hom, projective, Tor (at least on groups)
• Finite groups, Finitely generated groups, torsion groups
• Serre classes
• vector spaces,

In Progress

Done

• groups, rings, fields, R-modules, graded R-modules.
• Constructions on groups and abelian groups:: subgroup, quotient, product, free groups.
• Constructions on ablian groups: direct sum, sequential colimi.
• exact sequences, short and long.
• chain complexes and homology.
• exact couples graded over an arbitrary indexing set.
• spectral sequence of an exact couple.
• convergence of spectral sequences.

Topology

To do

• 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.
• fiber and cofiber sequences of spectra, stability
  • limits are levelwise
  • colimits need to be spectrified
• long exact sequence from cofiber sequences of spectra
  • indexed on ℤ, need to splice together LES's
• Parametrized and unreduced homology
• Cup product on cohomology groups
• Show that the spectral sequence respect the cup product structure of cohomology
• Steenrod squares
• ...

To do (short-term easy projects)

• Compute cohomology groups of K(ℤ, n)
• Compute cohomology groups of ΩSⁿ
• Show that all fibration sequences between spheres are of the form Sⁿ → S²ⁿ⁺¹ → Sⁿ⁺¹.
• Compute fiber of K(φ, n) for group hom φ in general and if it's injective/surjective
• [Steve] Prove Σ (X × Y) ≃* Σ X ∨ Σ Y ∨ Σ (X ∧ Y), where Σ is suspension. See homotopy.susp_product

In Progress

• prespectra and spectra, indexed over an arbitrary type with a successor
  • think about equivariant spectra indexed by representations of G
• spectrification
  • adjoint to forgetful
  • as sequential colimit, prove induction principle
  • connective spectrum: is_conn n.-2 Eₙ
• Postnikov towers of spectra.
  • basic definition already there
  • fibers of Postnikov sequence unstably and stably
• parametrized spectra, parametrized smash and hom between types and spectra.
• Check Eilenberg-Steenrod axioms for reduced homology.

Done

• Most things in the HoTT Book up to Section 8.9 (see this file)
• pointed types, maps, homotopies and equivalences
• Eilenberg-MacLane spaces and EM-spectrum
• fiber sequence
  • already have the LES
  • need shift isomorphism
  • Hom'ing into a fiber sequence gives another fiber sequence.
• long exact sequence of homotopy groups of spectra, indexed on ℤ
• exact couple of a tower of spectra
  • need to splice together LES's

Usage and Contributing

• To compile this repository you can run linja (or path/to/lean2/bin/linja) in the main directory.
  • You will need a working version of Lean 2. Installation instructions for Lean 2 can be found here.
  • We will try to make sure that this repository compiles with the newest version of Lean 2.
• The preferred editor for Lean 2 is Emacs. Notes on the Emacs mode can be found here (for example if some unicode characters don't show up, or increase the spacing between lines by a lot).
• We try to separate the repository into the folders algebra, homotopy, homology, cohomology, spectrum and colimit. Homotopy theotic properties of types which do not explicitly mention homotopy, homology or cohomology groups (such as A ∧ B ≃* B ∧ A) are part of homotopy.
• If you contribute, please use rebase instead of merge (e.g. git pull -r).