rename some files, update README

Notes/lessons.md

@@ -0,0 +1,18 @@
+In this file I (Floris) will collect some lessons learned from building and working with a HoTT library.
+Some of these things still need to be changes, some of them are already changed, and some of them are not worth the effort to change.
+
+- Spheres should be indexed by ℕ, it is not worth the effort to start counting at -1 (pointed spheres are much more useful anyway).
+- Don't have both susp and psusp. psusp should be the default (otherwise there is a distinction between iterate susp and iterate psusp)
+- Pointed maps should be special cases of dependent pointed maps. Pointed homotopies (between dependent pointed maps) should be special cases of dependent pointed maps, and pointed homotopies should be related themselves by pointed homotopies.
+- Type classes don't work well together with bundled structures and coercions in Lean (the instance is_contr_unit will not unify with (is_contr punit).
+- Overloading doesn't work well in Lean (mostly by degrading error messages)
+- It is useful to do categorical properties more uniformly. Define a 1-coherent ∞-category, which is a precategory (or category?) where the homs are not assumed to be sets. Examples include
+  + `Type` (with `→`),
+  + `A → B` (with `~`),
+  + `Type*` (with `→*`),
+  + `A →* B` (with `~*`),
+  + `A` (with `=`),
+  + spectrum (with `→ₛ`)
+  + ...
+  You cannot formulate everything in this, but it would be useful to compose natural transformations (instead of composing functions and manually show naturality).
+  Disadvantage: doesn't work

README.md

@@ -6,57 +6,88 @@ Formalization project of the CMU HoTT group towards formalizing the Serre spectr
 Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman.
 
 ## Resources
