michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

update README

Browse source
This commit is contained in:
Floris van Doorn 2018-10-02 15:36:27 -04:00
parent 627deba24b
commit 3b25ec0266
1 changed files with 13 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
README.md
View file

@ -1,11 +1,16 @@
# Spectral Sequences in Homotopy Type Theory # Spectral Sequences in Homotopy Type Theory
Formalization project of the CMU HoTT group to formalize the Serre spectral sequence. Formalization project of the CMU HoTT group to formalize the Serre spectral sequence in Lean 2.
*Update July 16*: The construction of the Serre spectral sequence has been completed. The result is `serre_convergence` in `cohomology.serre`. *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`. The main algebra part is in `algebra.exact_couple`.
This repository also contains the contents of the MRC group on formalizing homology in Lean. 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 #### Participants
Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman. Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman.
@ -66,8 +71,9 @@ These projects are done
+ colimits need to be spectrified + colimits need to be spectrified
- long exact sequence from cofiber sequences of spectra - long exact sequence from cofiber sequences of spectra
+ indexed on ℤ, need to splice together LES's + indexed on ℤ, need to splice together LES's
- Cup product on cohomology groups
- Parametrized and unreduced homology - Parametrized and unreduced homology
- Cup product on cohomology groups
- Show that the spectral sequence respect the cup product structure of cohomology
- Steenrod squares - Steenrod squares
- ... - ...
@ -105,9 +111,9 @@ These projects are done
- exact couple of a tower of spectra - exact couple of a tower of spectra
+ need to splice together LES's + need to splice together LES's
## Contributing ## Usage and Contributing
- To compile this repository you will need a working version of Lean 2. Installation instructions for Lean 2 can be found [here](https://github.com/leanprover/lean2).
- We will try to make sure that this repository compiles with the newest version of Lean 2. - We will try to make sure that this repository compiles with the newest version of Lean 2.
- Installation instructions for Lean 2 can be found [here](https://github.com/leanprover/lean2).
- Some notes on the Emacs mode can be found [here](https://github.com/leanprover/lean2/blob/master/src/emacs/README.md) (for example if some unicode characters don't show up, or increase the spacing between lines by a lot). - Some notes on the Emacs mode can be found [here](https://github.com/leanprover/lean2/blob/master/src/emacs/README.md) (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`). - If you contribute, please use rebase instead of merge (e.g. `git pull -r`).
- We try to separate the repository into the folders `algebra`, `homotopy`, `homology`, `cohomology` 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`.