From f8f0157df53f1a6f1660b4659df7953cbaad3b91 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 30 Jun 2017 13:54:23 +0100
Subject: [PATCH] define ==> notation for convergence of spectral sequences

---
 algebra/left_module.hlean         |  1 -
 algebra/module_exact_couple.hlean | 64 +++++++++++++++++++++++++++++--
 move_to_lib.hlean                 | 19 +++++++++
 3 files changed, 79 insertions(+), 5 deletions(-)

diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index 0de50d3..e7eff94 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -421,7 +421,6 @@ end
       (λa, to_right_inv (equiv_of_isomorphism eB) _) (λb, to_right_inv (equiv_of_isomorphism eC) _)
       (short_exact_mod.h H))
 
-
   end
 
   end
diff --git a/algebra/module_exact_couple.hlean b/algebra/module_exact_couple.hlean
index 80c4762..cf45445 100644
--- a/algebra/module_exact_couple.hlean
+++ b/algebra/module_exact_couple.hlean
@@ -451,6 +451,52 @@ namespace left_module
   -- print axioms Dinfdiag0
   -- print axioms Dinfdiag_stable
 
+  open int group prod convergence_theorem prod.ops
+
+  definition Z2 [constructor] : Set := gℤ ×g gℤ
+
+  structure converges_to.{u v w} {R : Ring} (E' : gℤ → gℤ → LeftModule.{u v} R)
+                                 (Dinf : graded_module.{u 0 w} R gℤ) : Type.{max u (v+1) (w+1)} :=
+    (X : exact_couple.{u 0 v w} R Z2)
+    (HH : is_bounded X)
+    (e : Π(x : gℤ ×g gℤ), exact_couple.E X x ≃lm E' x.1 x.2)
+    (s₀ : gℤ)
+    (p : Π(n : gℤ), is_bounded.B' HH (deg (k X) (n, s₀)) = 0)
+    (f : Π(n : gℤ), exact_couple.D X (deg (k X) (n, s₀)) ≃lm Dinf n)
+
+  infix ` ⟹ `:25 := converges_to
+
+  definition converges_to_g [reducible] (E' : gℤ → gℤ → AbGroup) (Dinf : gℤ → AbGroup) : Type :=
+  (λn s, LeftModule_int_of_AbGroup (E' n s)) ⟹ (λn, LeftModule_int_of_AbGroup (Dinf n))
+
+  infix ` ⟹ᵍ `:25 := converges_to_g
+
+  section
+  open converges_to
+  parameters {R : Ring} {E' : gℤ → gℤ → LeftModule R} {Dinf : graded_module R gℤ} (c : E' ⟹ Dinf)
+  local abbreviation X := X c
+  local abbreviation HH := HH c
+  local abbreviation s₀ := s₀ c
+  local abbreviation Dinfdiag (n : gℤ) (k : ℕ) := Dinfdiag X HH (n, s₀) k
+  local abbreviation Einfdiag (n : gℤ) (k : ℕ) := Einfdiag X HH (n, s₀) k
+
+  include c
+
+  theorem is_contr_converges_to (H : Π(n s : gℤ), is_contr (E' n s)) (n : gℤ) : is_contr (Dinf n) :=
+  begin
+    assert H2 : Π(m : gℤ) (k : ℕ), is_contr (Einfdiag m k),
+    { intro m k, apply is_contr_E, exact is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e c _)) },
+    assert H3 : Π(m : gℤ), is_contr (Dinfdiag m 0),
+    { intro m, fapply nat.rec_down (λk, is_contr (Dinfdiag m k)),
+      { exact is_bounded.B HH (deg (k X) (m, s₀)) },
+      { apply Dinfdiag_stable, reflexivity },
+      { intro k H, exact sorry /-note zz := is_contr_middle_of_is_exact (short_exact_mod_infpage k)-/ }},
+    refine @is_trunc_equiv_closed _ _ _ _ (H3 n),
+    apply equiv_of_isomorphism,
+    exact Dinfdiag0 X HH (n, s₀) (p c n) ⬝lm f c n
+  end
+  end
+
 end left_module
 open left_module
 namespace pointed
@@ -485,8 +531,7 @@ namespace pointed
   open prod prod.ops fiber
   parameters {A : ℤ → Type*[1]} (f : Π(n : ℤ), A n →* A (n - 1)) [Hf : Πn, is_conn_fun 1 (f n)]
   include Hf
-  protected definition I [constructor] : Set := trunctype.mk (gℤ ×g gℤ) !is_trunc_prod
-  local abbreviation I := @pointed.I
+  local abbreviation I [constructor] := Z2
 
   -- definition D_sequence : graded_module rℤ I :=
   -- λv, LeftModule_int_of_AbGroup (πc[v.2] (A (v.1)))
@@ -510,8 +555,8 @@ namespace spectrum
 
   parameters {A : ℤ → spectrum} (f : Π(s : ℤ), A s →ₛ A (s - 1))
 
-  protected definition I [constructor] : Set := trunctype.mk (gℤ ×g gℤ) !is_trunc_prod
-  local abbreviation I := @spectrum.I
+--  protected definition I [constructor] : Set := gℤ ×g gℤ
+  local abbreviation I [constructor] := Z2
 
   definition D_sequence : graded_module rℤ I :=
   λv, LeftModule_int_of_AbGroup (πₛ[v.1] (A (v.2)))
@@ -652,6 +697,17 @@ namespace spectrum
       refine !add.assoc ⬝ ap (add s) !add.comm ⬝ !add.assoc⁻¹,
     end
 
+  definition converges_to_sequence : (λn s, πₛ[n] (sfiber (f s))) ⟹ᵍ (λn, πₛ[n] (A ub)) :=
+  begin
+    fapply converges_to.mk,
+    { exact exact_couple_sequence },
+    { exact is_bounded_sequence },
+    { intros, reflexivity },
+    { exact ub },
+    { intro n, change max0 (ub - ub) = 0, exact ap max0 (sub_self ub) },
+    { intro n, reflexivity }
+  end
+
   end
 
 -- Uncomment the next line to see that the proof uses univalence, but that there are no holes
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 899739a..0be4007 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -120,6 +120,25 @@ namespace eq
 
 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
+    intro n p, cases n with n,
+    { exact p },
+    { exact Hs n p }
+  end,
+  have H : Πn, P (s - n),
+  begin
+    intro n, induction n with n p,
+    { exact H0 },
+    { exact Hp (s - n) p }
+  end,
+  transport P (nat.sub_self s) (H s)
+
+end nat
+
 namespace pmap
 
   definition eta {A B : Type*} (f : A →* B) : pmap.mk f (respect_pt f) = f :=