From eaf7290defa482839773c76cead5b57f624d691d Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 11 May 2017 17:25:02 -0400
Subject: [PATCH] some stuff about exact couples

---
 algebra/exact_couple.hlean | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean
index 62244f5..f3d9225 100644
--- a/algebra/exact_couple.hlean
+++ b/algebra/exact_couple.hlean
@@ -131,12 +131,20 @@ definition SES_of_exact_couple_at_i : SES (ab_kernel i) A (ab_image i) :=
   fapply ab_group_first_iso_thm i,
   end
 
+definition kj_zero (a : A) : k (j a) = 1 :=
+  begin
+    exact sorry
+  end
+
 definition j_factor : A →g (ab_kernel d) := 
 begin
   fapply ab_hom_lift j,
   intro a, 
   unfold kernel_subgroup, 
-  exact sorry --refine ap (group_fun j) _,  
+  exact calc
+    d (j a) = j (k (j a)) : rfl
+       ...  = j 1 : by exact ap j (kj_zero a)
+       ...  = 1   : to_respect_one,
 end