From 12a9345df1ac2f389ec6bf77c30e00d20d20a064 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 21 Sep 2017 20:14:24 -0400
Subject: [PATCH] Restructure spectral sequences, compute cohomology of
 projective space

This is still work in progress. Spectral sequences should be more usable, and probably the degrees of graded maps should be group homomorphisms so that we can reindex spectral sequences.
---
 algebra/exactness.hlean           |  24 +++
 algebra/graded.hlean              |   8 +
 algebra/left_module.hlean         |  47 +++++
 algebra/spectral_sequence.hlean   | 279 +++++++++++++++++++++++++-----
 algebra/submodule.hlean           |  34 +++-
 cohomology/basic.hlean            |  50 +++++-
 cohomology/projective_space.hlean | 137 +++++++++++++++
 cohomology/serre.hlean            |   6 +
 homotopy/wedge.hlean              |  42 ++++-
 move_to_lib.hlean                 |  42 ++++-
 spectrum/basic.hlean              |   7 +
 11 files changed, 624 insertions(+), 52 deletions(-)
 create mode 100644 cohomology/projective_space.hlean

diff --git a/algebra/exactness.hlean b/algebra/exactness.hlean
index 1af74b2..9fdec90 100644
--- a/algebra/exactness.hlean
+++ b/algebra/exactness.hlean
@@ -219,6 +219,30 @@ begin
   { exact is_short_exact.ker_in_im H }
 end
 
+lemma is_equiv_left_of_is_short_exact {A B C : Group} {f : A →g B} {g : B →g C}
+  (H : is_short_exact f g) (HC : is_contr C) : is_equiv f :=
+begin
+  apply is_equiv_of_is_surjective_of_is_embedding,
+    exact is_short_exact.is_emb H,
+    apply is_surjective_of_is_exact_of_is_contr, exact is_exact_of_is_short_exact H
+end
+
+lemma is_equiv_right_of_is_short_exact {A B C : Group} {f : A →g B} {g : B →g C}
+  (H : is_short_exact f g) (HA : is_contr A) : is_equiv g :=
+begin
+  apply is_equiv_of_is_surjective_of_is_embedding,
+    apply is_embedding_of_is_exact_g, exact is_exact_of_is_short_exact H,
+    exact is_short_exact.is_surj H
+end
+
+definition is_contr_right_of_is_short_exact {A B : Type} {C : Type*} {f : A → B} {g : B → C}
+  (H : is_short_exact f g) (HB : is_contr B) (HC : is_set C) : is_contr C :=
+is_contr_of_is_surjective g (is_short_exact.is_surj H) HB HC
+
+definition is_contr_left_of_is_short_exact {A B : Type} {C : Type*} {f : A → B} {g : B → C}
+  (H : is_short_exact f g) (HB : is_contr B) (a₀ : A) : is_contr A :=
+is_contr_of_is_embedding f (is_short_exact.is_emb H) _ a₀
+
 /- TODO: move and remove other versions -/
 
   definition is_surjective_qg_map {A : Group} (N : property A) [is_normal_subgroup A N] :
diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index c7a9194..d4f3f85 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -196,6 +196,10 @@ graded_hom.mk erfl (λi, lmid)
 variable {M}
 abbreviation gmid [constructor] := graded_hom_id M
 
+definition graded_hom_reindex [constructor] {J : Set} (e : J ≃ I) (f : M₁ →gm M₂) :
+  (λy, M₁ (e y)) →gm (λy, M₂ (e y)) :=
+graded_hom.mk' (e ⬝e deg f ⬝e e⁻¹ᵉ) (λy₁ y₂ p, f ↘ (eq_of_inv_eq p))
+
 definition gm_constant [constructor] (M₁ M₂ : graded_module R I) (d : I ≃ I) : M₁ →gm M₂ :=
 graded_hom.mk' d (gmd_constant d M₁ M₂)
 
