AbelianGroup.v

Require Import Basics Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Export Classes.interfaces.canonical_names (Zero, zero, Plus).
Require Export Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative).
Require Export Algebra.Groups.Group.
Require Export Algebra.Groups.Subgroup.
Require Import Algebra.Groups.QuotientGroup.
Require Import WildCat.

Local Set Polymorphic Inductive Cumulativity.

Local Open Scope mc_scope.
Local Open Scope mc_add_scope.

(** * Abelian groups *)

(** Definition of an abelian group *)

Record AbGroup := {
  abgroup_group : Group;
  abgroup_commutative : Commutative (@group_sgop abgroup_group);
}.

Coercion abgroup_group : AbGroup >-> Group.
Global Existing Instance abgroup_commutative.

Global Instance isabgroup_abgroup {A : AbGroup} : IsAbGroup A.A: AbGroup
IsAbGroup A
Proof.A: AbGroup
IsAbGroup A
  split; exact _.
Defined.

Definition issig_abgroup : _ <~> AbGroup := ltac:(issig).

Global Instance zero_abgroup (A : AbGroup) : Zero A := group_unit.
Global Instance plus_abgroup (A : AbGroup) : Plus A := group_sgop.
Global Instance negate_abgroup (A : AbGroup) : Negate A := group_inverse.

(** ** Paths between abelian groups *)

Definition equiv_path_abgroup `{Univalence} {A B : AbGroup@{u}}
  : GroupIsomorphism A B <~> (A = B).H: Univalence
A, B: AbGroup
GroupIsomorphism A B <~> A = B
Proof.H: Univalence
A, B: AbGroup
GroupIsomorphism A B <~> A = B
  refine (equiv_ap_inv issig_abgroup _ _ oE _).H: Univalence
A, B: AbGroup
GroupIsomorphism A B <~>
issig_abgroup^-1 A = issig_abgroup^-1 B
  refine (equiv_path_sigma_hprop _ _ oE _).H: Univalence
A, B: AbGroup
GroupIsomorphism A B <~>
(issig_abgroup^-1 A).1 = (issig_abgroup^-1 B).1
  exact equiv_path_group.
Defined.

Definition equiv_path_abgroup_group `{Univalence} {A B : AbGroup}
  : (A = B :> AbGroup) <~> (A = B :> Group)
  := equiv_path_group oE equiv_path_abgroup^-1.

(** ** Subgroups of abelian groups *)

(** Subgroups of abelian groups are abelian *)
Global Instance isabgroup_subgroup (G : AbGroup) (H : Subgroup G)
  : IsAbGroup H.G: AbGroup
H: Subgroup G
IsAbGroup H
Proof.G: AbGroup
H: Subgroup G
IsAbGroup H
  nrapply Build_IsAbGroup.G: AbGroup
H: Subgroup G
IsGroup H
G: AbGroup
H: Subgroup G
Commutative sg_op
  1: exact _.G: AbGroup
H: Subgroup G
Commutative sg_op
  intros x y.G: AbGroup
H: Subgroup G
x, y: H
x + y = y + x
  apply path_sigma_hprop.G: AbGroup
H: Subgroup G
x, y: H
(x + y).1 = (y + x).1
  cbn.G: AbGroup
H: Subgroup G
x, y: H
x.1 + y.1 = y.1 + x.1 apply commutativity.
Defined.

(** Given any subgroup of an abelian group, we can coerce it to an abelian group. Note that Coq complains this coercion doesn't satisfy the uniform-inheritance condition, but in practice it works and doesn't cause any issue, so we ignore it. *)
Definition abgroup_subgroup (G : AbGroup) : Subgroup G -> AbGroup
  := fun H => Build_AbGroup H _.
#[warnings="-uniform-inheritance"]
Coercion abgroup_subgroup : Subgroup >-> AbGroup.

Global Instance isnormal_ab_subgroup (G : AbGroup) (H : Subgroup G)
  : IsNormalSubgroup H.G: AbGroup
H: Subgroup G
IsNormalSubgroup H
Proof.G: AbGroup
H: Subgroup G
IsNormalSubgroup H
  intros x y; unfold in_cosetL, in_cosetR.G: AbGroup
H: Subgroup G
x, y: G
H (- x + y) <~> H (x + - y)
  refine (_ oE equiv_subgroup_inverse _ _).G: AbGroup
H: Subgroup G
x, y: G
H (- (- x + y)) <~> H (x + - y)
  rewrite negate_sg_op.G: AbGroup
