From 35db866a61118ddedd78b0e89bc6a6ab8892fb13 Mon Sep 17 00:00:00 2001
From: Mike Shulman <viritrilbia@gmail.com>
Date: Fri, 4 Dec 2015 09:25:18 -0800
Subject: [PATCH] Update README.md with roadmap based on Mike's blog post

---
 README.md | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 7b8fecd..36b9c26 100644
--- a/README.md
+++ b/README.md
@@ -11,12 +11,30 @@ Currently in the project: Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris v
 
 ## Things to do for Lean spectral sequences project
 
-###To Do:
+### Algebra To Do:
 - R-modules, vector spaces,
 - some basic theory: product, tensor, hom, projective,
 - categories of algebras, abelian categories,
+- exact sequences, short and long
 - snake lemma (Jeremy) 
+- 5-lemma
+- chain complexes and homology
+- exact couples, probably just of Z-graded objects
+- derived exact couples
+- spectral sequence of an exact couple
+- convergence of spectral sequences
 
-###Already Done:
+### Topology To Do:
+- pointed types, fiber and cofiber sequences (is this in the library already?)
+- prespectra and spectra, suspension
+- spectrification
+- parametrized smash and hom between types and spectra
+- fiber and cofiber sequences of spectra, stability
+- long exact sequences from (co)fiber sequences of spectra
+- Eilenberg-MacLane spaces and spectra
+- Postnikov towers of spectra
+- exact couple of a tower of spectra
+
+### Already Done:
 - definition of algebraic structures such as groups, rings, fields, 
 - some algebra: quotient, product, free.