From 38bff9ddb4d0e68d76f12c369d376d9366e90b9d Mon Sep 17 00:00:00 2001
From: Steve Awodey <sawodey@gmail.com>
Date: Thu, 1 Jun 2017 18:01:52 -0400
Subject: [PATCH] very small additions

---
 algebra/exact_couple.hlean |  6 +++++-
 algebra/subgroup.hlean     | 14 ++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean
index 8a4c47c..4d51500 100644
--- a/algebra/exact_couple.hlean
+++ b/algebra/exact_couple.hlean
@@ -175,12 +175,16 @@ definition subgroup_iso_exact_at_A_triangle : ab_kernel_incl i ~ ab_image_incl k
 
 definition subgroup_homom_ker_to_im : ab_kernel i →g ab_image d :=
   (image_homomorphism k j) ∘g subgroup_iso_exact_at_A
+
 open eq
+
 definition left_square_derived_ses : j_factor ∘g (ab_kernel_incl i) ~ (SES.f (SES_of_differential d H)) ∘g subgroup_homom_ker_to_im :=
   begin
   intro x,
   fapply subtype_eq,
-  refine sorry --(ap (j_factor) subgroup_iso_exact_at_A_triangle) ⬝ _,
+  refine sorry 
+-- fapply ab_hom_factors_through_lift _ _ ,
+--(ap (j_factor) subgroup_iso_exact_at_A_triangle) ⬝ _,
   end
 
 /-definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC :=
diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index b2bd9b8..dac59c2 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -308,6 +308,13 @@ definition hom_lift [constructor] {G H : Group} (f : G →g H) (K : subgroup_rel
     intro g h, apply subtype_eq, esimp, apply respect_mul
   end
 
+definition hom_factors_through_lift {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : 
+f = incl_of_subgroup K ∘g hom_lift f K Hyp :=
+  begin
+  fapply homomorphism_eq,
+    reflexivity
+  end
+
 definition ab_hom_lift [constructor] {G H : AbGroup} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g ab_subgroup K :=
   begin
     fapply homomorphism.mk,
@@ -318,6 +325,13 @@ definition ab_hom_lift [constructor] {G H : AbGroup} (f : G →g H) (K : subgrou
     intro g h, apply subtype_eq, apply respect_mul,
   end
 
+definition ab_hom_factors_through_lift {G H : AbGroup} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : 
+f = incl_of_subgroup K ∘g hom_lift f K Hyp :=
+  begin
+  fapply homomorphism_eq,
+    reflexivity
+  end
+
   definition image_lift [constructor] {G H : Group} (f : G →g H) : G →g image f :=
   begin
     fapply hom_lift f,