Mirror of https://github.com/cmu-phil/Spectral in case it ever disappears

algebra | ||

archive | ||

cohomology | ||

colimit | ||

homology | ||

homotopy | ||

Notes | ||

spectrum | ||

.gitignore | ||

.project | ||

choice.hlean | ||

coind_colim.hlean | ||

component.hlean | ||

heq.hlean | ||

higher_groups.hlean | ||

LICENSE | ||

logic.hlean | ||

move_to_lib.hlean | ||

pointed.hlean | ||

pointed_binary.hlean | ||

pointed_cubes.hlean | ||

pointed_pi.hlean | ||

property.hlean | ||

pyoneda.hlean | ||

README.md | ||

univalent_subcategory.hlean |

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

- Hom'ing out gives a fiber sequence: if
- 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`

- think about equivariant spectra indexed by representations of
- 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`

).