Exactness of six-term exact sequence of Ext at first spot

theories/Algebra/AbGroups/AbHom.v

@@ -1,4 +1,4 @@
-Require Import WildCat.
+Require Import WildCat HSet Truncations.
 Require Import AbelianGroup Biproduct.
 
 (** * Homomorphisms of abelian groups form an abelian group. *)
@@ -70,3 +70,17 @@ Proof.
   intros A A' f B B' g phi; cbn.
   by apply equiv_path_grouphomomorphism.
 Defined.
+
+(** ** Properties of [ab_hom] *)
+
+(** Precomposition with a surjection is an embedding. *)
+(* This could be deduced from [isembedding_precompose_surjection_hset], but relating precomposition of homomorphisms with precomposition of the underlying maps is tedious, so we give a direct proof. *)
+Global Instance isembedding_precompose_surjection_ab `{Funext} {A B C : AbGroup}
+  (f : A $-> B) `{IsSurjection f}
+  : IsEmbedding (fmap10 (A:=Group^op) ab_hom f C).
+Proof.
+  apply isembedding_isinj_hset; intros g0 g1 p.
+  apply equiv_path_grouphomomorphism.
+  rapply (conn_map_elim (Tr (-1)) f).
+  exact (equiv_path_grouphomomorphism^-1 p).
+Defined.

theories/Algebra/AbSES/SixTerm.v

@@ -9,13 +9,19 @@ Require Import WildCat HSet Pointed.Core Pointed.pTrunc Pointed.pEquiv
 
   As an application, we use the six-term exact sequence to show that [Ext Z/n A] is isomorphic to [A/n], for nonzero natural numbers [n]. (See [ext_cyclic_ab].) *)
 
-(** Exactness of [0 -> ab_hom B G -> ab_hom E G] follows from the rightmost map being an embedding, which is a consequence of [isembedding_precompose_surjection_hset] from Truncations.Core. *)
+(** Exactness of [0 -> ab_hom B G -> ab_hom E G] follows from the rightmost map being an embedding. *)
 Definition isexact_abses_sixterm_i `{Funext}
   {B A G : AbGroup} (E : AbSES B A)
   : IsExact (Tr (-1))
       (pconst : pUnit ->* ab_hom B G)
       (fmap10 (A:=Group^op) ab_hom (projection E) G).
-Abort. (* Left for future work. *)
+Proof.
+  apply isexact_purely_O.
+  rapply isexact_homotopic_i.
+  2: apply iff_grp_isexact_isembedding.
+  1: by apply phomotopy_homotopy_hset.
+  exact _. (* [isembedding_precompose_surjection_ab] *)
+Defined.
 
 (** Exactness of [ab_hom B G -> ab_hom E G -> ab_hom A G]. One can also deduce this from [isexact_abses_pullback]. *)
 Definition isexact_ext_contra_sixterm_ii `{Univalence}

theories/Algebra/Groups/ShortExactSequence.v

@@ -40,28 +40,23 @@ Local Existing Instance ishprop_phomotopy_hset.
 Local Existing Instance ishprop_isexact_hset.
 
 (** A complex 0 -> A -> B of groups is purely exact if and only if the map A -> B is an embedding. *)
-Lemma equiv_grp_isexact_isembedding `{Univalence} {A B : Group} (f : A $-> B)
-  : IsExact purely (@grp_homo_const grp_trivial A) f <~> IsEmbedding f.
+Lemma iff_grp_isexact_isembedding `{Funext} {A B : Group} (f : A $-> B)
+  : IsExact purely (@grp_homo_const grp_trivial A) f <-> IsEmbedding f.
 Proof.
-  srapply equiv_iff_hprop.
-  - intros [cx conn] b a.
-    rapply (transport IsHProp (x:= hfiber f 0)).
-    + apply path_universe_uncurried; symmetry.
-      apply equiv_grp_hfiber.
-      exact a.
-    + rapply (transport IsHProp (x:= grp_trivial)).
-      apply path_universe_uncurried.
-      rapply Build_Equiv.
+  split.
+  - intros ex b.
+    apply hprop_inhabited_contr; intro a.
+    rapply (contr_equiv' grp_trivial).
+    exact ((equiv_grp_hfiber f b a)^-1 oE pequiv_cxfib).
   - intro isemb_f.
     exists (grp_iscomplex_trivial f).
     intros y; rapply contr_inhabited_hprop.
     exists tt; apply path_ishprop.
 Defined.
 
 (** A complex 0 -> A -> B is purely exact if and only if the kernel of the map A -> B is trivial. *)
-Corollary equiv_grp_isexact_kernel `{Univalence} {A B : Group} (f : A $-> B)
+Definition equiv_grp_isexact_kernel `{Univalence} {A B : Group} (f : A $-> B)
   : IsExact purely (@grp_homo_const grp_trivial A) f
-            <~> (grp_kernel f = trivial_subgroup :> Subgroup _).
-Proof.
-  exact ((equiv_kernel_isembedding f)^-1%equiv oE equiv_grp_isexact_isembedding f).
-Defined.
+      <~> (grp_kernel f = trivial_subgroup :> Subgroup _)
+  := (equiv_kernel_isembedding f)^-1%equiv
+       oE equiv_iff_hprop_uncurried (iff_grp_isexact_isembedding f).