From 153e48d6e50ec3e5311415a0775fb33685fa4609 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 18 May 2017 17:24:02 -0400
Subject: [PATCH] ab_image_homomorphism

---
 algebra/subgroup.hlean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index 46b8b8d..25488f5 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -392,6 +392,18 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
     exact to_respect_mul f₂ g g'
   end
 
+  definition image_homomorphism {A B C : AbGroup} (f : A →g B) (g : B →g C) :
+    ab_image f →g ab_image (g ∘g f) :=
+  begin
+    fapply image_elim,
+    exact image_lift (g ∘g f),
+    intro a p,
+    fapply subtype_eq, unfold image_lift,
+    exact calc
+      g (f a) = g 1 : by exact ap g p
+         ...  = 1   : to_respect_one,
+  end
+
   end
 
   variables {G H K : Group} {R : subgroup_rel G} {S : subgroup_rel H} {T : subgroup_rel K}