From 3b25ec0266bb708e75b396cbe52a3cceaa496622 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 2 Oct 2018 15:36:27 -0400 Subject: [PATCH] update README --- README.md | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 98e3937..6edc9a9 100644 --- a/README.md +++ b/README.md @@ -1,11 +1,16 @@ # 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`. -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 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 - long exact sequence from cofiber sequences of spectra + indexed on ℤ, need to splice together LES's -- Cup product on cohomology groups - Parametrized and unreduced homology +- Cup product on cohomology groups +- Show that the spectral sequence respect the cup product structure of cohomology - Steenrod squares - ... @@ -105,9 +111,9 @@ These projects are done - exact couple of a tower of spectra + 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. -- 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). +- 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`). -- 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`. \ No newline at end of file