From 266e37d9ed3023296d996e49cacf73e53eb5195d Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 5 Oct 2018 18:01:43 -0400
Subject: [PATCH] prove some properties about first quadrant spectral sequences
 where the degree of d is as usual

---
 algebra/spectral_sequence.hlean | 32 ++++++++++++++++++++++++++++++++
 cohomology/serre.hlean          | 20 +++++++++++++++++---
 2 files changed, 49 insertions(+), 3 deletions(-)

diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean
index eb235fb..ec3bdcf 100644
--- a/algebra/spectral_sequence.hlean
+++ b/algebra/spectral_sequence.hlean
@@ -24,6 +24,7 @@ structure convergent_spectral_sequence.{u v w} {R : Ring} (E' : ℤ → ℤ →
   (lb : ℤ → ℤ)
   (HDinf : Π(n : ℤ), is_built_from (Dinf n)
                                      (λ(k : ℕ), (λx, E (s₀ x) x) (n - (k + lb n), k + lb n)))
+/- todo: the current definition doesn't say that E (s₀ x) x is contractible for x.1 + x.2 = n and x.2 < lb n -/
 
 definition convergent_spectral_sequence_g [reducible] (E' : ℤ → ℤ → AbGroup)
   (Dinf : ℤ → AbGroup) : Type :=
@@ -139,5 +140,36 @@ namespace spectral_sequence
     Einf c (n, s) ≃lm E' n s :=
   E_isomorphism0 c (λr Hr, H1 r) (λr Hr, H2 r)
 
+  /- we call a spectral sequence normal if it is a first-quadrant spectral sequence and the degree of d is what we expect -/
+  include c
+  structure is_normal : Type :=
+    (normal1 : Π{n} s, n < 0 → is_contr (E' n s))
+    (normal2 : Πn {s}, s < 0 → is_contr (E' n s))
+    (normal3 : Π(r : ℕ), deg_d c r = (r+2, -(r+1)))
+  open is_normal
+  variable {c}
+  variable (d : is_normal c)
+  include d
+  definition stable_range {n s : ℤ} {r : ℕ} (H1 : n < r + 2) (H2 : s < r + 1) :
+    Einf c (n, s) ≃lm E c r (n, s) :=
+  begin
+    fapply Einf_isomorphism,
+    { intro r' Hr', apply is_contr_E, apply normal1 d,
+      refine lt_of_le_of_lt (le_of_eq (ap (λx, n - x.1) (normal3 d r'))) _,
+      apply sub_lt_left_of_lt_add,
+      refine lt_of_lt_of_le H1 (le.trans _ (le_of_eq !add_zero⁻¹)),
+      exact add_le_add_right (of_nat_le_of_nat_of_le Hr') 2 },
+    { intro r' Hr', apply is_contr_E, apply normal2 d,
+      refine lt_of_le_of_lt (le_of_eq (ap (λx, s + x.2) (normal3 d r'))) _,
+      change s - (r' + 1) < 0,
+      apply sub_lt_left_of_lt_add,
+      refine lt_of_lt_of_le H2 (le.trans _ (le_of_eq !add_zero⁻¹)),
+      exact add_le_add_right (of_nat_le_of_nat_of_le Hr') 1 },
+  end
+  /- some properties which use the degree of the spectral sequence we construct. For the AHSS and SSS the hypothesis is by reflexivity -/
+
+
+--  definition foo
+
 
 end spectral_sequence
diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean
index e6c6ab4..64d8a8d 100644
--- a/cohomology/serre.hlean
+++ b/cohomology/serre.hlean
@@ -244,9 +244,23 @@ section atiyah_hirzebruch
   definition AHSS_deg_d (r : ℕ) :
     convergent_spectral_sequence.deg_d atiyah_hirzebruch_spectral_sequence r =
     (r + 2, -(r + 1)) :=
-  begin
-    reflexivity
-  end
+  by reflexivity
+
+  definition AHSS_lb (n : ℤ) :
+    convergent_spectral_sequence.lb atiyah_hirzebruch_spectral_sequence n = -s₀ :=
+  by reflexivity
+
+  -- open nat
+  -- definition AHSS_ub (n : ℤ) :
+  --   is_built_from.n₀ (convergent_spectral_sequence.HDinf atiyah_hirzebruch_spectral_sequence n) =
+  --   max0 (s₀ + n) + 1 :=
+  -- begin
+  --   -- refine refl (max (max0 (- - - -s₀ - (-(- -s₀ - -(s₀ - -n + -s₀) + - - -s₀) - 1)))
+  --   --   (max0 (max (s₀ + 1 - - - - -s₀) (s₀ + 1 - - - - -s₀)))) ⬝ _,
+
+  --   -- exact ap011 max (ap max0 (ap011 add (!neg_neg ⬝ !neg_neg) _)) _ ⬝ _,
+  --   exact sorry
+  -- end
 
 end atiyah_hirzebruch