From 271459d533e1544a00e1ecf33fb069f242c9df5b Mon Sep 17 00:00:00 2001
From: Steve Awodey <sawodey@gmail.com>
Date: Thu, 26 Jan 2017 16:44:49 -0500
Subject: [PATCH 1/2] image of a surjection is the codomain

---
 algebra/.#exact_couple.hlean |  1 +
 algebra/subgroup.hlean       | 23 ++++++++++++++++++++++-
 2 files changed, 23 insertions(+), 1 deletion(-)
 create mode 120000 algebra/.#exact_couple.hlean

diff --git a/algebra/.#exact_couple.hlean b/algebra/.#exact_couple.hlean
new file mode 120000
index 0000000..852a499
--- /dev/null
+++ b/algebra/.#exact_couple.hlean
@@ -0,0 +1 @@
+Steve@steveawodeysAir.wv.cc.cmu.edu.6485
\ No newline at end of file
diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index 33e382d..532d3f2 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -281,7 +281,28 @@ namespace group
   definition image_incl {G H : Group} (f : G →g H) : image f →g H :=
     incl_of_subgroup (image_subgroup f)
 
-  definition comm_image_incl {A B : AbGroup} (f : A →g B) : ab_image f →g B := incl_of_subgroup (image_subgroup f)
+  definition ab_image_incl {A B : AbGroup} (f : A →g B) : ab_image f →g B := incl_of_subgroup (image_subgroup f)
+
+  definition is_equiv_surjection_ab_image_incl {A B : AbGroup} (f : A →g B) (H : is_surjective f) : is_equiv (ab_image_incl f ) :=
+  begin
+    fapply is_equiv.adjointify (ab_image_incl f),
+    intro b,
+    fapply sigma.mk,
+    exact b,
+    exact H b,
+    intro b,
+    reflexivity,
+    intro x,
+    apply subtype_eq,
+    reflexivity
+  end
+
+  definition iso_surjection_ab_image_incl {A B : AbGroup} (f : A →g B) (H : is_surjective f) : ab_image f ≃g B :=
+  begin
+    fapply isomorphism.mk,
+    exact (ab_image_incl f),
+    exact is_equiv_surjection_ab_image_incl f H
+  end
 
   definition hom_lift {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g subgroup K :=
   begin

From b4bdf3a77e6a9704b01db0e685629d663ee343e6 Mon Sep 17 00:00:00 2001
From: Steve Awodey <sawodey@gmail.com>
Date: Thu, 26 Jan 2017 16:55:07 -0500
Subject: [PATCH 2/2] image group

---
 algebra/quotient_group.hlean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean
index 963cd70..676fb4b 100644
--- a/algebra/quotient_group.hlean
+++ b/algebra/quotient_group.hlean
@@ -372,7 +372,7 @@ definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
     exact is_embedding_kernel_quotient_extension f
   end
 
-definition ab_group_first_iso_thm (A B : AbGroup) (f : A →g B) 
+definition ab_group_first_iso_thm {A B : AbGroup} (f : A →g B) 
            : quotient_ab_group (kernel_subgroup f) ≃g ab_image f :=
   begin
     fapply isomorphism.mk,
@@ -382,8 +382,11 @@ definition ab_group_first_iso_thm (A B : AbGroup) (f : A →g B)
     exact is_surjective_kernel_quotient_to_image f
   end
 
-
-
+definition codomain_surjection_is_quotient (A B : AbGroup) (f : A →g B)( H : is_surjective f)
+           : quotient_ab_group (kernel_subgroup f) ≃g B :=
+    begin
+     exact (ab_group_first_iso_thm f) ⬝g (iso_surjection_ab_image_incl f H)
+   end
 
 
 -- print iff.mpr