H: Subgroup G
x, y: G
H (- y + - - x) <~> H (x + - y)
  rewrite negate_involutive.G: AbGroup
H: Subgroup G
x, y: G
H (- y + x) <~> H (x + - y)
  by rewrite (commutativity (-y) x).
Defined.

(** ** Quotients of abelian groups *)

Global Instance isabgroup_quotient (G : AbGroup) (H : Subgroup G)
  : IsAbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)).G: AbGroup
H: Subgroup G
IsAbGroup
  (QuotientGroup' G H (isnormal_ab_subgroup G H))
Proof.G: AbGroup
H: Subgroup G
IsAbGroup
  (QuotientGroup' G H (isnormal_ab_subgroup G H))
  nrapply Build_IsAbGroup.G: AbGroup
H: Subgroup G
IsGroup
  (QuotientGroup' G H (isnormal_ab_subgroup G H))
G: AbGroup
H: Subgroup G
Commutative sg_op
  1: exact _.G: AbGroup
H: Subgroup G
Commutative sg_op
  intro x.G: AbGroup
H: Subgroup G
x: QuotientGroup' G H (isnormal_ab_subgroup G H)
forall
y : QuotientGroup' G H (isnormal_ab_subgroup G H),
x + y = y + x
  srapply Quotient_ind_hprop.G: AbGroup
H: Subgroup G
x: QuotientGroup' G H (isnormal_ab_subgroup G H)
forall x0 : G,
(fun
   q : G /
       in_cosetL
         {|
           normalsubgroup_subgroup := H;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup G H
         |} => x + q = q + x)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := H;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup G H
        |}) x0)
  intro y; revert x.G: AbGroup
H: Subgroup G
y: G
forall
x : QuotientGroup' G H (isnormal_ab_subgroup G H),
(fun
   q : G /
       in_cosetL
         {|
           normalsubgroup_subgroup := H;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup G H
         |} => x + q = q + x)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := H;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup G H
        |}) y)
  srapply Quotient_ind_hprop.G: AbGroup
H: Subgroup G
y: G
forall x : G,
(fun
   q : G /
       in_cosetL
         {|
           normalsubgroup_subgroup := H;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup G H
         |} =>
 (fun
    q0 : G /
         in_cosetL
           {|
             normalsubgroup_subgroup := H;
             normalsubgroup_isnormal :=
               isnormal_ab_subgroup G H
           |} => q + q0 = q0 + q)
   (class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := H;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup G H
         |}) y))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := H;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup G H
        |}) x)
  intro x.G: AbGroup
H: Subgroup G
y, x: G
(fun
   q : G /
       in_cosetL
         {|
           normalsubgroup_subgroup := H;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup G H
         |} =>
 (fun
    q0 : G /
         in_cosetL
           {|
             normalsubgroup_subgroup := H;
             normalsubgroup_isnormal :=
               isnormal_ab_subgroup G H
           |} => q + q0 = q0 + q)
   (class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := H;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup G H
         |}) y))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := H;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup G H
        |}) x)
  apply (ap (class_of _)).G: AbGroup
H: Subgroup G
y, x: G
x + y = y + x
  apply commutativity.
Defined.

Definition QuotientAbGroup (G : AbGroup) (H : Subgroup G) : AbGroup
  := (Build_AbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)) _).

Definition quotient_abgroup_rec {G : AbGroup}
  (N : Subgroup G) (H : AbGroup)
  (f : GroupHomomorphism G H) (h : forall n : G, N n -> f n = mon_unit)
  : GroupHomomorphism (QuotientAbGroup G N) H
  := grp_quotient_rec G (Build_NormalSubgroup G N _) f h.

Theorem equiv_quotient_abgroup_ump {F : Funext} {G : AbGroup}
  (N : Subgroup G) (H : Group)
  : {f : GroupHomomorphism G H & forall (n : G), N n -> f n = mon_unit}
    <~> (GroupHomomorphism (QuotientAbGroup G N) H).F: Funext
G: AbGroup
N: Subgroup G
H: Group
{f : GroupHomomorphism G H &
forall n : G, N n -> f n = mon_unit} <~>
GroupHomomorphism (QuotientAbGroup G N) H
Proof.F: Funext
G: AbGroup
N: Subgroup G
H: Group
{f : GroupHomomorphism G H &
forall n : G, N n -> f n = mon_unit} <~>
GroupHomomorphism (QuotientAbGroup G N) H
  exact (equiv_grp_quotient_ump (Build_NormalSubgroup G N _) _).
