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

algebra/exact_couple.hlean

@@ -32,17 +32,37 @@ definition diff_im_in_ker {B : AbGroup} (d : B →g B) (H : is_differential d) :
 definition homology {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup :=
   @quotient_ab_group (ab_kernel d) (image_subgroup_of_diff d H)
 
+definition homology_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup :=
+(quotient_ab_group (image_subgroup (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H))))
+
+definition homology_iso_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : (homology d H) ≃g (homology_ugly d H) :=
+  begin
+-- fapply quotientgroupiso ...
+  exact sorry
+  end
+
+definition SES_iso_C {A B C C' : AbGroup} (ses : SES A B C) (k : C ≃g C') : SES A B C' :=
+  begin 
+  fapply SES.mk,
+  exact SES.f ses,
+  exact k ∘g SES.g ses,
+  exact SES.Hf ses,
+  fapply @is_surjective_compose _ _ _ k (SES.g ses),
+  exact is_surjective_of_is_equiv k,
+  exact SES.Hg ses,
+  fapply is_exact.mk,  
+  repeat exact sorry
+  end
+
+definition SES_of_differential_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : SES (ab_image d) (ab_kernel d) (homology_ugly d H) :=
+  begin
+    exact SES_of_inclusion (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)) (is_embedding_ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)),
+   end
+
 definition SES_of_differential {B : AbGroup} (d : B →g B) (H : is_differential d) : SES (ab_image d) (ab_kernel d) (homology d H) :=
   begin
-    fapply SES.mk,
+    exact SES_of_inclusion (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)) (is_embedding_ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)),
-    exact @ab_subgroup_of_subgroup_incl B (image_subgroup d) (kernel_subgroup d) (diff_im_in_ker d H),
+   end
-    exact ab_qg_map (image_subgroup_of_diff d H),
-    rexact is_embedding_ab_subgroup_of_subgroup_incl (diff_im_in_ker d H),
-    exact is_surjective_ab_qg_map (image_subgroup_of_diff d H),
-    fapply is_exact.mk,
-    intro b, induction b,
-    sorry,
-  end
 
 structure exact_couple (A B : AbGroup) : Type :=
   ( i : A →g A) (j : A →g B) (k : B →g A)

algebra/subgroup.hlean

@@ -284,24 +284,15 @@ namespace group
     exact H
   end
 
-  definition ab_image {G : AbGroup} {H : Group} (f : G →g H) : AbGroup :=
+definition ab_image {G : AbGroup} {H : AbGroup} (f : G →g H) : AbGroup :=
-  AbGroup_of_Group (image f)
+ ab_subgroup (image_subgroup f)
-  begin
-    intro g h,
-    induction g with x t, induction h with y s,
-    fapply subtype_eq,
-    induction t with p, induction s with q, induction p with g p, induction q with h q, induction p, induction q,
-    refine (((respect_mul f g h)⁻¹ ⬝ _) ⬝ (respect_mul f h g)),
-    apply (ap f),
-    induction G, induction struct, apply mul_comm
-  end
 
-  definition image_incl {G H : Group} (f : G →g H) : image f →g H :=
+definition image_incl {G H : Group} (f : G →g H) : image f →g H :=
     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 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 ) :=
+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,
@@ -315,14 +306,14 @@ namespace group
     reflexivity
   end
 
-  definition iso_surjection_ab_image_incl [constructor] {A B : AbGroup} (f : A →g B) (H : is_surjective f) : ab_image f ≃g B :=
+definition iso_surjection_ab_image_incl [constructor] {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 [constructor] {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g subgroup K :=
+definition hom_lift [constructor] {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g subgroup K :=
   begin
     fapply homomorphism.mk,
     intro g,