From 200885ad2189b6d1010b5b4af77761d02925e31e Mon Sep 17 00:00:00 2001
From: Steve Awodey <sawodey@gmail.com>
Date: Fri, 7 Apr 2017 15:05:10 -0400
Subject: [PATCH] started on derived couple

---
 algebra/exact_couple.hlean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean
index 8f28d6c..eaf9e9b 100644
--- a/algebra/exact_couple.hlean
+++ b/algebra/exact_couple.hlean
@@ -26,6 +26,14 @@ definition image_subgroup_of_diff {B : AbGroup} (d : B →g B) (H : is_different
 definition homology {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup :=
   @quotient_ab_group (ab_kernel d) (image_subgroup_of_diff d H)
 
+definition SES_of_differential {B : AbGroup} (d : B →g B) (H : is_differential d) : SES (ab_image d) (ab_kernel d) (homology d H) :=
+  begin
+    fapply SES.mk,
+    sorry,
+-- use the more general fact that a subgroup inclusion is a group homomorphism
+-- maybe use SES_of_subgroup?
+  end
+
 structure exact_couple (A B : AbGroup) : Type :=
   ( i : A →g A) (j : A →g B) (k : B →g A)
   ( exact_ij : is_exact i j)