Merge branch 'master' of https://github.com/cmu-phil/Spectral

algebra/.#exact_couple.hlean

@@ -0,0 +1 @@
+Steve@steveawodeysAir.wv.cc.cmu.edu.6485

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

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