proposition: Lemma abses_from_surjection {E B : AbGroup@{u}} (p : E $-> B) `{IsSurjection p} : AbSES B (ab_kernel p).
proof: Proof. srapply (Build_AbSES E _ p). 1: exact (subgroup_incl _). 1: exact _. snrapply Build_IsExact. - apply phomotopy_homotopy_hset. intros [e q]; cbn. exact q. - rapply conn_map_isequiv. Defined.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse