From 80694430f95a70f59bb4833407849ce3827d1075 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sun, 6 Dec 2015 17:38:55 -0500 Subject: [PATCH 1/3] Update README.md --- README.md | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/README.md b/README.md index c0e1e45..b09a886 100644 --- a/README.md +++ b/README.md @@ -9,36 +9,35 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, - [Mike's blog post](http://homotopytypetheory.org/2013/08/08/spectral-sequences/) at the HoTT blog. - [Mike's blog post](https://golem.ph.utexas.edu/category/2013/08/what_is_a_spectral_sequence.html) at the n-category café. - The [Licata-Finster article](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) about Eilenberg-Mac Lane spaces. -- There is an [entry about spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification) on the nlab. - We learned about the Serre spectral sequence from [Hatcher's chapter about spectral sequences](https://www.math.cornell.edu/~hatcher/SSAT/SSATpage.html). - 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. ## Things to do for Lean spectral sequences project ### Algebra To Do: -- R-modules, vector spaces, +- [R-modules](http://ncatlab.org/nlab/show/module), [vector spaces](http://ncatlab.org/nlab/show/vector+space), - some basic theory: product, tensor, hom, projective, -- categories of algebras, abelian categories, +- categories of algebras, [abelian categories](http://ncatlab.org/nlab/show/abelian+category), - 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 +- [snake lemma](http://ncatlab.org/nlab/show/snake+lemma) +- [5-lemma](http://ncatlab.org/nlab/show/five+lemma) +- [chain complexes](http://ncatlab.org/nlab/show/chain+complex) and [homology](http://ncatlab.org/nlab/show/homology) +- [exact couples](http://ncatlab.org/nlab/show/exact+couple), probably just of Z-graded objects, and derived exact couples - spectral sequence of an exact couple -- convergence of spectral sequences +- [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences) ### 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 (is this in the library already?) +- [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and spectra, suspension +- [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification) +- [parametrized spectra](http://ncatlab.org/nlab/show/parametrized+spectrum), 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 +- [Eilenberg-MacLane spaces](http://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space) and spectra - Postnikov towers of spectra - exact couple of a tower of spectra ### Already Done: +- pointed types - definition of algebraic structures such as groups, rings, fields, - some algebra: quotient, product, free. From 0d4166bfbce8a4fa5124cd63b4b1311a18019f9a Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sun, 6 Dec 2015 18:00:19 -0500 Subject: [PATCH 2/3] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index b09a886..db719a0 100644 --- a/README.md +++ b/README.md @@ -28,7 +28,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, ### Topology To Do: - fiber and cofiber sequences (is this in the library already?) -- [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and spectra, suspension +- [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), suspension - [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification) - [parametrized spectra](http://ncatlab.org/nlab/show/parametrized+spectrum), parametrized smash and hom between types and spectra - fiber and cofiber sequences of spectra, stability From af9f77b71cd32a51fee4ebf32c796bed11982e58 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Mon, 7 Dec 2015 09:20:54 +0100 Subject: [PATCH 3/3] add Mac Lane's Homology to README.md --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index db719a0..e839737 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, - The [Licata-Finster article](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) about Eilenberg-Mac Lane spaces. - We learned about the Serre spectral sequence from [Hatcher's chapter about spectral sequences](https://www.math.cornell.edu/~hatcher/SSAT/SSATpage.html). - 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. +- Mac Lane's Homology contains a lot of homological algebra and a chapter on spectral sequences, including exact couples. ## Things to do for Lean spectral sequences project