From 8d9dd87f3a4f3bf2cea90b1f834f0dd51bfbb018 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 3 Dec 2015 19:55:16 -0500
Subject: [PATCH] Update README.md

---
 README.md | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/README.md b/README.md
index 5bafbf6..60fb70d 100644
--- a/README.md
+++ b/README.md
@@ -2,3 +2,15 @@
 
 Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.
 
+## Things to do for Lean SS project
+
+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.
+
+###To Do:
+- R-modules, vector spaces,
+- some basic theory: product, tensor, hom, projective,
+- categories of algebras, abelian categories,
+
+###Already Done:
+- definition of algebraic structures such as groups, rings, fields, 
+- some algebra: quotient, product, free.