proposition: Theorem groupiso_isabelianization {G : Group} (A B : AbGroup) (eta1 : GroupHomomorphism G A) (eta2 : GroupHomomorphism G B) {isab1 : IsAbelianization A eta1} {isab2 : IsAbelianization B eta2} : A ≅ B.
proof: Proof. destruct (esssurj (group_precomp B eta1) eta2) as [a ac]. destruct (esssurj (group_precomp A eta2) eta1) as [b bc]. srapply (Build_GroupIsomorphism _ _ a). srapply (isequiv_adjointify _ b). { refine (essinj (group_precomp B eta2) (x := a $o b) (y := Id (A := Group) B) _). intros x; cbn in *. refine (_ @ ac x). apply ap, bc. } { refine (essinj (group_precomp A eta1) (x := b $o a) (y := Id (A := Group) A) _). intros x; cbn in *. refine (_ @ bc x). apply ap, ac. } Defined.
imports: Basics Types Truncations.Core Cubical WildCat Colimits.Coeq Algebra.Groups.Group Algebra.AbGroups.AbelianGroup Modalities.ReflectiveSubuniverse