From 4d7963d2262c7756537f7c5e1430ada07ae2803b Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 17 Jul 2017 16:09:09 +0100 Subject: [PATCH] update README. Add small projects, which anyone could work on --- README.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index b4885ee..1537012 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ 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`. +*Update July 16*: 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.spectral_sequence`. This repository also contains the contents of the MRC group on formalizing homology in Lean. @@ -71,6 +71,14 @@ These projects are done - Steenrod squares - ... +#### To do (short-term easy projects) + +- Compute cohomology groups of `K(ℤ, n)` +- Compute cohomology groups of `ΩSⁿ` +- Show that all fibration sequences between spheres are of the form `Sⁿ → S²ⁿ⁺¹ → Sⁿ⁺¹`. +- Compute fiber of `K(φ, n)` for group hom `φ` in general and if it's injective/surjective +- [Steve] Prove `Σ (X × Y) ≃* Σ X ∨ Σ Y ∨ Σ (X ∧ Y)`, where `Σ` is suspension. See `homotopy.susp_product` + #### In Progress - [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), indexed over an arbitrary type with a successor + think about equivariant spectra indexed by representations of `G`