quotient_extend_unique_SES

algebra/quotient_group.hlean

@@ -243,18 +243,31 @@ namespace group
     exact K g
   end
 
+  definition ab_gelim_unique {K : subgroup_rel A} (f : A →g B) (H : Π (a :A), K a → f a = 1) (k : quotient_ab_group K →g B)
+    : ( k ∘g ab_qg_map K ~ f) → k ~ quotient_group_elim f H :=
+  begin
+    fapply gelim_unique,
+  end
+
   definition qg_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1)  :
-    is_contr (Σ(g : quotient_group N →g G'), g ∘g qg_map N = f) :=
+    is_contr (Σ(g : quotient_group N →g G'), g ∘g qg_map N ~ f) :=
   begin
     fapply is_contr.mk,
       -- give center of contraction
-    { fapply sigma.mk, exact quotient_group_elim f H, apply homomorphism_eq, exact quotient_group_compute f H },
+    { fapply sigma.mk, exact quotient_group_elim f H, exact quotient_group_compute f H },
       -- give contraction
     { intro pair, induction pair with g p, fapply sigma_eq,
-      {esimp, apply homomorphism_eq, symmetry, exact gelim_unique f H g (homotopy_of_homomorphism_eq p)},
+      {esimp, apply homomorphism_eq, symmetry, exact gelim_unique f H g p},
       {fapply is_prop.elimo} }
   end
 
+  definition ab_qg_universal_property {K : subgroup_rel A} (f : A →g B) (H : Π (a :A), K a → f a = 1) :
+  is_contr ((Σ(g : quotient_ab_group K →g B), g ∘g ab_qg_map K ~ f) ) :=
+  begin
+    fapply qg_universal_property,
+    exact H
+  end
+
 ------------------------------------------------
   -- FIRST ISOMORPHISM THEOREM
 ------------------------------------------------

algebra/ses.hlean

@@ -3,7 +3,9 @@ Copyright (c) 2017 Egbert Rijke. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Egbert Rijke
 
-Exact couple, derived couples, and so on
+Basic facts about short exact sequences. 
+
+At the moment, it only covers short exact sequences of abelian groups, but this should be extended to short exact sequences in any abelian category.
 -/
 
 import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup
@@ -38,6 +40,18 @@ definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f)
     fapply rel_of_ab_qg_map_eq_one, assumption
   end
 
+definition SES_of_subgroup {B : AbGroup} (S : subgroup_rel B) : SES (ab_subgroup S) B (quotient_ab_group S) :=
+  begin
+    fapply SES.mk,
+    exact incl_of_subgroup S,
+    exact ab_qg_map S,
+    exact is_embedding_incl_of_subgroup S,
+    exact is_surjective_ab_qg_map S,
+    fapply is_exact.mk,
+    intro a, fapply ab_qg_map_eq_one, induction a with b p, exact p,
+    intro b p, fapply tr, fapply fiber.mk, fapply sigma.mk b, fapply rel_of_ab_qg_map_eq_one, exact p, reflexivity,
+  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,
@@ -57,6 +71,15 @@ structure hom_SES {A B C A' B' C' : AbGroup} (ses : SES A B C) (ses' : SES A' B'
   ( htpy1 : hB ∘g (SES.f ses) ~ (SES.f ses') ∘g hA)
   ( htpy2 : hC ∘g (SES.g ses) ~ (SES.g ses') ∘g hB)
 
+section ses
+parameters {A B C : AbGroup} (ses : SES A B C)
+
+  local abbreviation f := SES.f ses
+  local notation `g` := SES.g ses
+  local abbreviation ex := SES.ex ses
+  local abbreviation q := ab_qg_map (kernel_subgroup g)
+  local abbreviation B_mod_A := quotient_ab_group (kernel_subgroup g)
+
 --definition quotient_SES {A B C : AbGroup} (ses : SES A B C) : 
 --  quotient_ab_group (image_subgroup (SES.f ses)) ≃g C :=
 --  begin
@@ -65,34 +88,63 @@ 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 quotient_codomain_SES {A B C : AbGroup} (ses : SES A B C) : quotient_ab_group (kernel_subgroup (SES.g ses)) ≃g C :=
+definition quotient_codomain_SES : B_mod_A ≃g C :=
   begin
-    exact (codomain_surjection_is_quotient (SES.g ses) (SES.Hg ses))
+    exact (codomain_surjection_is_quotient g (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) :=
+  local abbreviation α := quotient_codomain_SES
+
+definition quotient_triangle_SES : α ∘g q ~ g :=
   begin
     reflexivity
   end
 
-section short_exact_sequences
+definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
-  parameters {A B C A' B' C' : AbGroup} 
+  (Σ (h : C →g C'), h ∘g g ~ k) ≃ (Σ (h' : B_mod_A →g C'), h' ∘g q ~ k) :=
-  (ses : SES A B C) (ses' : SES A' B' C')  
+  begin
-  (hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g (SES.f ses) ~ (SES.f ses') ∘g hA)
+    fapply equiv.mk,
+    intro pair, induction pair with h H, 
+    fapply sigma.mk, exact h ∘g α, intro b,
+    exact H b,
+    fapply adjointify,
+    intro pair, induction pair with h' H', fapply sigma.mk,
+    exact h' ∘g α⁻¹ᵍ,
+    intro b,
+    exact calc
+      h' (α⁻¹ᵍ (g b)) = h' (α⁻¹ᵍ (α (q b))) : by reflexivity
+                  ... = h' (q b) : by exact hwhisker_left h' (left_inv α) (q b)
+                  ... = k b : by exact H' b,
+    intro pair, induction pair with h' H', fapply sigma_eq, esimp, fapply homomorphism_eq, fapply hwhisker_left h' (left_inv α),    esimp, fapply is_prop.elimo, fapply pi.is_trunc_pi, intro a, fapply is_trunc_eq,
+    intro pair, induction pair with h H, fapply sigma_eq, esimp, fapply homomorphism_eq, fapply hwhisker_left h (right_inv α),
+    esimp, fapply is_prop.elimo, fapply pi.is_trunc_pi, intro a, fapply is_trunc_eq,
+  end
+
+  parameters {A' B' C' : AbGroup} 
+  (ses' : SES A' B' C')  
+  (hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g f ~ (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 notation `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
-  local abbreviation α' := quotient_codomain_SES ses'
   
   include htpy1
 
+  definition quotient_extend_unique_SES : is_contr (Σ (hC : C →g C'), hC ∘g g ~ g' ∘g hB) := 
+  begin
+    fapply @(is_trunc_equiv_closed_rev _ (quotient_triangle_extend_SES (g' ∘g hB))), 
+    fapply ab_qg_universal_property,
+    intro b, intro 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,
+    induction p,
+    refine (ap g' (htpy1 a)) ⬝ _,
+    fapply is_exact.im_in_ker ex' (hA a)
+  end
+
+/-
   -- 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
@@ -118,13 +170,8 @@ definition right_extend_SES  : C →g C' :=
 
 local abbreviation hC := right_extend_SES
 
-definition right_extend_hom_SES : hom_SES ses ses' :=
+definition right_extend_SES_square : hC ∘g g ~ g' ∘ hB :=
   begin
-    fapply hom_SES.mk,
-    exact hA,
-    exact hB,
-    exact hC,
-    exact htpy1,
     exact calc
       hC ∘g g ~ hC ∘g α ∘g q              : by reflexivity
           ... ~ α' ∘g k ∘g α⁻¹ᵍ ∘g α ∘g q : by reflexivity
@@ -133,4 +180,36 @@ definition right_extend_hom_SES : hom_SES ses ses' :=
           ... ~ g' ∘g hB                  : by reflexivity
   end
 
-end short_exact_sequences
+local abbreviation htpy2 := right_extend_SES_square
+
+definition right_extend_SES_unique_map_aux (hC' : C →g C') (htpy2' : g' ∘g hB ~ hC' ∘g g) : k ∘g q ~  α'⁻¹ᵍ ∘g hC' ∘g α ∘g q :=
+  begin
+    exact calc
+      k ∘g q ~ q' ∘g hB                : by reflexivity
+      ... ~ α'⁻¹ᵍ ∘g α' ∘g q' ∘g hB    : by exact hwhisker_right (q' ∘g hB) (homotopy.symm (left_inv α'))
+      ... ~ α'⁻¹ᵍ ∘g g' ∘g hB          : by reflexivity
+      ... ~ α'⁻¹ᵍ ∘g hC' ∘g g          : by exact hwhisker_left (α'⁻¹ᵍ) htpy2'
+      ... ~ α'⁻¹ᵍ ∘g hC' ∘g α ∘g q     : by reflexivity
+  end
+
+definition right_extend_SES_unique_map (hC' : C →g C') (htpy2' : hC' ∘g g ~ g' ∘g hB) : hC ~ hC' :=
+  begin
+    exact calc
+      hC ~ α' ∘g k ∘g α⁻¹ᵍ : by reflexivity
+     ... ~ α' ∘g α'⁻¹ᵍ ∘g hC' ∘g α ∘g α⁻¹ᵍ : 
+     ... ~ hC' ∘g α ∘g α⁻¹ᵍ : _
+     ... ~ hC' : _
+  end
+
+definition right_extend_hom_SES : hom_SES ses ses' :=
+  begin
+    fapply hom_SES.mk,
+    exact hA,
+    exact hB,
+    exact hC,
+    exact htpy1,
+    exact htpy2
+  end
+-/
+
+end ses