From bdf0d1bb0e548aeefb1f16117b8d0502c4f30245 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Tue, 23 May 2017 00:32:03 -0400
Subject: [PATCH] small cleanup on modules

---
 algebra/left_module.hlean         |  3 ++-
 algebra/module_exact_couple.hlean | 11 ++++++-----
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index 29727f8..a8db111 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -401,7 +401,7 @@ end
   structure short_exact_mod (A B C : LeftModule R) :=
     (f : A →lm B)
     (g : B →lm C)
-    (h : @is_short_exact _ _ (pType.mk _ 0) f g)
+    (h : @is_short_exact A B C f g)
 
   local abbreviation g_of_lm := @group_homomorphism_of_lm_homomorphism
   definition short_exact_mod_of_is_exact {X A B C Y : LeftModule R}
@@ -421,6 +421,7 @@ 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 c595e6a..bbf0c30 100644
--- a/algebra/module_exact_couple.hlean
+++ b/algebra/module_exact_couple.hlean
@@ -97,8 +97,6 @@ namespace left_module
   graded_image_elim (graded_homology_intro d d ∘gm graded_hom_lift j j_lemma1) j_lemma2
   -- degree deg j - deg i
 
-  -- mk_out_in (deg f) (deg g)
-
   lemma k_lemma1 ⦃x : I⦄ (m : E x) (p : d x m = 0) : image (i ← (deg k x)) (k x m) :=
   gmod_ker_in_im (exact_couple.ij X) (k x m) p
 
@@ -381,7 +379,7 @@ 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
 
-  parameters {x : I}
+  parameters (x : I)
 
   definition r (n : ℕ) : ℕ :=
   max (max (B (deg (j X) (deg (k X) x)) + n + 1) (B3 ((deg (i X))^[n] x)))
@@ -475,11 +473,12 @@ namespace pointed
     exact π→g[n+2] f
   end
 
-  definition homotopy_group_conn_functor : Π(n : ℤ) {A B : Type*[1]} (f : A →* B), πc[n] A →g πc[n] B
+  definition homotopy_group_conn_functor :
+    Π(n : ℤ) {A B : Type*[1]} (f : A →* B), πc[n] A →g πc[n] B
   | (of_nat n) A B f := homotopy_group_conn_nat_functor n f
   | (-[1+ n])  A B f := homomorphism_of_is_contr_right _ _
 
-  notation `π→ag'[`:95 n:0 `]`:0 := homotopy_group_conn_functor n
+  notation `π→c[`:95 n:0 `]`:0 := homotopy_group_conn_functor n
 
   section
   open prod prod.ops fiber
@@ -493,6 +492,8 @@ namespace pointed
   definition E_sequence : graded_module rℤ I :=
   λv, LeftModule_int_of_AbGroup (πc[v.2] (pconntype.mk (pfiber (f (v.1))) !Hf pt))
 
+  /- first need LES of these connected homotopy groups -/
+
   -- definition exact_couple_sequence : exact_couple rℤ I :=
   -- exact_couple.mk D_sequence E_sequence sorry sorry sorry sorry sorry sorry