-- [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é.
+- [Mike's blog posts on ncatlab](https://ncatlab.org/homotopytypetheory/show/spectral+sequences).
 - 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
+## Contents for Lean spectral sequences project
 
-### Algebra To Do:
-- [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](http://ncatlab.org/nlab/show/abelian+category),
-- exact sequences, short and long
-- [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](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences)
+### Outline
 
-### Topology To Do:
+These projects are mostly done
+
+- Given a sequence of spectra and maps, indexed over `ℤ`, we get an exact couple, indexed over `ℤ × ℤ`.
+- We can derive an exact couple.
+- If the exact couple is bounded, we repeat this process to get a convergent spectral sequence.
+- We construct the Atiyah-Hirzebruch and Serre spectral sequences for cohomology.
+
+### Future directions
+- Hurewicz Theorem and Hurewicz theorem modulo a Serre class.
+- Homological Serre spectral sequence.
+- Interaction between steenrod squares and cup product with spectral sequences
+- ...
+
+### Algebra
+
+#### To do
+- Constructions: tensor, hom, projective, Tor (at least on groups)
+- Finite groups, Finitely generated groups, torsion groups
+- Serre classes
+- [vector spaces](http://ncatlab.org/nlab/show/vector+space),
+
+#### In Progress
+
+
+#### Done
+- groups, rings, fields, [R-modules](http://ncatlab.org/nlab/show/module), graded R-modules.
+- Constructions on groups and abelian groups:: subgroup, quotient, product, free groups.
+- Constructions on ablian groups: direct sum, sequential colimi.
+- exact sequences, short and long.
+- [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) graded over an arbitrary indexing set.
+- spectral sequence of an exact couple.
+- [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences).
+
+### Topology
+
+#### To do
+- cofiber sequences
+  + Hom'ing out gives a fiber sequence: if `A → B → coker f` cofiber
+    sequences, then `X^A → X^B → X^(coker f)` is a fiber sequence.
+- fiber and cofiber sequences of spectra, stability
+  + limits are levelwise
+  + colimits need to be spectrified
+- long exact sequence from cofiber sequences of spectra
+  + indexed on ℤ, need to splice together LES's
+- Cup product on cohomology groups
+- Parametrized and unreduced homology
+- Steenrod squares
+- ...
+
+#### 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`
+- [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification)
+  + adjoint to forgetful
+  + as sequential colimit, prove induction principle
+  + connective spectrum: `is_conn n.-2 Eₙ`
+- Postnikov towers of spectra.
+  + basic definition already there
+  + fibers of Postnikov sequence unstably and stably
+- [parametrized spectra](http://ncatlab.org/nlab/show/parametrized+spectrum), parametrized smash and hom between types and spectra.
+- Check Eilenberg-Steenrod axioms for reduced homology.
+
+
+#### Done
+- Most things in the HoTT Book up to Section 8.9 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md))
+- pointed types, maps, homotopies and equivalences
+- [Eilenberg-MacLane spaces](http://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space) and EM-spectrum
 - fiber sequence
   + already have the LES
   + need shift isomorphism
   + Hom'ing into a fiber sequence gives another fiber sequence.
-- cofiber sequences
-  + Hom'ing out gives a fiber sequence: if `A → B → coker f` cofiber
-    sequences, then `X^A → X^B → X^(coker f)` is a fiber sequence.
-- [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), suspension
-  + try indexing on arbitrary successor structure
-  + think about equivariant spectra indexed by representations of `G`
-- [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification)
-  + adjoint to forgetful
-  + as sequential colimit, prove induction principle (if useful)
-  + connective spectrum: `is_conn n.-2 Eₙ`
-- [parametrized spectra](http://ncatlab.org/nlab/show/parametrized+spectrum), parametrized smash and hom between types and spectra
-- fiber and cofiber sequences of spectra, stability
-  + limits are levelwise
-  + colimits need to be spectrified
-- long exact sequences from (co)fiber sequences of spectra
-  + indexed on ℤ, need to splice together LES's
-- Postnikov towers of spectra
-  + basic definition already there
-  + fibers of Postnikov sequence unstably and stably
+- long exact sequence of homotopy groups of spectra, indexed on ℤ
 - exact couple of a tower of spectra
   + need to splice together LES's
-
-### Already Done:
-- Most things in the HoTT Book up to Section 8.9 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md))
-- pointed types, maps, homotopies and equivalences
-- definition of algebraic structures such as groups, rings, fields
-- some algebra: quotient, product, free groups.
-- [Eilenberg-MacLane spaces](http://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space) and EM-spectrum

TODO.txt

@@ -1,34 +0,0 @@
-- reindex spheres
-- define pmap in terms of ppi
-
-- move move_to_lib and pointed to library
-
-talk with Favonia about:
-- dependent pointed maps
-- higher cube filling strategies
-- HIT equivalences
-- algebra
-
-
-/-
-Adjointness:
-Σ X ⟶ Y    X ∧ Y → Z
-=======    ===========
-X → Ω Y    X → (Y → Z)
-
-Spectrum: Y : ℕ → Type* with e : Ω Yₙ₊₁ ≃* Yₙ.
-
-
-HOMOLOGY:
-Hₙ(X, Y) :≡? ∥ X ∧ Ω² (Y (n+2)) ∥₀ ≃ ∥ X ∧ Y n ∥₀
-
-Eilenberg Steenrod-axioms:
-H : ℤ → Type* → AbGroup
-- functorial in second argument
-- (optional): respects pointed equivalences and pointed homotopies
-axioms:
-- the canonical map
--
-- Given (Xᵢ)ᵢ : I → Type* (satisfying AC?) the canonical functor
-  ⊕ hₙ
--/

algebra/direct_sum.hlean

@@ -6,7 +6,7 @@ Authors: Floris van Doorn, Egbert Rijke, Favonia
 Constructions with groups
 -/
 
-import .quotient_group .free_commutative_group .product_group
+import .quotient_group .free_abelian_group .product_group
 
 open eq is_equiv algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops lift
 

algebra/seq_colim.hlean

@@ -1,6 +1,6 @@
 --Authors: Robert Rose, Liz Vidaurre
 
-import .direct_sum .quotient_group ..move_to_lib
+import .direct_sum ..move_to_lib
 
 open eq algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops nat
 

algebra/serre.hlean

@@ -1,15 +0,0 @@
-/- The serre spectral sequence -/
-
--- Author: Floris van Doorn
-
-import .module_exact_couple
-
-namespace left_module
-
-  /- The Atiyah-Hirzebruch spectral sequence (with local coefficents) -/
-
-
-
-  /- The Serre Spectral Sequence -/
-
-end left_module

algebra/tensor.hlean

@@ -3,10 +3,10 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Egbert Rijke
 
-Constructions with groups
+Tensor group
 -/
 
-import .free_commutative_group
+import .free_abelian_group
 
 open eq algebra is_trunc sigma sigma.ops prod trunc function equiv
 namespace group

homotopy/serre.hlean

@@ -1,4 +1,4 @@
-import ..algebra.module_exact_couple .strunc .cohomology
+import ..algebra.spectral_sequence .strunc .cohomology
 
 open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift equiv is_equiv
      cohomology group sigma unit is_conn