very small additions

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 :=

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,