Defined.

(** ** The wild category of abelian groups *)

Global Instance isgraph_abgroup : IsGraph AbGroup
  := isgraph_induced abgroup_group.

Global Instance is01cat_abgroup : Is01Cat AbGroup
  := is01cat_induced abgroup_group.

Global Instance is01cat_grouphomomorphism {A B : AbGroup} : Is01Cat (A $-> B)
  := is01cat_induced (@grp_homo_map A B).

Global Instance is0gpd_grouphomomorphism {A B : AbGroup} : Is0Gpd (A $-> B)
  := is0gpd_induced (@grp_homo_map A B).

Global Instance is2graph_abgroup : Is2Graph AbGroup
  := is2graph_induced abgroup_group.

(** AbGroup forms a 1Cat *)
Global Instance is1cat_abgroup : Is1Cat AbGroup
  := is1cat_induced _.

Global Instance hasmorext_abgroup `{Funext} : HasMorExt AbGroup
  := hasmorext_induced _.

Global Instance hasequivs_abgroup : HasEquivs AbGroup
  := hasequivs_induced _.

(** Zero object of AbGroup *)

Definition abgroup_trivial : AbGroup.AbGroup
Proof.AbGroup
  rapply (Build_AbGroup grp_trivial).Commutative group_sgop
  by intros [].
Defined.

(** AbGroup is a pointed category *)
Global Instance ispointedcat_abgroup : IsPointedCat AbGroup.IsPointedCat AbGroup
Proof.IsPointedCat AbGroup
  apply Build_IsPointedCat with abgroup_trivial.IsInitial abgroup_trivial
IsTerminal abgroup_trivial
  all: intro A; apply ispointedcat_group.
Defined.

(** Image of group homomorphisms between abelian groups *)
Definition abgroup_image {A B : AbGroup} (f : A $-> B) : AbGroup
  := Build_AbGroup (grp_image f) _.

(** First isomorphism theorem of abelian groups *)
Definition abgroup_first_iso `{Funext} {A B : AbGroup} (f : A $-> B)
  : GroupIsomorphism (QuotientAbGroup A (grp_kernel f)) (abgroup_image f).H: Funext
A, B: AbGroup
f: A $-> B
GroupIsomorphism (QuotientAbGroup A (grp_kernel f))
  (abgroup_image f)
Proof.H: Funext
A, B: AbGroup
f: A $-> B
GroupIsomorphism (QuotientAbGroup A (grp_kernel f))
  (abgroup_image f)
  etransitivity.H: Funext
A, B: AbGroup
f: A $-> B
GroupIsomorphism (QuotientAbGroup A (grp_kernel f))
  ?Goal
H: Funext
A, B: AbGroup
f: A $-> B
GroupIsomorphism ?Goal (abgroup_image f)
  2: rapply grp_first_iso.H: Funext
A, B: AbGroup
f: A $-> B
GroupIsomorphism (QuotientAbGroup A (grp_kernel f))
  (QuotientGroup A (grp_kernel f))
  apply grp_iso_quotient_normal.
Defined.

(** ** Kernels of abelian groups *)

Definition ab_kernel {A B : AbGroup} (f : A $-> B) : AbGroup
  := Build_AbGroup (grp_kernel f) _.

(** ** Transporting in families related to abelian groups *)

