derive the unparametrized serre spectral sequence

algebra/arrow_group.hlean

@@ -67,8 +67,9 @@ namespace group
     : Group.mk (trunc 0 (Π*(a : A), Ω B)) !trunc_group
       ≃g Group.mk (trunc 0 (A →* Ω B)) !trunc_group :=
   begin
-    apply trunc_isomorphism_of_equiv (pppi_equiv_pmap A (Ω B)),
-    intro h k, induction h with h h_pt, induction k with k k_pt, reflexivity
+    reflexivity,
+    -- apply trunc_isomorphism_of_equiv (pppi_equiv_pmap A (Ω B)),
+    -- intro h k, induction h with h h_pt, induction k with k k_pt, reflexivity
   end
 
   section

algebra/spectral_sequence.hlean

@@ -442,6 +442,17 @@ namespace left_module
   lemma Dinfdiag_stable {s : ℕ} (h : B (deg (k X) x) ≤ s) : is_contr (Dinfdiag s) :=
   is_contr_D _ _ (Dub !deg_iterate_ik_commute h)
 
+  /- some useful immediate properties -/
+
+  definition short_exact_mod_infpage0 (bound_zero : B' (deg (k X) x) = 0) :
+    short_exact_mod (Einfdiag 0) (D X (deg (k X) x)) (Dinfdiag 1) :=
+  begin
+    refine short_exact_mod_isomorphism _ _ _ (short_exact_mod_infpage 0),
+    { reflexivity },
+    { exact (Dinfdiag0 bound_zero)⁻¹ˡᵐ },
+    { reflexivity }
+  end
+
   end
   end convergence_theorem
 

cohomology/basic.hlean

@@ -9,13 +9,15 @@ Reduced cohomology of spectra and cohomology theories
 import ..spectrum.basic ..algebra.arrow_group ..homotopy.fwedge ..choice ..homotopy.pushout ..algebra.product_group
 
 open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc
-     function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi
+     function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi is_conn
 
 namespace cohomology
 
 /- The cohomology of X with coefficients in Y is
    trunc 0 (A →* Ω[2] (Y (n+2)))
    In the file arrow_group (in algebra) we construct the group structure on this type.
+   Equivalently, it's
+   πₛ[n] (sp_cotensor X Y)
 -/
 definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup :=
 AbGroup_trunc_pmap X (Y (n+2))
@@ -60,16 +62,7 @@ notation `opH^` n `[`:0 binders `, ` r:(scoped G, ordinary_parametrized_cohomolo
 notation `upH^` n `[`:0 binders `, ` r:(scoped Y, unreduced_parametrized_cohomology Y n) `]`:0 := r
 notation `uopH^` n `[`:0 binders `, ` r:(scoped G, unreduced_ordinary_parametrized_cohomology G n) `]`:0 := r
 
--- check H^3[S¹*,EM_spectrum agℤ]
--- check H^3[S¹*]
--- check pH^3[(x : S¹*), EM_spectrum agℤ]
-
 /- an alternate definition of cohomology -/
-definition cohomology_equiv_shomotopy_group_sp_cotensor (X : Type*) (Y : spectrum) (n : ℤ) :
-  H^n[X, Y] ≃ πₛ[-n] (sp_cotensor X Y) :=
-trunc_equiv_trunc 0 (!pfunext ⬝e loop_pequiv_loop !pfunext ⬝e loopn_pequiv_loopn 2
-  (pequiv_of_eq (ap (λn, ppmap X (Y n)) (add.comm n 2 ⬝ ap (add 2) !neg_neg⁻¹))))
-
 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
@@ -145,6 +138,14 @@ cohomology_isomorphism_shomotopy_group_sp_cotensor X Y !neg_neg ⬝g
 shomotopy_group_isomorphism_of_pequiv (-n) (λk, pequiv_ppcompose_left (e k)) ⬝g
 (cohomology_isomorphism_shomotopy_group_sp_cotensor X Y' !neg_neg)⁻¹ᵍ
 
+definition unreduced_cohomology_isomorphism {X X' : Type} (f : X' ≃ X) (Y : spectrum) (n : ℤ) :
+  uH^n[X, Y] ≃g uH^n[X', Y] :=
+cohomology_isomorphism (add_point_pequiv f) Y n
+
+definition unreduced_cohomology_isomorphism_right (X : Type) {Y Y' : spectrum} (e : Πn, Y n ≃* Y' n)
+  (n : ℤ) : uH^n[X, Y] ≃g uH^n[X, Y'] :=
+cohomology_isomorphism_right X₊ 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
@@ -178,6 +179,28 @@ parametrized_cohomology_isomorphism_right
   end
   n
 
+definition pH_isomorphism_H {X : Type*} (Y : spectrum) (n : ℤ) : pH^n[(x : X), Y] ≃g H^n[X, Y] :=
+by reflexivity
+
+definition opH_isomorphism_oH {X : Type*} (G : AbGroup) (n : ℤ) : opH^n[(x : X), G] ≃g oH^n[X, G] :=
+by reflexivity
+
+definition upH_isomorphism_uH {X : Type} (Y : spectrum) (n : ℤ) : upH^n[(x : X), Y] ≃g uH^n[X, Y] :=
+unreduced_parametrized_cohomology_isomorphism_shomotopy_group_supi _ !neg_neg ⬝g
+(unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor _ _ !neg_neg)⁻¹ᵍ
+
+definition uopH_isomorphism_uoH {X : Type} (G : AbGroup) (n : ℤ) :
+  uopH^n[(x : X), G] ≃g uoH^n[X, G] :=
+!upH_isomorphism_uH
+
+definition uopH_isomorphism_uoH_of_is_conn {X : Type*} (G : X → AbGroup) (n : ℤ) (H : is_conn 1 X) :
+  uopH^n[(x : X), G x] ≃g uoH^n[X, G pt] :=
+begin
+  refine _ ⬝g !uopH_isomorphism_uoH,
+  apply unreduced_ordinary_parametrized_cohomology_isomorphism_right,
+  refine is_conn.elim 0 _ _, reflexivity
+end
+
 /- suspension axiom -/
 
 definition cohomology_susp_2 (Y : spectrum) (n : ℤ) :

cohomology/serre.hlean

@@ -208,7 +208,9 @@ converges_to_g_isomorphism
 end unreduced_atiyah_hirzebruch
 
 section serre
-  variables {X : Type} (F : X → Type) (Y : spectrum) (s₀ : ℤ) (H : is_strunc s₀ Y)
+  universe variable u
+  variables {X : Type} (x₀ : X) (F : X → Type) {X₁ X₂ : pType.{u}} (f : X₁ →* X₂)
+            (Y : spectrum) (s₀ : ℤ) (H : is_strunc s₀ Y)
 
   include H
   definition serre_convergence :
@@ -231,7 +233,25 @@ section serre
      apply shomotopy_group_isomorphism_of_pequiv, intro k,
      exact (sigma_pumap F (Y k))⁻¹ᵉ*
     end
- qed
+  qed
+
+  definition serre_convergence_of_is_conn (H2 : is_conn 1 X) :
+    (λn s, uoH^-(n-s)[X, uH^-s[F x₀, Y]]) ⟹ᵍ (λn, uH^-n[Σ(x : X), F x, Y]) :=
+  proof
+  converges_to_g_isomorphism
+    (serre_convergence F Y s₀ H)
+    begin intro n s, exact @uopH_isomorphism_uoH_of_is_conn (pointed.MK X x₀) _ _ H2 end
+    begin intro n, reflexivity end
+  qed
+
+  definition serre_convergence_of_pmap (H2 : is_conn 1 X₂) :
+    (λn s, uoH^-(n-s)[X₂, uH^-s[pfiber f, Y]]) ⟹ᵍ (λn, uH^-n[X₁, Y]) :=
+  proof
+  converges_to_g_isomorphism
+    (serre_convergence_of_is_conn pt (λx, fiber f x) Y s₀ H H2)
+    begin intro n s, reflexivity end
+    begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end
+  qed
 
 
 end serre

pointed.hlean

@@ -215,6 +215,43 @@ namespace pointed
   definition loop_punit : Ω punit ≃* punit :=
   loop_pequiv_punit_of_is_set punit
 
+  definition add_point_functor' [unfold 4] {A B : Type} (e : A → B) (a : A₊) : B₊ :=
+  begin induction a with a, exact none, exact some (e a) end
+
+  definition add_point_functor [constructor] {A B : Type} (e : A → B) : A₊ →* B₊ :=
+  pmap.mk (add_point_functor' e) idp
+
+  definition add_point_functor_compose {A B C : Type} (f : B → C) (e : A → B) :
+    add_point_functor (f ∘ e) ~* add_point_functor f ∘* add_point_functor e :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x: reflexivity },
+    reflexivity
+  end
+
+  definition add_point_functor_id (A : Type) :
+    add_point_functor id ~* pid A₊ :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x: reflexivity },
+    reflexivity
+  end
+
+  definition add_point_functor_phomotopy {A B : Type} {e e' : A → B} (p : e ~ e') :
+    add_point_functor e ~* add_point_functor e' :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x with a, reflexivity, exact ap some (p a) },
+    reflexivity
+  end
+
+  definition add_point_pequiv {A B : Type} (e : A ≃ B) : A₊ ≃* B₊ :=
+  pequiv.MK (add_point_functor e) (add_point_functor e⁻¹ᵉ)
+    abstract !add_point_functor_compose⁻¹* ⬝* add_point_functor_phomotopy (left_inv e) ⬝*
+      !add_point_functor_id end
+    abstract !add_point_functor_compose⁻¹* ⬝* add_point_functor_phomotopy (right_inv e) ⬝*
+      !add_point_functor_id end
+
   definition add_point_over [unfold 3] {A : Type} (B : A → Type*) : A₊ → Type*
   | (some a) := B a
   | none     := plift punit