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 2017-07-16 01:16:06 +01:00
parent c98c9bb1e6
commit e76f1db8ae
2 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
README.md
View file

@ -1,6 +1,9 @@
# Spectral Sequences # Spectral Sequences
Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence. Formalization project of the CMU HoTT group to formalize the Serre spectral sequence.
*Update July 16*: The construction of the Serre spectral sequence has been completed. The result is `serre_convergence` in `homotopy.serre`.
The main algebra part is in `algebra.spectral_sequence`.
This repository also contains the contents of the MRC group on formalizing homology in Lean. This repository also contains the contents of the MRC group on formalizing homology in Lean.
@ -18,7 +21,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
### Outline ### Outline
These projects are mostly done These projects are done
- Given a sequence of spectra and maps, indexed over `ℤ`, we get an exact couple, indexed over `ℤ × ℤ`. - Given a sequence of spectra and maps, indexed over `ℤ`, we get an exact couple, indexed over `ℤ × ℤ`.
- We can derive an exact couple. - We can derive an exact couple.

1
homotopy/serre.hlean
View file

@ -267,5 +267,4 @@ section serre
qed qed
end serre end serre
end spectrum end spectrum