@@ -647,5 +651,9 @@ definition gmod_ker_in_im (h : is_exact_gmod f f') ⦃i : I⦄ (m : M₂ i) (p :
   image (f ← i) m :=
 is_exact.ker_in_im (h (right_inv (deg f) i) idp) m p
 
+definition is_exact_gmod_reindex [constructor] {J : Set} (e : J ≃ I) (h : is_exact_gmod f f') :
+  is_exact_gmod (graded_hom_reindex e f) (graded_hom_reindex e f') :=
+λi j k p q, h (eq_of_inv_eq p) (eq_of_inv_eq q)
+
 
 end left_module
diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index 6dfe619..cdc293f 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -195,6 +195,11 @@ definition LeftModule_of_AddAbGroup {R : Ring} (G : AddAbGroup) (smul : R → G
   (h1 h2 h3 h4) : LeftModule R :=
 LeftModule.mk G (left_module_of_ab_group smul h1 h2 h3 h4)
 
+open unit
+definition trivial_LeftModule [constructor] (R : Ring) : LeftModule R :=
+LeftModule_of_AddAbGroup trivial_ab_group (λr u, star)
+  (λr u₁ u₂, idp) (λr₁ r₂ u, idp) (λr₁ r₂ u, idp) unit.eta
+
 section
   variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R}
 
@@ -389,6 +394,15 @@ end
     (φ : M₁ →a M₂) (h : Π(r : R) g, φ (r • g) = r • φ g) : M₁ →lm M₂ :=
   homomorphism.mk' φ (group.to_respect_add φ) h
 
+  definition group_isomorphism_of_lm_isomorphism [constructor] {M₁ M₂ : LeftModule R}
+    (φ : M₁ ≃lm M₂) : AddGroup_of_AddAbGroup M₁ ≃g AddGroup_of_AddAbGroup M₂ :=
+  group.isomorphism.mk (group_homomorphism_of_lm_homomorphism φ) (isomorphism.is_equiv_to_hom φ)
+
+  definition lm_isomorphism_of_group_isomorphism [constructor] {M₁ M₂ : LeftModule R}
+    (φ : AddGroup_of_AddAbGroup M₁ ≃g AddGroup_of_AddAbGroup M₂)
+    (h : Π(r : R) g, φ (r • g) = r • φ g) : M₁ ≃lm M₂ :=
+  isomorphism.mk (lm_homomorphism_of_group_homomorphism φ h) (group.isomorphism.is_equiv_to_hom φ)
+
   section
   local attribute pSet_of_LeftModule [coercion]
   definition is_exact_mod (f : M₁ →lm M₂) (f' : M₂ →lm M₃) : Type :=
@@ -425,6 +439,34 @@ end
     (HA : is_contr A) (HC : is_contr C) : is_contr B :=
   is_contr_middle_of_is_exact (is_exact_of_is_short_exact (short_exact_mod.h H))
 
+  definition is_contr_right_of_short_exact_mod {A B C : LeftModule R} (H : short_exact_mod A B C)
+    (HB : is_contr B) : is_contr C :=
+  is_contr_right_of_is_short_exact (short_exact_mod.h H) _ _
+
+  definition is_contr_left_of_short_exact_mod {A B C : LeftModule R} (H : short_exact_mod A B C)
+    (HB : is_contr B) : is_contr A :=
+  is_contr_left_of_is_short_exact (short_exact_mod.h H) _ pt
+
+  definition isomorphism_of_is_contr_left {A B C : LeftModule R} (H : short_exact_mod A B C)
+    (HA : is_contr A) : B ≃lm C :=
+  isomorphism.mk (short_exact_mod.g H)
+    begin
+      apply @is_equiv_right_of_is_short_exact _ _ _
+        (group_homomorphism_of_lm_homomorphism (short_exact_mod.f H))
+        (group_homomorphism_of_lm_homomorphism (short_exact_mod.g H)),
+      rexact short_exact_mod.h H, exact HA,
+    end
+
+  definition isomorphism_of_is_contr_right {A B C : LeftModule R} (H : short_exact_mod A B C)
+    (HC : is_contr C) : A ≃lm B :=
+  isomorphism.mk (short_exact_mod.f H)
+    begin
+      apply @is_equiv_left_of_is_short_exact _ _ _
+        (group_homomorphism_of_lm_homomorphism (short_exact_mod.f H))
+        (group_homomorphism_of_lm_homomorphism (short_exact_mod.g H)),
+      rexact short_exact_mod.h H, exact HC,
+    end
+
   end
 
   end
@@ -446,6 +488,11 @@ lm_homomorphism_of_group_homomorphism φ (to_respect_imul φ)
 definition lm_iso_int.mk [constructor] {A B : AbGroup} (φ : A ≃g B) :
   LeftModule_int_of_AbGroup A ≃lm LeftModule_int_of_AbGroup B :=
 isomorphism.mk (lm_hom_int.mk φ) (group.isomorphism.is_equiv_to_hom φ)
+
+definition group_isomorphism_of_lm_isomorphism_int [constructor] {A B : AbGroup}
+  (φ : LeftModule_int_of_AbGroup A ≃lm LeftModule_int_of_AbGroup B) : A ≃g B :=
+group_isomorphism_of_lm_isomorphism φ
+
 end int
 
 end left_module
diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean
index 4f7152b..5240c7d 100644
--- a/algebra/spectral_sequence.hlean
+++ b/algebra/spectral_sequence.hlean
@@ -7,12 +7,70 @@
 
 import .graded ..spectrum.basic .product_group
 
-open algebra is_trunc left_module is_equiv equiv eq function nat sigma sigma.ops set_quotient
+open algebra is_trunc left_module is_equiv equiv eq function nat sigma set_quotient
 
 /- exact couples -/
 
 namespace left_module
 
+  section
+  /- move to left_module -/
+  structure is_built_from.{u v w} {R : Ring} (D : LeftModule.{u v} R)
+      (E : ℕ → LeftModule.{u w} R) : Type.{max u (v+1) w} :=
+    (part : ℕ → LeftModule.{u v} R)
+    (ses : Πn, short_exact_mod (E n) (part n) (part (n+1)))
+    (e0 : part 0 ≃lm D)
+    (n₀ : ℕ)
+    (HD' : Π(s : ℕ), n₀ ≤ s → is_contr (part s))
+
+  open is_built_from
+  universe variables u v w
+  variables {R : Ring.{u}} {D D' : LeftModule.{u v} R} {E E' : ℕ → LeftModule.{u w} R}
+
+  definition is_built_from_shift (H : is_built_from D E) :
+    is_built_from (part H 1) (λn, E (n+1)) :=
+  is_built_from.mk (λn, part H (n+1)) (λn, ses H (n+1)) isomorphism.rfl (pred (n₀ H))
+    (λs Hle, HD' H _ (le_succ_of_pred_le Hle))
+
+  definition isomorphism_of_is_contr_part (H : is_built_from D E) (n : ℕ) (HE : is_contr (E n)) :
+    part H n ≃lm part H (n+1) :=
+  isomorphism_of_is_contr_left (ses H n) HE
+
+  definition is_contr_submodules (H : is_built_from D E) (HD : is_contr D) (n : ℕ) :
+    is_contr (part H n) :=
+  begin
+    induction n with n IH,
+    { exact is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e0 H)) },
+    { exact is_contr_right_of_short_exact_mod (ses H n) IH }
+  end
+
+  definition is_contr_quotients (H : is_built_from D E) (HD : is_contr D) (n : ℕ) :
+    is_contr (E n) :=
+  begin
+    apply is_contr_left_of_short_exact_mod (ses H n),
+    exact is_contr_submodules H HD n
+  end
+
+  definition is_contr_total (H : is_built_from D E) (HE : Πn, is_contr (E n)) : is_contr D :=
+  have is_contr (part H 0), from
+  nat.rec_down (λn, is_contr (part H n)) _ (HD' H _ !le.refl)
+    (λn H2, is_contr_middle_of_short_exact_mod (ses H n) (HE n) H2),
+  is_contr_equiv_closed (equiv_of_isomorphism (e0 H))
+
+  definition is_built_from_isomorphism (e : D ≃lm D') (f : Πn, E n ≃lm E' n)
+    (H : is_built_from D E) : is_built_from D' E' :=
+  ⦃is_built_from, H, e0 := e0 H ⬝lm e,
+    ses := λn, short_exact_mod_isomorphism (f n)⁻¹ˡᵐ isomorphism.rfl isomorphism.rfl (ses H n)⦄
+
+  definition is_built_from_isomorphism_left (e : D ≃lm D') (H : is_built_from D E) :
+    is_built_from D' E :=
+  ⦃is_built_from, H, e0 := e0 H ⬝lm e⦄
+
+  definition isomorphism_zero_of_is_built_from (H : is_built_from D E) (p : n₀ H = 1) : E 0 ≃lm D :=
+  isomorphism_of_is_contr_right (ses H 0) (HD' H 1 (le_of_eq p)) ⬝lm e0 H
+
+  end
+
   structure exact_couple (R : Ring) (I : Set) : Type :=
     (D E : graded_module R I)
     (i : D →gm D) (j : D →gm E) (k : E →gm D)
@@ -22,6 +80,13 @@ namespace left_module
 
   open exact_couple
 
+  definition exact_couple_reindex [constructor] {R : Ring} {I J : Set} (e : J ≃ I)
+    (X : exact_couple R I) : exact_couple R J :=
+  ⦃exact_couple, D := λy, D X (e y), E := λy, E X (e y),
+    i := graded_hom_reindex e (i X), j := graded_hom_reindex e (j X),
+    k := graded_hom_reindex e (k X), ij := is_exact_gmod_reindex e (ij X),
+    jk := is_exact_gmod_reindex e (jk X), ki := is_exact_gmod_reindex e (ki X)⦄
+
   namespace derived_couple
   section
 
@@ -45,6 +110,10 @@ namespace left_module
   definition is_contr_D' {x : I} (H : is_contr (D x)) : is_contr (D' x) :=
   !is_contr_image_module
 
+  definition E'_isomorphism {x : I} (H1 : is_contr (E ((deg d)⁻¹ᵉ x)))
+    (H2 : is_contr (E (deg d x))) : E' x ≃lm E x :=
+  @(homology_isomorphism _ _) H1 H2
+
   definition i' : D' →gm D' :=
   graded_image_lift i ∘gm  graded_submodule_incl (λx, image (i ← x))
 
@@ -114,9 +183,10 @@ namespace left_module
   end
 
   definition k' : E' →gm D' :=
-  @graded_quotient_elim _ _ _ _ _ _ (graded_submodule_functor k k_lemma1)
+  @graded_quotient_elim _ _ _ _ _ _ k₂
                        (by intro x m h; cases m with [m1, m2]; exact k_lemma2 m1 m2 h)
 
+  open sigma.ops
   definition i'_eq ⦃x : I⦄ (m : D x) (h : image (i ← x) m) : (i' x ⟨m, h⟩).1 = i x m :=
   by reflexivity
 
@@ -234,18 +304,34 @@ namespace left_module
   begin
     apply is_bounded.mk' (λx, max (B x) (B'' x)) B',
     { intro x y s p h, induction p, exact Dub (le.trans !le_max_left h) },
-    { intro x y z s p q h, induction p, induction q,
+    { exact abstract begin intro x y z s p q h, induction p, induction q,
       refine transport (λx, is_surjective (i X x)) _ (Dlb h),
-      rewrite [-iterate_succ], apply iterate_left_inv },
+      rewrite [-iterate_succ], apply iterate_left_inv end end },
     { intro x y s p h, induction p, exact Elb (le.trans !le_max_right h) },
     { assumption },
     { assumption }
   end
 
+  open is_bounded
+  definition is_bounded_reindex [constructor] {R : Ring} {I J : Set} (e : J ≃ I)
+    {X : exact_couple R I} (HH : is_bounded X) : is_bounded (exact_couple_reindex e X) :=
+  begin
+    apply is_bounded.mk' (B HH ∘ e) (B' HH ∘ e),
+    { intros x y s p h, refine Dub HH _ h,
+      refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x, exact to_right_inv e _ },
+    { intros x y z s p q h, refine Dlb HH _ _ h,
+      refine (iterate_hsquare e _ s y)⁻¹ ⬝ ap e q, intro x, exact to_right_inv e _ },
+    { intro x y s p h, refine Elb HH _ h,
+      refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x, exact to_right_inv e _ },
+    { intro y, exact ap e⁻¹ᵉ (ap (deg (i X)) (to_right_inv e _) ⬝
+        deg_ik_commute HH (e y) ⬝ ap (deg (k X)) (to_right_inv e _)⁻¹) },
+    { intro y, exact ap e⁻¹ᵉ (ap (deg (i X)) (to_right_inv e _) ⬝
+        deg_ij_commute HH (e y) ⬝ ap (deg (j X)) (to_right_inv e _)⁻¹) }
+  end
+
   namespace convergence_theorem
   section
 
-  open is_bounded
   parameters {R : Ring} {I : Set} (X : exact_couple R I) (HH : is_bounded X)
 
   local abbreviation B := B HH
@@ -256,25 +342,7 @@ namespace left_module
   local abbreviation deg_ik_commute := deg_ik_commute HH
   local abbreviation deg_ij_commute := deg_ij_commute HH
 
-  definition deg_iterate_ik_commute (n : ℕ) :
-    hsquare (deg (k X)) (deg (k X)) ((deg (i X))^[n]) ((deg (i X))^[n]) :=
-  iterate_commute n deg_ik_commute
-
-  definition deg_iterate_ij_commute (n : ℕ) :
-    hsquare (deg (j X)) (deg (j X)) ((deg (i X))⁻¹ᵉ^[n]) ((deg (i X))⁻¹ᵉ^[n]) :=
-  iterate_commute n (hvinverse deg_ij_commute)
-
-  definition B2 (x : I) : ℕ := max (B (deg (k X) x)) (B ((deg (j X))⁻¹ x))
-  definition Eub ⦃x y : I⦄ ⦃s : ℕ⦄ (p : (deg (i X))^[s] x = y) (h : B2 x ≤ s) :
-    is_contr (E X y) :=
-  begin
-    induction p,
-    refine @(is_contr_middle_of_is_exact (exact_couple.jk X (right_inv (deg (j X)) _) idp)) _ _ _,
-    exact Dub (iterate_commute s (hhinverse deg_ij_commute) x) (le.trans !le_max_right h),
-    exact Dub !deg_iterate_ik_commute (le.trans !le_max_left h)
-  end
-
-  -- we start counting pages at 0
+  /- We start counting pages at 0, which corresponds to what is usually called the second page -/
   definition page (r : ℕ) : exact_couple R I :=
   iterate derived_couple r X
 
@@ -324,6 +392,45 @@ namespace left_module
     (deg (d (page r)))⁻¹ ~ (deg (k X))⁻¹ ∘ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ :=
   compose2 (to_inv_homotopy_inv (deg_k r)) (deg_j_inv r)
 
+  definition E_isomorphism' {x : I} {r₁ r₂ : ℕ} (H : r₁ ≤ r₂)
+    (H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+    (H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (deg (d (page r)) x))) :
+    E (page r₂) x ≃lm E (page r₁) x :=
+  begin
+    assert H2 : Π⦃r⦄, r₁ ≤ r → r ≤ r₂ → E (page r) x ≃lm E (page r₁) x,
+    { intro r Hr₁ Hr₂,
+      induction Hr₁ with r Hr₁ IH, reflexivity,
+      let Hr₂' := le_of_succ_le Hr₂,
+      exact E'_isomorphism (page r) (is_contr_E r _ (H1 Hr₁ Hr₂)) (is_contr_E r _ (H2 Hr₁ Hr₂))
+        ⬝lm IH Hr₂' },
+    exact H2 H (le.refl _)
+  end
+
+  definition E_isomorphism0' {x : I} {r : ℕ}
+    (H1 : Πr, is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+    (H2 : Πr, is_contr (E X (deg (d (page r)) x))) : E (page r) x ≃lm E X x :=
+  E_isomorphism' (zero_le r) _ _
+
+  parameter {X}
+
+  definition deg_iterate_ik_commute (n : ℕ) :
+    hsquare (deg (k X)) (deg (k X)) ((deg (i X))^[n]) ((deg (i X))^[n]) :=
+  iterate_commute n deg_ik_commute
+
+  definition deg_iterate_ij_commute (n : ℕ) :
+    hsquare (deg (j X)) (deg (j X)) ((deg (i X))⁻¹ᵉ^[n]) ((deg (i X))⁻¹ᵉ^[n]) :=
+  iterate_commute n (hvinverse deg_ij_commute)
+
+  definition B2 (x : I) : ℕ := max (B (deg (k X) x)) (B ((deg (j X))⁻¹ x))
+  definition Eub ⦃x y : I⦄ ⦃s : ℕ⦄ (p : (deg (i X))^[s] x = y) (h : B2 x ≤ s) :
+    is_contr (E X y) :=
+  begin
+    induction p,
+    refine @(is_contr_middle_of_is_exact (exact_couple.jk X (right_inv (deg (j X)) _) idp)) _ _ _,
+    exact Dub (iterate_commute s (hhinverse deg_ij_commute) x) (le.trans !le_max_right h),
+    exact Dub !deg_iterate_ik_commute (le.trans !le_max_left h)
+  end
+
   definition B3 (x : I) : ℕ :=
   max (B (deg (j X) (deg (k X) x))) (B2 ((deg (k X))⁻¹ ((deg (j X))⁻¹ x)))
 
@@ -344,12 +451,6 @@ namespace left_module
   begin
     revert x y z s H p q, induction r with r IH: intro x y z s H p q,
     { exact Dlb p q H },
-/- the following is a start of the proof that i is surjective using that E is contractible (but this
-   makes the bound 1 higher than necessary -/
-      -- induction p, change is_surjective (i X x),
-      -- apply @(is_surjective_of_is_exact_of_is_contr (exact_couple.ij X idp idp)),
-      -- refine Elb _ H,
-      -- exact sorry
     { change is_surjective (i' (page r) ↘ p),
       apply is_surjective_i', intro z' q',
       refine IH _ _ _ _ (le.trans H (le_of_eq (succ_add s r)⁻¹)) _ _,
@@ -379,6 +480,22 @@ namespace left_module
   definition Dinfstable {x y : I} {r : ℕ} (Hr : B' y ≤ r) (p : x = y) : Dinf y ≃lm D (page r) x :=
   by symmetry; induction p; induction Hr with r Hr IH; reflexivity; exact Dstable Hr ⬝lm IH
 
+  definition Einf_isomorphism' {x : I} (r₁ : ℕ)
+    (H1 : Π⦃r⦄, r₁ ≤ r → is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+    (H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E X (deg (d (page r)) x))) :
+    Einf x ≃lm E (page r₁) x :=
+  begin
+    cases le.total r₁ (B3 x) with Hr Hr,
+    exact E_isomorphism' Hr (λr Hr₁ Hr₂, H1 Hr₁) (λr Hr₁ Hr₂, H2 Hr₁),
+    exact Einfstable Hr idp
+  end
+
+  definition Einf_isomorphism0' {x : I}
+    (H1 : Π⦃r⦄, is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+    (H2 : Π⦃r⦄, is_contr (E X (deg (d (page r)) x))) :
+    Einf x ≃lm E X x :=
+  E_isomorphism0' _ _
+
   parameters (x : I)
 
   definition r (n : ℕ) : ℕ :=
@@ -426,7 +543,6 @@ namespace left_module
     { apply ij (page (r n)) }
   end
 
-  /- the convergence theorem is a combination of the following three results -/
   definition short_exact_mod_infpage (n : ℕ) :
     short_exact_mod (Einfdiag n) (Dinfdiag n) (Dinfdiag (n+1)) :=
   begin
@@ -453,26 +569,40 @@ namespace left_module
     { reflexivity }
   end
 
+  /- the convergence theorem is the following result -/
+  definition is_built_from_infpage (bound_zero : B' (deg (k X) x) = 0) :
+    is_built_from (D X (deg (k X) x)) Einfdiag :=
+  is_built_from.mk Dinfdiag short_exact_mod_infpage (Dinfdiag0 bound_zero) (B (deg (k X) x))
+    (λs, Dinfdiag_stable)
+
   end
   end convergence_theorem
 
-  -- open convergence_theorem
-  -- print axioms short_exact_mod_infpage
-  -- print axioms Dinfdiag0
-  -- print axioms Dinfdiag_stable
-
   open int group prod convergence_theorem prod.ops
 
   definition Z2 [constructor] : Set := gℤ ×g gℤ
 
+  /- TODO: redefine/generalize converges_to so that it supports the usual indexing on ℤ × ℤ -/
   structure converges_to.{u v w} {R : Ring} (E' : gℤ → gℤ → LeftModule.{u v} R)
                                  (Dinf : gℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
-    (X : exact_couple.{u 0 v w} R Z2)
+    (X : exact_couple.{u 0 w v} R Z2)
     (HH : is_bounded X)
     (s₀ : gℤ → gℤ)
-    (p : Π(n : gℤ), is_bounded.B' HH (deg (k X) (n, s₀ n)) = 0)
-    (e : Π(x : gℤ ×g gℤ), exact_couple.E X x ≃lm E' x.1 x.2)
+    (HB : Π(n : gℤ), is_bounded.B' HH (deg (k X) (n, s₀ n)) = 0)
+    (e : Π(x : Z2), exact_couple.E X x ≃lm E' x.1 x.2)
     (f : Π(n : gℤ), exact_couple.D X (deg (k X) (n, s₀ n)) ≃lm Dinf n)
+    (deg_d1 : ℕ → gℤ) (deg_d2 : ℕ → gℤ)
+    (deg_d_eq : Π(r : ℕ) (n s : gℤ), deg (d (page X r)) (n, s) = (n + deg_d1 r, s + deg_d2 r))
+
+  structure converging_spectral_sequence.{u v w} {R : Ring} (E' : gℤ → gℤ → LeftModule.{u v} R)
+                                 (Dinf : gℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
+    (E : ℕ → graded_module.{u 0 v} R Z2)
+    (d : Π(n : ℕ), E n →gm E n)
+    (α : Π(n : ℕ) (x : Z2), E (n+1) x ≃lm graded_homology (d n) (d n) x)
+    (e : Π(n : ℕ) (x : Z2), E 0 x ≃lm E' x.1 x.2)
+    (s₀ : Z2 → ℕ)
+    (f : Π{n : ℕ} {x : Z2} (h : s₀ x ≤ n), E (s₀ x) x ≃lm E n x)
+    (HDinf : Π(n : gℤ), is_built_from (Dinf n) (λ(k : ℕ), (λx, E (s₀ x) x) (k, n - k)))
 
   infix ` ⟹ `:25 := converges_to
 
@@ -488,15 +618,43 @@ namespace left_module
   local abbreviation i := i X
   local abbreviation HH := HH c
   local abbreviation s₀ := s₀ c
-  local abbreviation Dinfdiag (n : gℤ) (k : ℕ) := Dinfdiag X HH (n, s₀ n) k
-  local abbreviation Einfdiag (n : gℤ) (k : ℕ) := Einfdiag X HH (n, s₀ n) k
+  local abbreviation Dinfdiag (n : gℤ) (k : ℕ) := Dinfdiag HH (n, s₀ n) k
+  local abbreviation Einfdiag (n : gℤ) (k : ℕ) := Einfdiag HH (n, s₀ n) k
+
+  definition deg_d_inv_eq (r : ℕ) (n s : gℤ) :
+    (deg (d (page X r)))⁻¹ᵉ (n, s) = (n - deg_d1 c r, s - deg_d2 c r) :=
+  inv_eq_of_eq (!deg_d_eq ⬝ prod_eq !sub_add_cancel !sub_add_cancel)⁻¹
 
   definition converges_to_isomorphism {E'' : gℤ → gℤ → LeftModule R} {Dinf' : graded_module R gℤ}
     (e' : Πn s, E' n s ≃lm E'' n s) (f' : Πn, Dinf n ≃lm Dinf' n) : E'' ⟹ Dinf' :=
-  converges_to.mk X HH s₀ (p c)
+  converges_to.mk X HH s₀ (HB c)
     begin intro x, induction x with n s, exact e c (n, s) ⬝lm e' n s end
     (λn, f c n ⬝lm f' n)
+    (deg_d1 c) (deg_d2 c) (λr n s, deg_d_eq c r n s)
 
+/-  definition converges_to_reindex {E'' : gℤ → gℤ → LeftModule R} {Dinf' : graded_module R gℤ}
+    (i : gℤ ×g gℤ ≃ gℤ × gℤ) (e' : Πp q, E' p q ≃lm E'' (i (p, q)).1 (i (p, q)).2)
+    (i2 : gℤ ≃ gℤ) (f' : Πn, Dinf n ≃lm Dinf' (i2 n)) :
+    (λp q, E'' p q) ⟹ λn, Dinf' n :=
+  converges_to.mk (exact_couple_reindex i X) (is_bounded_reindex i HH) s₀
+    sorry --(λn, ap (B' HH) (to_right_inv i _ ⬝ begin end) ⬝ HB c n)
+    sorry --begin intro x, induction x with p q, exact e c (p, q) ⬝lm e' p q end
+    sorry-/
+
+/-  definition converges_to_reindex_neg {E'' : gℤ → gℤ → LeftModule R} {Dinf' : graded_module R gℤ}
+    (e' : Πp q, E' p q ≃lm E'' (-p) (-q))
+    (f' : Πn, Dinf n ≃lm Dinf' (-n)) :
+    (λp q, E'' p q) ⟹ λn, Dinf' n :=
+  converges_to.mk (exact_couple_reindex (equiv_neg ×≃ equiv_neg) X) (is_bounded_reindex _ HH)
+    (λn, -s₀ (-n))
+    (λn, ap (B' HH) (begin esimp, end) ⬝ HB c n)
+    sorry --begin intro x, induction x with p q, exact e c (p, q) ⬝lm e' p q end
+    sorry-/
+
+  definition is_built_from_of_converges_to (n : ℤ) : is_built_from (Dinf n) (Einfdiag n) :=
+  is_built_from_isomorphism_left (f c n) (is_built_from_infpage HH (n, s₀ n) (HB c n))
+
+  /- TODO: reprove this using is_built_of -/
   theorem is_contr_converges_to_precise (n : gℤ)
   (H : Π(n : gℤ) (l : ℕ), is_contr (E' ((deg i)^[l] (n, s₀ n)).1 ((deg i)^[l] (n, s₀ n)).2)) :
     is_contr (Dinf n) :=
@@ -509,15 +667,41 @@ namespace left_module
       { exact is_bounded.B HH (deg (k X) (n, s₀ n)) },
       { apply Dinfdiag_stable, reflexivity },
       { intro l H,
-        exact is_contr_middle_of_short_exact_mod (short_exact_mod_infpage X HH (n, s₀ n) l)
+        exact is_contr_middle_of_short_exact_mod (short_exact_mod_infpage HH (n, s₀ n) l)
                 (H2 l) H }},
     refine @is_trunc_equiv_closed _ _ _ _ H3,
-    exact equiv_of_isomorphism (Dinfdiag0 X HH (n, s₀ n) (p c n) ⬝lm f c n)
+    exact equiv_of_isomorphism (Dinfdiag0 HH (n, s₀ n) (HB c n) ⬝lm f c n)
   end
 
   theorem is_contr_converges_to (n : gℤ) (H : Π(n s : gℤ), is_contr (E' n s)) : is_contr (Dinf n) :=
   is_contr_converges_to_precise n (λn s, !H)
 
+  definition E_isomorphism {r₁ r₂ : ℕ} {n s : gℤ} (H : r₁ ≤ r₂)
+    (H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
+    (H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
+    E (page X r₂) (n, s) ≃lm E (page X r₁) (n, s) :=
+  E_isomorphism' X H (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_inv_eq r n s)⁻¹ᵖ (H1 Hr₁ Hr₂))
+                    (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_eq c r n s)⁻¹ᵖ (H2 Hr₁ Hr₂))
+
+  definition E_isomorphism0 {r : ℕ} {n s : gℤ}
+    (H1 : Πr, is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
+    (H2 : Πr, is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
+    E (page X r) (n, s) ≃lm E' n s :=
+  E_isomorphism (zero_le r) _ _ ⬝lm e c (n, s)
+
+  definition Einf_isomorphism (r₁ : ℕ) {n s : gℤ}
+    (H1 : Π⦃r⦄, r₁ ≤ r → is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
+    (H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
+    Einf HH (n, s) ≃lm E (page X r₁) (n, s) :=
+  Einf_isomorphism' HH r₁ (λr Hr₁, transport (is_contr ∘ E X) (deg_d_inv_eq r n s)⁻¹ᵖ (H1 Hr₁))
+                         (λr Hr₁, transport (is_contr ∘ E X) (deg_d_eq c r n s)⁻¹ᵖ (H2 Hr₁))
+
+  definition Einf_isomorphism0 {n s : gℤ}
+    (H1 : Π⦃r⦄, is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
+    (H2 : Π⦃r⦄, is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
+    Einf HH (n, s) ≃lm E' n s :=
+  E_isomorphism0 _ _
+
   end
 
   variables {E' : gℤ → gℤ → AbGroup} {Dinf : gℤ → AbGroup} (c : E' ⟹ᵍ Dinf)
@@ -734,7 +918,12 @@ namespace spectrum
     { intro n, exact ub },
     { intro n, change max0 (ub - ub) = 0, exact ap max0 (sub_self ub) },
     { intro ns, reflexivity },
-    { intro n, reflexivity }
+    { intro n, reflexivity },
+    { intro r, exact - 1 },
+    { intro r, exact r + 1 },
+    { intro r n s, refine !convergence_theorem.deg_d ⬝ _,
+      refine ap (deg j_sequence) !iterate_deg_i_inv ⬝ _,
+      exact prod_eq idp (!add.assoc ⬝ ap (λx, s + (r + x)) !neg_neg) },
   end
 
   end
diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean
index 980c375..279feed 100644
--- a/algebra/submodule.hlean
+++ b/algebra/submodule.hlean
@@ -209,6 +209,7 @@ begin
   intro m, exact to_one_smul m
 end
 
+variable (S)
 definition quotient_module (S : property M) [is_submodule M S] : LeftModule R :=
 LeftModule_of_AddAbGroup (quotient_module' S) (quotient_module_smul S)
   (λr, homomorphism.addstruct (quotient_module_smul S r))
@@ -216,7 +217,7 @@ LeftModule_of_AddAbGroup (quotient_module' S) (quotient_module_smul S)
   quotient_module_mul_smul
   quotient_module_one_smul
 
-definition quotient_map [constructor] (S : property M) [is_submodule M S] : M →lm quotient_module S :=
+definition quotient_map [constructor] : M →lm quotient_module S :=
 lm_homomorphism_of_group_homomorphism (ab_qg_map _) (λr g, idp)
 
 definition quotient_map_eq_zero (m : M) (H : S m) : quotient_map S m = 0 :=
@@ -225,6 +226,7 @@ definition quotient_map_eq_zero (m : M) (H : S m) : quotient_map S m = 0 :=
 definition rel_of_quotient_map_eq_zero (m : M) (H : quotient_map S m = 0) : S m :=
 @rel_of_qg_map_eq_one _ _ (is_normal_subgroup_ab _) m H
 
+variable {S}
 definition quotient_elim [constructor] (φ : M →lm M₂) (H : Π⦃m⦄, m ∈ S → φ m = 0) :
   quotient_module S →lm M₂ :=
 lm_homomorphism_of_group_homomorphism
@@ -244,6 +246,10 @@ definition is_contr_quotient_module [instance] (S : property M) [is_submodule M
   is_contr (quotient_module S) :=
 is_contr_of_inhabited_prop 0
 
+definition rel_of_is_contr_quotient_module (S : property M) [is_submodule M S]
+  (H : is_contr (quotient_module S)) (m : M) : S m :=
+rel_of_quotient_map_eq_zero S m (@eq_of_is_contr _ H _ _)
+
 definition quotient_module_isomorphism [constructor] (S : property M) [is_submodule M S] (h : Π⦃m⦄, S m → m = 0) :
   quotient_module S ≃lm M :=
 (isomorphism.mk (quotient_map S) (is_equiv_ab_qg_map S h))⁻¹ˡᵐ
@@ -420,6 +426,32 @@ definition homology_isomorphism [constructor] (ψ : M₂ →lm M₃) (φ : M₁
 (quotient_module_isomorphism (homology_quotient_property ψ φ)
   (eq_zero_of_mem_property_submodule_trivial (image_trivial _))) ⬝lm (kernel_module_isomorphism ψ)
 
+definition ker_in_im_of_is_contr_homology (ψ : M₂ →lm M₃) {φ : M₁ →lm M₂}
+  (H₁ : is_contr (homology ψ φ)) {m : M₂} (p : ψ m = 0) : image φ m :=
+rel_of_is_contr_quotient_module _ H₁ ⟨m, p⟩
+
+definition is_embedding_of_is_contr_homology_of_constant {ψ : M₂ →lm M₃} (φ : M₁ →lm M₂)
+  (H₁ : is_contr (homology ψ φ)) (H₂ : Πm, φ m = 0) : is_embedding ψ :=
+begin
+  apply to_is_embedding_homomorphism (group_homomorphism_of_lm_homomorphism ψ),
+  intro m p, note H := rel_of_is_contr_quotient_module _ H₁ ⟨m, p⟩,
+  induction H with n q,
+  exact q⁻¹ ⬝ H₂ n
+end
+
+definition is_embedding_of_is_contr_homology_of_is_contr {ψ : M₂ →lm M₃} (φ : M₁ →lm M₂)
+  (H₁ : is_contr (homology ψ φ)) (H₂ : is_contr M₁) : is_embedding ψ :=
+is_embedding_of_is_contr_homology_of_constant φ H₁
+  (λm, ap φ (@eq_of_is_contr _ H₂ _ _) ⬝ respect_zero φ)
+
+definition is_surjective_of_is_contr_homology_of_constant (ψ : M₂ →lm M₃) {φ : M₁ →lm M₂}
+  (H₁ : is_contr (homology ψ φ)) (H₂ : Πm, ψ m = 0) : is_surjective φ :=
+λm, ker_in_im_of_is_contr_homology ψ H₁ (H₂ m)
+
+definition is_surjective_of_is_contr_homology_of_is_contr (ψ : M₂ →lm M₃) {φ : M₁ →lm M₂}
+  (H₁ : is_contr (homology ψ φ)) (H₂ : is_contr M₃) : is_surjective φ :=
+is_surjective_of_is_contr_homology_of_constant ψ H₁ (λm, @eq_of_is_contr _ H₂ _ _)
+
 -- remove:
 
 -- definition homology.rec (P : homology ψ φ → Type)
diff --git a/cohomology/basic.hlean b/cohomology/basic.hlean
index 1c4a2da..ec6bdbd 100644
--- a/cohomology/basic.hlean
+++ b/cohomology/basic.hlean
@@ -63,6 +63,7 @@ notation `upH^` n `[`:0 binders `, ` r:(scoped Y, unreduced_parametrized_cohomol
 notation `uopH^` n `[`:0 binders `, ` r:(scoped G, unreduced_ordinary_parametrized_cohomology G n) `]`:0 := r
 
 /- an alternate definition of cohomology -/
+
 definition parametrized_cohomology_isomorphism_shomotopy_group_spi {X : Type*} (Y : X → spectrum)
   {n m : ℤ} (p : -m = n) : pH^n[(x : X), Y x] ≃g πₛ[m] (spi X Y) :=
 begin
@@ -146,6 +147,14 @@ definition unreduced_cohomology_isomorphism_right (X : Type) {Y Y' : spectrum} (
   (n : ℤ) : uH^n[X, Y] ≃g uH^n[X, Y'] :=
 cohomology_isomorphism_right X₊ e n
 
+definition unreduced_ordinary_cohomology_isomorphism {X X' : Type} (f : X' ≃ X) (G : AbGroup)
+  (n : ℤ) : uoH^n[X, G] ≃g uoH^n[X', G] :=
+unreduced_cohomology_isomorphism f (EM_spectrum G) n
+
+definition unreduced_ordinary_cohomology_isomorphism_right (X : Type) {G G' : AbGroup}
+  (e : G ≃g G') (n : ℤ) : uoH^n[X, G] ≃g uoH^n[X, G'] :=
+unreduced_cohomology_isomorphism_right X (EM_spectrum_pequiv e) n
+
 definition parametrized_cohomology_isomorphism_right {X : Type*} {Y Y' : X → spectrum}
   (e : Πx n, Y x n ≃* Y' x n) (n : ℤ) : pH^n[(x : X), Y x] ≃g pH^n[(x : X), Y' x] :=
 parametrized_cohomology_isomorphism_shomotopy_group_spi Y !neg_neg ⬝g
@@ -201,6 +210,14 @@ begin
   refine is_conn.elim 0 _ _, reflexivity
 end
 
+definition cohomology_change_int (X : Type*) (Y : spectrum) {n n' : ℤ} (p : n = n') :
+  H^n[X, Y] ≃g H^n'[X, Y] :=
+isomorphism_of_eq (ap (λn, H^n[X, Y]) p)
+
+definition parametrized_cohomology_change_int (X : Type*) (Y : X → spectrum) {n n' : ℤ}
+  (p : n = n') : pH^n[(x : X), Y x] ≃g pH^n'[(x : X), Y x] :=
+isomorphism_of_eq (ap (λn, pH^n[(x : X), Y x]) p)
+
 /- suspension axiom -/
 
 definition cohomology_susp_2 (Y : spectrum) (n : ℤ) :
@@ -271,7 +288,7 @@ is_equiv_of_equiv_of_homotopy (additive_equiv H X Y n) begin intro f, induction
 /- dimension axiom for ordinary cohomology -/
 open is_conn trunc_index
 theorem EM_dimension' (G : AbGroup) (n : ℤ) (H : n ≠ 0) :
-  is_contr (ordinary_cohomology pbool G n) :=
+  is_contr (oH^n[pbool, G]) :=
 begin
   apply is_conn_equiv_closed 0 !pmap_pbool_equiv⁻¹ᵉ,
   apply is_conn_equiv_closed 0 !equiv_glue2⁻¹ᵉ,
@@ -290,10 +307,39 @@ theorem EM_dimension (G : AbGroup) (n : ℤ) (H : n ≠ 0) :
   (EM_dimension' G n H)
 
 open group algebra
-theorem ordinary_cohomology_pbool (G : AbGroup) : ordinary_cohomology pbool G 0 ≃g G :=
+theorem ordinary_cohomology_pbool (G : AbGroup) : oH^0[pbool, G] ≃g G :=
 sorry
 --isomorphism_of_equiv (trunc_equiv_trunc 0 (ppmap_pbool_pequiv _ ⬝e _)  ⬝e !trunc_equiv) sorry
 
+theorem is_contr_cohomology_of_is_contr_spectrum (n : ℤ) (X : Type*) (Y : spectrum) (H : is_contr (Y n)) :
+  is_contr (H^n[X, Y]) :=
+begin
+  apply is_trunc_trunc_of_is_trunc,
+  apply is_trunc_pmap,
+  apply is_trunc_equiv_closed_rev,
+  exact loop_pequiv_loop (loop_pequiv_loop (pequiv_ap Y (add.assoc n 1 1)⁻¹) ⬝e* (equiv_glue Y (n+1))⁻¹ᵉ*) ⬝e
+    (equiv_glue Y n)⁻¹ᵉ*
+end
+
+theorem is_contr_ordinary_cohomology (n : ℤ) (X : Type*) (G : AbGroup) (H : is_contr G) :
+  is_contr (oH^n[X, G]) :=
+begin
+  apply is_contr_cohomology_of_is_contr_spectrum,
+  exact is_contr_EM_spectrum _ _ H
+end
+
+theorem is_contr_unreduced_ordinary_cohomology (n : ℤ) (X : Type) (G : AbGroup) (H : is_contr G) :
+  is_contr (uoH^n[X, G]) :=
+is_contr_ordinary_cohomology _ _ _ H
+
+theorem is_contr_ordinary_cohomology_of_neg {n : ℤ} (X : Type*) (G : AbGroup) (H : n < 0) :
+  is_contr (oH^n[X, G]) :=
+begin
+  apply is_contr_cohomology_of_is_contr_spectrum,
+  cases n with n n, contradiction,
+  apply is_contr_EM_spectrum_neg
+end
+
 /- cohomology theory -/
 
 structure cohomology_theory.{u} : Type.{u+1} :=
diff --git a/cohomology/projective_space.hlean b/cohomology/projective_space.hlean
new file mode 100644
index 0000000..c2272f5
--- /dev/null
+++ b/cohomology/projective_space.hlean
@@ -0,0 +1,137 @@
+/- A computation of the cohomology groups of K(ℤ,2) using the Serre spectral sequence
+
+Author: Floris van Doorn-/
+
+import .serre
+
+open eq spectrum EM EM.ops int pointed cohomology left_module algebra group fiber is_equiv equiv
+     prod is_trunc function
+
+namespace temp
+
+  definition uH0_circle : uH^0[circle] ≃g gℤ :=
+  sorry
+
+  definition uH1_circle : uH^1[circle] ≃g gℤ :=
+  sorry
+
+  definition uH_circle_of_ge (n : ℤ) (h : n ≥ 2) : uH^n[circle] ≃g trivial_ab_group :=
+  sorry
+
+  definition f : unit → K agℤ 2 :=
+  λx, pt
+
+  definition fserre :
+    (λn s, uoH^-(n-s)[K agℤ 2, H^-s[circle₊]]) ⟹ᵍ (λn, H^-n[unit₊]) :=
+  proof
+  converges_to_g_isomorphism
+    (serre_convergence_map_of_is_conn pt f (EM_spectrum agℤ) 0
+      (is_strunc_EM_spectrum agℤ) (is_conn_EM agℤ 2))
+    begin
+      intro n s, apply unreduced_ordinary_cohomology_isomorphism_right,
+      apply unreduced_cohomology_isomorphism, symmetry,
+      refine !fiber_const_equiv ⬝e _,
+      refine loop_EM _ 1 ⬝e _,
+      exact EM_pequiv_circle
+    end
+    begin intro n, reflexivity end
+  qed
+
+  section
+  local notation `X`   := converges_to.X fserre
+  local notation `E∞`  := convergence_theorem.Einf (converges_to.HH fserre)
+  local notation `E∞d` := convergence_theorem.Einfdiag (converges_to.HH fserre)
+  local notation `E`   := exact_couple.E X
+
+  definition fbuilt (n : ℤ) :
+    is_built_from (LeftModule_int_of_AbGroup (H^-n[unit₊])) (E∞d (n, 0)) :=
+  is_built_from_of_converges_to fserre n
+
+  definition fEinf0 : E∞ (0, 0) ≃lm LeftModule_int_of_AbGroup agℤ :=
+  isomorphism_zero_of_is_built_from (fbuilt 0) (by reflexivity) ⬝lm
+  lm_iso_int.mk (cohomology_change_int _ _ neg_zero ⬝g
+    cohomology_isomorphism pbool_pequiv_add_point_unit _ _ ⬝g ordinary_cohomology_pbool _)
+
+  definition fEinfd (n : ℤ) (m : ℕ) (p : n ≠ 0) : is_contr (E∞d (n, 0) m) :=
+  have p' : -n ≠ 0, from λH, p (eq_zero_of_neg_eq_zero H),
+  is_contr_quotients (fbuilt n) (@(is_trunc_equiv_closed_rev -2
+    (group.equiv_of_isomorphism (cohomology_isomorphism pbool_pequiv_add_point_unit _ _)))
+    (EM_dimension' _ _ p')) _
+
+  definition fEinf (n : ℤ) (m : ℕ) (p : n ≠ 0) : is_contr (E∞ (n, -m)) :=
+  transport (is_contr ∘ E∞)
+    begin
+      induction m with m q, reflexivity, refine ap (deg (exact_couple.i X)) q ⬝ _,
+      exact prod_eq idp (neg_add m 1)⁻¹
+    end
+    (fEinfd n m p)
+
+  definition is_contr_fD (n s : ℤ) (p : s > 0) : is_contr (E (n, s)) :=
+  have is_contr H^-s[circle₊], from
+  is_contr_ordinary_cohomology_of_neg _ _ (neg_neg_of_pos p),
+  have is_contr (uoH^-(n-s)[K agℤ 2, H^-s[circle₊]]), from
+  is_contr_unreduced_ordinary_cohomology _ _ _ _,
+  @(is_contr_equiv_closed (left_module.equiv_of_isomorphism (converges_to.e fserre (n, s))⁻¹ˡᵐ))
+    this
+
+  definition is_contr_fD2 (n s : ℤ) (p : n > s) : is_contr (E (n, s)) :=
+  have -(n-s) < 0, from neg_neg_of_pos (sub_pos_of_lt p),
+  @(is_contr_equiv_closed (left_module.equiv_of_isomorphism (converges_to.e fserre (n, s))⁻¹ˡᵐ))
+    (is_contr_ordinary_cohomology_of_neg _ _ this)
+
+  definition is_contr_fD3 (n s : ℤ) (p : s ≤ - 2) : is_contr (E (n, s)) :=
+  have -s ≥ 2, from sorry, --from neg_neg_of_pos (sub_pos_of_lt p),
+  @(is_contr_equiv_closed (group.equiv_of_isomorphism (unreduced_ordinary_cohomology_isomorphism_right _ (uH_circle_of_ge _ this)⁻¹ᵍ _) ⬝e
+    left_module.equiv_of_isomorphism (converges_to.e fserre (n, s))⁻¹ˡᵐ))
+    (is_contr_ordinary_cohomology _ _ _ !is_contr_unit)
+--(unreduced_ordinary_cohomology_isomorphism_right _ _ _)
+--(is_contr_ordinary_cohomology_of_neg _ _ this)
+--(is_contr_ordinary_cohomology_of_neg _ _ this)
+  definition fE00 : E (0,0) ≃lm LeftModule_int_of_AbGroup agℤ :=
+  begin
+    refine (Einf_isomorphism fserre 0 _ _)⁻¹ˡᵐ ⬝lm fEinf0,
+    intro r H, apply is_contr_fD2, exact sub_nat_lt 0 (r+1),
+    intro r H, apply is_contr_fD, change 0 + (r + 1) >[ℤ] 0,
+    apply of_nat_lt_of_nat_of_lt,
+    apply nat.zero_lt_succ,
+  end
+
+  definition Ex0 (n : ℕ) : AddGroup_of_AddAbGroup (E (-n,0)) ≃g uH^n[K agℤ 2] :=
+  begin
+    refine group_isomorphism_of_lm_isomorphism_int (converges_to.e fserre (-n,0)) ⬝g _,
+    refine cohomology_change_int _ _ (ap neg !sub_zero ⬝ !neg_neg) ⬝g
+      unreduced_ordinary_cohomology_isomorphism_right _ uH0_circle _,
+  end
+
+  definition Ex1 (n : ℕ) : AddGroup_of_AddAbGroup (E (-(n+1),- 1)) ≃g uH^n[K agℤ 2] :=
+  begin
+    refine group_isomorphism_of_lm_isomorphism_int (converges_to.e fserre (-(n+1),- 1)) ⬝g _,
+    refine cohomology_change_int _ _ (ap neg _ ⬝ !neg_neg) ⬝g
+      unreduced_ordinary_cohomology_isomorphism_right _ !uH1_circle _,
+    exact ap (λx, x - - 1) !neg_add ⬝ !add_sub_cancel
+  end
+
+  definition uH0 : uH^0[K agℤ 2] ≃g gℤ :=
+  (Ex0 0)⁻¹ᵍ ⬝g group_isomorphism_of_lm_isomorphism_int fE00
+
+  definition fE10 : is_contr (E (- 1,0)) :=
+  begin
+    refine @(is_trunc_equiv_closed _ _) (fEinf (- 1) 0 dec_star),
+    apply equiv_of_isomorphism,
+    refine Einf_isomorphism fserre 0 _ _,
+    intro r H, --apply is_contr_fD2, change (- 1) - (- 1) >[ℤ] (- 0) - (r + 1),
+--    apply is_contr_fD, change (-0) - (r + 1) >[ℤ] 0,
+--exact sub_nat_lt 0 r,
+    -- intro r H, apply is_contr_fD, change 0 + (r + 1) >[ℤ] 0,
+    -- apply of_nat_lt_of_nat_of_lt,
+    -- apply nat.zero_lt_succ,
+  end
+
+  definition uH1 : is_contr (uH^1[K agℤ 2]) :=
+  begin
+    refine @(is_trunc_equiv_closed -2 (group.equiv_of_isomorphism !Ex0)) fE10,
+  end
+
+  end
+
+end temp
diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean
index 943c34c..e84db26 100644
--- a/cohomology/serre.hlean
+++ b/cohomology/serre.hlean
@@ -187,6 +187,12 @@ section atiyah_hirzebruch
       exact ppi_pequiv_right (λx, ptrunc_pequiv (maxm2 (s₀ + k)) (Y x k)),
     end
 
+-- set_option pp.metavar_args true
+--   definition atiyah_reindexed : (λp q, opH^p[(x : X), πₛ[q] (Y x)]) ⟹ᵍ (λn, pH^n[(x : X), Y x])
+-- :=
+--   converges_to_reindex atiyah_hirzebruch_convergence (λp q, -(p - q)) (λp q, q) (λp q, by reflexivity)
+--     (λn, -n) (λn, by reflexivity)
+
 end atiyah_hirzebruch
 
 section unreduced_atiyah_hirzebruch
diff --git a/homotopy/wedge.hlean b/homotopy/wedge.hlean
index d971bc3..2e30696 100644
--- a/homotopy/wedge.hlean
+++ b/homotopy/wedge.hlean
@@ -2,10 +2,49 @@
 
 import homotopy.wedge
 
-open wedge pushout eq prod sum pointed equiv is_equiv unit lift
+open wedge pushout eq prod sum pointed equiv is_equiv unit lift bool option
 
 namespace wedge
 
+variable (A : Type*)
+variables {A}
+
+
+definition add_point_of_wedge_pbool [unfold 2]
+  (x : A ∨ pbool) : A₊ :=
+begin
+  induction x with a b,
+  { exact some a },
+  { induction b, exact some pt, exact none },
+  { reflexivity }
+end
+
+definition wedge_pbool_of_add_point [unfold 2]
+  (x : A₊) : A ∨ pbool :=
+begin
+  induction x with a,
+  { exact inr tt },
+  { exact inl a }
+end
+
+variables (A)
+definition wedge_pbool_equiv_add_point [constructor] :
+  A ∨ pbool ≃ A₊ :=
+equiv.MK add_point_of_wedge_pbool wedge_pbool_of_add_point
+  abstract begin
+    intro x, induction x,
+    { reflexivity },
+    { reflexivity }
+  end end
+  abstract begin
+    intro x, induction x with a b,
+    { reflexivity },
+    { induction b, exact wedge.glue, reflexivity },
+    { apply eq_pathover_id_right,
+      refine ap_compose wedge_pbool_of_add_point _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
+      exact square_of_eq idp }
+  end end
+
   definition wedge_flip' [unfold 3] {A B : Type*} (x : A ∨ B) : B ∨ A :=
   begin
     induction x,
@@ -14,7 +53,6 @@ namespace wedge
     { exact (glue ⋆)⁻¹ }
   end
 
-  -- TODO: fix precedences
   definition wedge_flip [constructor] (A B : Type*) : A ∨ B →* B ∨ A :=
   pmap.mk wedge_flip' (glue ⋆)⁻¹
 
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index c7ab7ff..d5a8299 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -11,6 +11,14 @@ attribute ap010 [unfold 7]
   -- TODO: homotopy_of_eq and apd10 should be the same
   -- TODO: there is also apd10_eq_of_homotopy in both pi and eq(?)
 
+namespace algebra
+
+variables {A : Type} [add_ab_inf_group A]
+definition add_sub_cancel_middle (a b : A) : a + (b - a) = b :=
+!add.comm ⬝ !sub_add_cancel
+
+end algebra
+
 namespace eq
 
   definition apd10_prepostcompose_nondep {A B C D : Type} (h : C → D) {g g' : B → C} (p : g = g')
@@ -173,7 +181,12 @@ end eq open eq
 namespace nat
 
   protected definition rec_down (P : ℕ → Type) (s : ℕ) (H0 : P s) (Hs : Πn, P (n+1) → P n) : P 0 :=
-  have Hp : Πn, P n → P (pred n),
+  begin
+    induction s with s IH,
+    { exact H0 },
+    { exact IH (Hs s H0) }
+  end
+/-  have Hp : Πn, P n → P (pred n),
   begin
     intro n p, cases n with n,
     { exact p },
@@ -185,7 +198,16 @@ namespace nat
     { exact H0 },
     { exact Hp (s - n) p }
   end,
-  transport P (nat.sub_self s) (H s)
+  transport P (nat.sub_self s) (H s)-/
+
+  /- this generalizes iterate_commute -/
+  definition iterate_hsquare {A B : Type} {f : A → A} {g : B → B}
+    (h : A → B) (p : hsquare f g h h) (n : ℕ) : hsquare (f^[n]) (g^[n]) h h :=
+  begin
+    induction n with n q,
+      exact homotopy.rfl,
+      exact q ⬝htyh p
+  end
 
 end nat
 
@@ -299,6 +321,9 @@ namespace int
   definition sub_nat_le (n : ℤ) (m : ℕ) : n - m ≤ n :=
   le.intro !sub_add_cancel
 
+  definition sub_nat_lt (n : ℤ) (m : ℕ) : n - m < n + 1 :=
+  add_le_add_right (sub_nat_le n m) 1
+
   definition sub_one_le (n : ℤ) : n - 1 ≤ n :=
   sub_nat_le n 1
 
@@ -573,6 +598,14 @@ namespace function
   variables {A B : Type} {f f' : A → B}
   open is_conn sigma.ops
 
+  definition is_contr_of_is_surjective (f : A → B) (H : is_surjective f) (HA : is_contr A)
+    (HB : is_set B) : is_contr B :=
+  is_contr.mk (f !center) begin intro b, induction H b, exact ap f !is_prop.elim ⬝ p end
+
+  definition is_contr_of_is_embedding (f : A → B) (H : is_embedding f) (HB : is_prop B)
+    (a₀ : A) : is_contr A :=
+  is_contr.mk a₀ (λa, is_injective_of_is_embedding (is_prop.elim (f a₀) (f a)))
+
   definition merely_constant {A B : Type} (f : A → B) : Type :=
   Σb, Πa, merely (f a = b)
 
@@ -780,6 +813,10 @@ end
 
 
 namespace pointed
+
+  definition pbool_pequiv_add_point_unit [constructor] : pbool ≃* unit₊ :=
+  pequiv_of_equiv (bool_equiv_option_unit) idp
+
   definition to_homotopy_pt_mk {A B : Type*} {f g : A →* B} (h : f ~ g)
     (p : h pt ⬝ respect_pt g = respect_pt f) : to_homotopy_pt (phomotopy.mk h p) = p :=
   to_right_inv !eq_con_inv_equiv_con_eq p
@@ -839,6 +876,7 @@ end sum
 namespace prod
 
   infix ` ×→ `:63 := prod_functor
+  infix ` ×≃ `:63 := prod_equiv_prod
 
 end prod
 
diff --git a/spectrum/basic.hlean b/spectrum/basic.hlean
index 851c89d..21e73ec 100644
--- a/spectrum/basic.hlean
+++ b/spectrum/basic.hlean
@@ -908,6 +908,13 @@ namespace spectrum
     { apply is_contr_loop_of_is_contr, exact IH }
   end
 
+  definition is_contr_EM_spectrum (G : AbGroup) (n : ℤ) (H : is_contr G) : is_contr (EM_spectrum G n) :=
+  begin
+    cases n with n n,
+    { apply is_contr_EM n H },
+    { apply is_contr_EM_spectrum_neg G n }
+  end
+
   /- K(πₗ(Aₖ),l) ≃* K(πₙ(A),l) for l = n + k -/
   definition EM_type_pequiv_EM (A : spectrum) {n k : ℤ} {l : ℕ} (p : n + k = l) :
     EM_type (A k) l ≃* EM (πₛ[n] A) l :=