Lemma transport_abgrouphomomorphism_from_const `{Univalence} {A B B' : AbGroup}
      (p : B = B') (f : GroupHomomorphism A B)
  : transport (Hom A) p f
    = grp_homo_compose (equiv_path_abgroup^-1 p) f.H: Univalence
A, B, B': AbGroup
p: B = B'
f: GroupHomomorphism A B
transport (Hom A) p f =
grp_homo_compose (equiv_path_abgroup^-1 p) f
Proof.H: Univalence
A, B, B': AbGroup
p: B = B'
f: GroupHomomorphism A B
transport (Hom A) p f =
grp_homo_compose (equiv_path_abgroup^-1 p) f
  induction p.H: Univalence
A, B: AbGroup
f: GroupHomomorphism A B
transport (Hom A) 1 f =
grp_homo_compose (equiv_path_abgroup^-1 1%path) f
  by apply equiv_path_grouphomomorphism.
Defined.

Lemma transport_iso_abgrouphomomorphism_from_const `{Univalence} {A B B' : AbGroup}
      (phi : GroupIsomorphism B B') (f : GroupHomomorphism A B)
  : transport (Hom A) (equiv_path_abgroup phi) f
    = grp_homo_compose phi f.H: Univalence
A, B, B': AbGroup
phi: GroupIsomorphism B B'
f: GroupHomomorphism A B
transport (Hom A) (equiv_path_abgroup phi) f =
grp_homo_compose phi f
Proof.H: Univalence
A, B, B': AbGroup
phi: GroupIsomorphism B B'
f: GroupHomomorphism A B
transport (Hom A) (equiv_path_abgroup phi) f =
grp_homo_compose phi f
  refine (transport_abgrouphomomorphism_from_const _ _ @ _).H: Univalence
A, B, B': AbGroup
phi: GroupIsomorphism B B'
f: GroupHomomorphism A B
grp_homo_compose
  (equiv_path_abgroup^-1 (equiv_path_abgroup phi)) f =
grp_homo_compose phi f
  by rewrite eissect.
Defined.

Lemma transport_abgrouphomomorphism_to_const `{Univalence} {A A' B : AbGroup}
      (p : A = A') (f : GroupHomomorphism A B)
  : transport (fun G => Hom G B) p f
    = grp_homo_compose f (grp_iso_inverse (equiv_path_abgroup^-1 p)).H: Univalence
A, A', B: AbGroup
p: A = A'
f: GroupHomomorphism A B
transport (fun G : AbGroup => G $-> B) p f =
grp_homo_compose f
  (grp_iso_inverse (equiv_path_abgroup^-1 p))
Proof.H: Univalence
A, A', B: AbGroup
p: A = A'
f: GroupHomomorphism A B
transport (fun G : AbGroup => G $-> B) p f =
grp_homo_compose f
  (grp_iso_inverse (equiv_path_abgroup^-1 p))
  induction p; cbn.H: Univalence
A, B: AbGroup
f: GroupHomomorphism A B
f = grp_homo_compose f (Build_GroupHomomorphism idmap)
  by apply equiv_path_grouphomomorphism.
Defined.

Lemma transport_iso_abgrouphomomorphism_to_const `{Univalence} {A A' B : AbGroup}
      (phi : GroupIsomorphism A A') (f : GroupHomomorphism A B)
  : transport (fun G => Hom G B) (equiv_path_abgroup phi) f
    = grp_homo_compose f (grp_iso_inverse phi).H: Univalence
A, A', B: AbGroup
phi: GroupIsomorphism A A'
f: GroupHomomorphism A B
transport (fun G : AbGroup => G $-> B)
  (equiv_path_abgroup phi) f =
grp_homo_compose f (grp_iso_inverse phi)
Proof.H: Univalence
A, A', B: AbGroup
phi: GroupIsomorphism A A'
f: GroupHomomorphism A B
transport (fun G : AbGroup => G $-> B)
  (equiv_path_abgroup phi) f =
grp_homo_compose f (grp_iso_inverse phi)
  refine (transport_abgrouphomomorphism_to_const _ _ @ _).H: Univalence
A, A', B: AbGroup
phi: GroupIsomorphism A A'
f: GroupHomomorphism A B
grp_homo_compose f
  (grp_iso_inverse
     (equiv_path_abgroup^-1 (equiv_path_abgroup phi))) =
grp_homo_compose f (grp_iso_inverse phi)
  by rewrite eissect.
Defined.

(** ** Operations on abelian groups *)

(** The negation automorphism of an abelian group *)
Definition ab_homo_negation {A : AbGroup} : GroupIsomorphism A A.A: AbGroup
GroupIsomorphism A A
Proof.A: AbGroup
GroupIsomorphism A A
  snrapply Build_GroupIsomorphism.A: AbGroup
GroupHomomorphism A A
A: AbGroup
IsEquiv ?grp_iso_homo
  -A: AbGroup
GroupHomomorphism A A snrapply Build_GroupHomomorphism.A: AbGroup
A -> A
A: AbGroup
IsSemiGroupPreserving ?f
    +A: AbGroup
A -> A exact (fun a => -a).
    +A: AbGroup
IsSemiGroupPreserving (fun a : A => - a) intros x y.A: AbGroup
x, y: A
- (x + y) = - x + - y
      refine (grp_inv_op x y @ _).A: AbGroup
x, y: A
- y + - x = - x + - y
      apply commutativity.
  -A: AbGroup
IsEquiv (Build_GroupHomomorphism (fun a : A => - a)) srapply isequiv_adjointify.A: AbGroup
A -> A
A: AbGroup
Build_GroupHomomorphism (fun a : A => - a) o ?g ==
idmap
A: AbGroup
?g o Build_GroupHomomorphism (fun a : A => - a) ==
idmap
    1: exact (fun a => -a).A: AbGroup
Build_GroupHomomorphism (fun a : A => - a)
o (fun a : A => - a) == idmap
A: AbGroup
(fun a : A => - a)
o Build_GroupHomomorphism (fun a : A => - a) == idmap
    1-2: exact negate_involutive.
Defined.

(** Multiplication by [n : nat] defines an endomorphism of any abelian group [A]. *)
Definition ab_mul_nat {A : AbGroup} (n : nat) : GroupHomomorphism A A.A: AbGroup
n: nat
GroupHomomorphism A A
Proof.A: AbGroup
n: nat
GroupHomomorphism A A
  snrapply Build_GroupHomomorphism.A: AbGroup
n: nat
A -> A
A: AbGroup
n: nat
IsSemiGroupPreserving ?f
  1: exact (fun a => grp_pow a n).A: AbGroup
n: nat
IsSemiGroupPreserving (fun a : A => grp_pow a n)
  intros a b.A: AbGroup
n: nat
a, b: A
grp_pow (a + b) n = grp_pow a n + grp_pow b n
  induction n; cbn.A: AbGroup
a, b: A
mon_unit = mon_unit + mon_unit
A: AbGroup
n: nat
a, b: A
IHn: grp_pow (a + b) n = grp_pow a n + grp_pow b n
a + b +
(fix F (m : nat) : A :=
   match m with
   | 0%nat => mon_unit
   | (m'.+1)%nat => a + b + F m'
   end) n =
a +
(fix F (m : nat) : A :=
   match m with
   | 0%nat => mon_unit
   | (m'.+1)%nat => a + F m'
   end) n +
(b +
 (fix F (m : nat) : A :=
    match m with
    | 0%nat => mon_unit
    | (m'.+1)%nat => b + F m'
    end) n)
  1: exact (grp_unit_l _)^.A: AbGroup
n: nat
a, b: A
IHn: grp_pow (a + b) n = grp_pow a n + grp_pow b n
a + b +
(fix F (m : nat) : A :=
   match m with
   | 0%nat => mon_unit
   | (m'.+1)%nat => a + b + F m'
   end) n =
a +
(fix F (m : nat) : A :=
   match m with
   | 0%nat => mon_unit
   | (m'.+1)%nat => a + F m'
   end) n +
(b +
 (fix F (m : nat) : A :=
    match m with
    | 0%nat => mon_unit
    | (m'.+1)%nat => b + F m'
    end) n)
  refine (_ @ associativity _ _ _).A: AbGroup
n: nat
a, b: A
IHn: grp_pow (a + b) n = grp_pow a n + grp_pow b n
a + b +
(fix F (m : nat) : A :=
   match m with
   | 0%nat => mon_unit
   | (m'.+1)%nat => a + b + F m'
   end) n =
a +
((fix F (m : nat) : A :=
    match m with
    | 0%nat => mon_unit
    | (m'.+1)%nat => a + F m'
    end) n +
 (b +
  (fix F (m : nat) : A :=
     match m with
     | 0%nat => mon_unit
     | (m'.+1)%nat => b + F m'
     end) n))
  refine (_ @ ap _ (associativity _ _ _)^).A: AbGroup
n: nat
a, b: A
IHn: grp_pow (a + b) n = grp_pow a n + grp_pow b n
a + b +
(fix F (m : nat) : A :=
   match m with
   | 0%nat => mon_unit
   | (m'.+1)%nat => a + b + F m'
   end) n =
a +
((fix F (m : nat) : A :=
    match m with
    | 0%nat => mon_unit
    | (m'.+1)%nat => a + F m'
    end) n + b +
 (fix F (m : nat) : A :=
    match m with
    | 0%nat => mon_unit
    | (m'.+1)%nat => b + F m'
    end) n)
  rewrite (commutativity (grp_pow a n) b).A: AbGroup
n: nat
a, b: A
IHn: grp_pow (a + b) n = grp_pow a n + grp_pow b n
a + b +
(fix F (m : nat) : A :=
   match m with
   | 0%nat => mon_unit
   | (m'.+1)%nat => a + b + F m'
   end) n =
a +
(b + grp_pow a n +
 (fix F (m : nat) : A :=
    match m with
    | 0%nat => mon_unit
    | (m'.+1)%nat => b + F m'
    end) n)
  refine (_ @ ap _ (associativity _ _ _)).A: AbGroup
n: nat
a, b: A
IHn: grp_pow (a + b) n = grp_pow a n + grp_pow b n
a + b +
(fix F (m : nat) : A :=
   match m with
   | 0%nat => mon_unit
   | (m'.+1)%nat => a + b + F m'
   end) n =
a +
(b +
 (grp_pow a n +
  (fix F (m : nat) : A :=
     match m with
     | 0%nat => mon_unit
     | (m'.+1)%nat => b + F m'
     end) n))
  refine (_ @ (associativity _ _ _)^).A: AbGroup
n: nat
a, b: A
IHn: grp_pow (a + b) n = grp_pow a n + grp_pow b n
a + b +
(fix F (m : nat) : A :=
   match m with
   | 0%nat => mon_unit
   | (m'.+1)%nat => a + b + F m'
   end) n =
a + b +
(grp_pow a n +
 (fix F (m : nat) : A :=
    match m with
    | 0%nat => mon_unit
    | (m'.+1)%nat => b + F m'
    end) n)
  apply grp_cancelL.A: AbGroup
n: nat
a, b: A
IHn: grp_pow (a + b) n = grp_pow a n + grp_pow b n
(fix F (m : nat) : A :=
   match m with
   | 0%nat => mon_unit
   | (m'.+1)%nat => a + b + F m'
   end) n =
grp_pow a n +
(fix F (m : nat) : A :=
   match m with
   | 0%nat => mon_unit
   | (m'.+1)%nat => b + F m'
   end) n
  assumption.
Defined.

Definition ab_mul_nat_homo {A B : AbGroup}
  (f : GroupHomomorphism A B) (n : nat)
  : f o ab_mul_nat n == ab_mul_nat n o f
  := grp_pow_homo f n.

(** The image of an inclusion is a normal subgroup. *)
Definition ab_image_embedding {A B : AbGroup} (f : A $-> B) `{IsEmbedding f} : NormalSubgroup B
  := {| normalsubgroup_subgroup := grp_image_embedding f; normalsubgroup_isnormal := _ |}.

Definition ab_image_in_embedding {A B : AbGroup} (f : A $-> B) `{IsEmbedding f}
  : GroupIsomorphism A (ab_image_embedding f)
  := grp_image_in_embedding f.

(** The cokernel of a homomorphism into an abelian group. *)
Definition ab_cokernel {G : Group@{u}} {A : AbGroup@{u}} (f : GroupHomomorphism G A)
  : AbGroup := QuotientAbGroup _ (grp_image f).

Definition ab_cokernel_embedding {G : Group} {A : AbGroup} (f : G $-> A) `{IsEmbedding f}
  : AbGroup := QuotientAbGroup _ (grp_image_embedding f).

Definition ab_cokernel_embedding_rec {G: Group} {A B : AbGroup} (f : G $-> A) `{IsEmbedding f}
  (h : A $-> B) (p : grp_homo_compose h f $== grp_homo_const)
  : ab_cokernel_embedding f $-> B.G: Group
A, B: AbGroup
f: G $-> A
IsEmbedding0: IsEmbedding f
h: A $-> B
p: grp_homo_compose h f $== grp_homo_const
ab_cokernel_embedding f $-> B
Proof.G: Group
A, B: AbGroup
f: G $-> A
IsEmbedding0: IsEmbedding f
h: A $-> B
p: grp_homo_compose h f $== grp_homo_const
ab_cokernel_embedding f $-> B
  snrapply (grp_quotient_rec _ _ h).G: Group
A, B: AbGroup
f: G $-> A
IsEmbedding0: IsEmbedding f
h: A $-> B
p: grp_homo_compose h f $== grp_homo_const
forall n : A,
{|
  normalsubgroup_subgroup := grp_image_embedding f;
  normalsubgroup_isnormal :=
    isnormal_ab_subgroup A (grp_image_embedding f)
|} n -> h n = mon_unit
  intros a [g q].G: Group
A, B: AbGroup
f: G $-> A
IsEmbedding0: IsEmbedding f
h: A $-> B
p: grp_homo_compose h f $== grp_homo_const
a: A
g: G
q: f g = a
h a = mon_unit
  induction q.G: Group
A, B: AbGroup
f: G $-> A
IsEmbedding0: IsEmbedding f
h: A $-> B
p: grp_homo_compose h f $== grp_homo_const
g: G
h (f g) = mon_unit
  exact (p g).
Defined.