SES_hom extension lemma

algebra/exact_couple.hlean

@@ -9,7 +9,7 @@ Exact couple, derived couples, and so on
 import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup
 
 open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc
-     equiv
+     equiv is_equiv
 
 structure is_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) :=
   ( im_in_ker : Π(a:A), g (f a) = 1)
@@ -22,6 +22,34 @@ structure SES (A B C : AbGroup) :=
   ( Hg : is_surjective g)
   ( ex : is_exact f g)
 
+definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f) : SES A B (quotient_ab_group (image_subgroup f)) := 
+  begin
+    have Hg : is_surjective (ab_qg_map (image_subgroup f)),
+    from is_surjective_ab_qg_map (image_subgroup f),
+    fapply SES.mk,
+    exact f,
+    exact ab_qg_map (image_subgroup f),
+    exact Hf,
+    exact Hg,
+    fapply is_exact.mk,
+    intro a,
+    fapply qg_map_eq_one, fapply tr, fapply fiber.mk, exact a, reflexivity,
+    intro b, intro p,
+    fapply rel_of_ab_qg_map_eq_one, assumption
+  end
+
+definition SES_of_surjective_map {B C : AbGroup} (g : B →g C) (Hg : is_surjective g) : SES (ab_kernel g) B C :=
+  begin
+    fapply SES.mk,
+    exact ab_kernel_incl g,
+    exact g,
+    exact is_embedding_ab_kernel_incl g,
+    exact Hg,
+    fapply is_exact.mk,
+    intro a, induction a with a p, exact p,
+    intro b p, fapply tr, fapply fiber.mk, fapply sigma.mk, exact b, exact p, reflexivity,
+  end
+
 structure hom_SES {A B C A' B' C' : AbGroup} (ses : SES A B C) (ses' : SES A' B' C') :=
   ( hA : A →g A')
   ( hB : B →g B')
@@ -37,34 +65,76 @@ structure hom_SES {A B C A' B' C' : AbGroup} (ses : SES A B C) (ses' : SES A' B'
 
 -- definition pre_right_extend_SES (to separate the following definition and replace C with B/A)
 
-definition right_extend_SES {A B C A' B' C' : AbGroup} 
-  (ses : SES A B C) (ses' : SES A' B' C')  
-  (hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g (SES.f ses) ~ (SES.f ses') ∘g hA) : C →g C' :=
+definition quotient_codomain_SES {A B C : AbGroup} (ses : SES A B C) : quotient_ab_group (kernel_subgroup (SES.g ses)) ≃g C :=
   begin
-    refine _ ∘g (codomain_surjection_is_quotient (SES.g ses) (SES.Hg ses))⁻¹ᵍ,
-    refine (codomain_surjection_is_quotient (SES.g ses') (SES.Hg ses')) ∘g _,
-    fapply ab_group_quotient_homomorphism B B' (kernel_subgroup (SES.g ses)) (kernel_subgroup (SES.g ses')) hB,
+    exact (codomain_surjection_is_quotient (SES.g ses) (SES.Hg ses))
+  end
+
+definition quotient_triangle_SES {A B C : AbGroup} (ses : SES A B C) : (quotient_codomain_SES ses) ∘g (ab_qg_map (kernel_subgroup (SES.g ses))) ~ (SES.g ses) :=
+  begin
+    reflexivity
+  end
+
+section short_exact_sequences
+  parameters {A B C A' B' C' : AbGroup} 
+  (ses : SES A B C) (ses' : SES A' B' C')  
+  (hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g (SES.f ses) ~ (SES.f ses') ∘g hA)
+
+  local abbreviation f := SES.f ses
+  local abbreviation g := SES.g ses
+  local abbreviation ex := SES.ex ses
+  local abbreviation q := ab_qg_map (kernel_subgroup g)
+  local abbreviation f' := SES.f ses'
+  local abbreviation g' := SES.g ses'
+  local abbreviation ex' := SES.ex ses'
+  local abbreviation q' := ab_qg_map (kernel_subgroup g')
+  local abbreviation α := quotient_codomain_SES ses
+  local abbreviation α' := quotient_codomain_SES ses'
+  
+  include htpy1
+
+  -- We define a group homomorphism B/ker(g) →g B'/ker(g'), keeping in mind that ker(g)=A and ker(g')=A'.
+definition quotient_extend_SES : quotient_ab_group (kernel_subgroup g) →g quotient_ab_group (kernel_subgroup g') :=
+  begin
+    fapply ab_group_quotient_homomorphism B B' (kernel_subgroup g) (kernel_subgroup g') hB,
     intro b,
     intro K,
-    have k : trunctype.carrier (image_subgroup (SES.f ses) b), from is_exact.ker_in_im (SES.ex ses) b K,
+    have k : trunctype.carrier (image_subgroup f b), from is_exact.ker_in_im ex b K,
     induction k, induction a with a p,
     rewrite [p⁻¹],
     rewrite [htpy1 a],
-    fapply is_exact.im_in_ker (SES.ex ses') (hA a), 
+    fapply is_exact.im_in_ker ex' (hA a)
   end
 
-definition right_extend_hom_SES {A B C A' B' C' : AbGroup}
-  (ses : SES A B C) (ses' : SES A' B' C')
-  (hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g (SES.f ses) ~ (SES.f ses') ∘g hA) : hom_SES ses ses' :=
+  local abbreviation k := quotient_extend_SES
+
+definition quotient_extend_SES_square : k ∘g (ab_qg_map (kernel_subgroup g)) ~ (ab_qg_map (kernel_subgroup g')) ∘g hB :=
+  begin
+    fapply quotient_group_compute
+  end
+
+definition right_extend_SES  : C →g C' := 
+  α' ∘g k ∘g α⁻¹ᵍ
+
+local abbreviation hC := right_extend_SES
+
+definition right_extend_hom_SES : hom_SES ses ses' :=
   begin
     fapply hom_SES.mk,
     exact hA,
     exact hB,
-    exact right_extend_SES ses ses' hA hB htpy1,
+    exact hC,
     exact htpy1,
-    exact sorry -- fapply quotient_group_compute,
+    exact calc
+      hC ∘g g ~ hC ∘g α ∘g q              : by reflexivity
+          ... ~ α' ∘g k ∘g α⁻¹ᵍ ∘g α ∘g q : by reflexivity
+          ... ~ α' ∘g k ∘g q              : by exact hwhisker_left (α' ∘g k) (hwhisker_right q (left_inv α))
+          ... ~ α' ∘g q' ∘g hB            : by exact hwhisker_left α' (quotient_extend_SES_square)
+          ... ~ g' ∘g hB                  : by reflexivity
   end
 
+end short_exact_sequences
+
 definition is_differential {B : AbGroup} (d : B →g B) := Π(b:B), d (d b) = 1
 
 definition image_subgroup_of_diff {B : AbGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (ab_kernel d) :=

algebra/quotient_group.hlean

@@ -195,6 +195,16 @@ namespace group
     apply rel_of_eq _ H
   end
 
+  definition rel_of_ab_qg_map_eq_one {K : subgroup_rel A} (a :A) (H : ab_qg_map K a = 1) : K a := 
+  begin
+    have e : (a * 1⁻¹ = a),
+    from calc
+      a * 1⁻¹ = a * 1 : one_inv
+        ...   = a : mul_one,
+    rewrite (inverse e),
+    apply rel_of_eq _ H
+  end
+
   definition quotient_group_elim_fun [unfold 6] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1)
     (g : quotient_group N) : G' :=
   begin

algebra/subgroup.hlean

@@ -241,6 +241,23 @@ namespace group
     intro g h, reflexivity
   end
 
+  definition is_embedding_incl_of_subgroup {G : Group} (H : subgroup_rel G) : is_embedding (incl_of_subgroup H) :=
+  begin
+    fapply function.is_embedding_of_is_injective,
+    intro h h', 
+    fapply subtype_eq
+  end
+
+  definition ab_kernel_incl {G H : AbGroup} (f : G →g H) : ab_kernel f →g G :=
+  begin
+    fapply incl_of_subgroup,
+  end
+
+  definition is_embedding_ab_kernel_incl {G H : AbGroup} (f : G →g H) : is_embedding (ab_kernel_incl f) :=
+  begin
+    fapply is_embedding_incl_of_subgroup,
+  end 
+
   definition subgroup_rel_of_subgroup {G : Group} (H1 H2 : subgroup_rel G) (hyp : Π (g : G), subgroup_rel.R H1 g → subgroup_rel.R H2 g) : subgroup_rel (subgroup H2) :=
   subgroup_rel.mk
       -- definition of the subset