proposition: Lemma abses_cokernel_iso `{Funext} {A E B : AbGroup@{u}} (f : A $-> E) (g : GroupHomomorphism E B) `{IsSurjection g, IsExact (Tr (-1)) _ _ _ f g} : GroupIsomorphism (ab_cokernel f) B.
proof: Proof. snrapply Build_GroupIsomorphism. - snrapply (quotient_abgroup_rec _ _ g). intros e; rapply Trunc_rec; intros [a p]. refine (ap _ p^ @ _). rapply cx_isexact. - apply isequiv_surj_emb. 1: rapply cancelR_conn_map. apply isembedding_isinj_hset. srapply Quotient_ind_hprop; intro x. srapply Quotient_ind_hprop; intro y. intro p. apply qglue; cbn. refine (isexact_preimage (Tr (-1)) _ _ (-x + y) _). refine (grp_homo_op _ _ _ @ _). rewrite grp_homo_inv. apply grp_moveL_M1^-1. exact p^. Defined.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse