From b31658c2f385b0bfc765fb3265c3914ee5a933f8 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 20 Sep 2017 22:00:58 -0400
Subject: [PATCH] construct serre spectral sequence for any map

---
 cohomology/serre.hlean | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean
index 4ec0db2..8d986f0 100644
--- a/cohomology/serre.hlean
+++ b/cohomology/serre.hlean
@@ -209,7 +209,9 @@ end unreduced_atiyah_hirzebruch
 
 section serre
   universe variable u
-  variables {X : Type} (x₀ : X) (F : X → Type) {X₁ X₂ : pType.{u}} (f : X₁ →* X₂)
+  variables {X : Type} (x₀ : X) (F : X → Type)
+            {X₁ X₂ : pType.{u}} (f : X₁ →* X₂)
+            {Z₁ Z₂ : Type.{u}} (g : Z₁ → Z₂)
             (Y : spectrum) (s₀ : ℤ) (H : is_strunc s₀ Y)
 
   include H
@@ -235,6 +237,15 @@ section serre
     end
   qed
 
+  definition serre_convergence_of_map :
+    (λn s, uopH^-(n-s)[(x : Z₂), uH^-s[fiber g x, Y]]) ⟹ᵍ (λn, uH^-n[Z₁, Y]) :=
+  proof
+  converges_to_g_isomorphism
+    (serre_convergence (fiber g) Y s₀ H)
+    begin intro n s, reflexivity end
+    begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end
+  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
@@ -248,7 +259,7 @@ section serre
     (λ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)
+    (serre_convergence_of_is_conn pt (fiber f) Y s₀ H H2)
     begin intro n s, reflexivity end
     begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end
   qed