Require Import Basics Types Truncations.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Cubical WildCat.
Require Import Colimits.Coeq.
Require Import Algebra.AbGroups.AbelianGroup.
Require Import Modalities.ReflectiveSubuniverse.

(** In this file we define what it means for a group homomorphism G -> H into an abelian group H to be an abelianization. We then construct an example of an abelianization. *)

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.
Local Open Scope wc_iso_scope.

(** Definition of Abelianization.

  A "unit" homomorphism [eta : G -> G_ab], with [G_ab] abelian, is considered an abelianization if and only if for all homomorphisms [G -> A], where [A] is abelian, there exists a unique [g : G_ab -> A] such that [h == g o eta X].   We express this in funext-free form by saying that precomposition with [eta] in the wild 1-category [Group] induces an equivalence of hom 0-groupoids, in the sense of WildCat/EquivGpd.

  Unfortunately, if [eta : GroupHomomorphism G G_ab] and we write [cat_precomp A eta] then Coq is unable to guess that the relevant 1-category is [Group].  Even writing [cat_precomp (A := Group) A eta] isn't good enough, I guess because the typeclass inference that finds the instance [is01cat_group] doesn't happen until after the type of [eta] would have to be resolved to a [Hom] in some wild category.  However, with the following auxiliary definition we can force the typeclass inference to happen first.  (It would be worth thinking about whether the design of the wild categories library could be improved to avoid this.)  *)
Definition group_precomp {a b} := @cat_precomp Group _ _ a b.

Class IsAbelianization {G : Group} (G_ab : AbGroup)
      (eta : GroupHomomorphism G G_ab)
  := issurjinj_isabel : forall (A : AbGroup),
      IsSurjInj (group_precomp A eta).
Global Existing Instance issurjinj_isabel.

(** Here we define abelianization as a HIT. Specifically as a set-coequalizer of the following two maps: (a, b, c) |-> a (b c) and (a, b, c) |-> a (c b).

From this we can show that Abel G is an abelian group.

In fact this models the following HIT:

HIT Abel (G : Group) := 
 | ab : G -> Abel G
 | ab_comm : forall x y z, ab (x * (y * z)) = ab (x * (z * y)).

We also derive ab and ab_comm from our coequalizer definition, and even prove the induction and computation rules for this HIT.

This HIT was suggested by Dan Christensen.
*)

Section Abel.

  (** Let G be a group. *)
  Context (G : Group).

  (** We locally define a map uncurry2 that lets us uncurry A * B * C -> D twice. *)
  Local Definition uncurry2 {A B C D : Type}
    : (A -> B -> C -> D) -> A * B * C -> D.
G: Group
A, B, C, D: Type
(A -> B -> C -> D) -> A * B * C -> D
  Proof.
G: Group
A, B, C, D: Type
(A -> B -> C -> D) -> A * B * C -> D
    intros f [[a b] c].
G: Group
A, B, C, D: Type
f: A -> B -> C -> D
a: A
b: B
c: C
D
    by apply f.
  Defined.

  (** The type Abel is defined to be the set coequalizer of the following maps G^3 -> G. *)
  Definition Abel
    := Tr 0 (Coeq
      (uncurry2 (fun a b c : G => a * (b * c)))
      (uncurry2 (fun a b c : G => a * (c * b)))).

  (** We have a natural map from G to Abel G. *)
  Definition ab : G -> Abel.
G: Group
G -> Abel
  Proof.
G: Group
G -> Abel
    intro g.
G: Group
g: G
Abel
    apply tr, coeq, g.
  Defined.

  (** This map satisfies the condition ab_comm. *)
  Definition ab_comm a b c
    : ab (a * (b * c)) = ab (a * (c * b)).
G: Group
a, b, c: G
ab (a * (b * c)) = ab (a * (c * b))
  Proof.
G: Group
a, b, c: G
ab (a * (b * c)) = ab (a * (c * b))
    apply (ap tr).
G: Group
a, b, c: G
coeq (a * (b * c)) = coeq (a * (c * b))
    exact (cglue (a, b, c)).
  Defined.

  (** It is clear that Abel is a set. *)
  Global Instance istrunc_abel : IsHSet Abel := _.

  (** We can derive the induction principle from the ones for truncation and the coequalizer. *)
  Definition Abel_ind (P : Abel -> Type) `{forall x, IsHSet (P x)} 
    (a : forall x, P (ab x)) (c : forall x y z, DPath P (ab_comm x y z)
      (a (x * (y * z))) (a (x * (z * y))))
    : forall (x : Abel), P x.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (ab x)
c: forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
forall x : Abel, P x
  Proof.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (ab x)
c: forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
forall x : Abel, P x
    srapply Trunc_ind.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (ab x)
c: forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
forall
a : Coeq (uncurry2 (fun a b c : G => a * (b * c)))
      (uncurry2 (fun a b c : G => a * (c * b))),
P (tr a)
    srapply Coeq_ind.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (ab x)
c: forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
forall a : G,
(fun
   w : Coeq
         (uncurry2 (fun a0 b c : G => a0 * (b * c)))
         (uncurry2 (fun a0 b c : G => a0 * (c * b)))
 => P (tr w)) (coeq a)
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (ab x)
c: forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
forall b : G * G * G,
transport
  (fun
     w : Coeq
           (uncurry2 (fun a b0 c : G => a * (b0 * c)))
           (uncurry2 (fun a b0 c : G => a * (c * b0)))
   => P (tr w)) (cglue b)
  (?coeq'
     (uncurry2 (fun a b0 c : G => a * (b0 * c)) b)) =
?coeq' (uncurry2 (fun a b0 c : G => a * (c * b0)) b)
    1: apply a.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (ab x)
c: forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
forall b : G * G * G,
transport
  (fun
     w : Coeq
           (uncurry2 (fun a b0 c : G => a * (b0 * c)))
           (uncurry2 (fun a b0 c : G => a * (c * b0)))
   => P (tr w)) (cglue b)
  (a (uncurry2 (fun a b0 c : G => a * (b0 * c)) b)) =
a (uncurry2 (fun a b0 c : G => a * (c * b0)) b)
    intros [[x y] z].
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (ab x)
c: forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
x, y, z: G
transport
  (fun
     w : Coeq
           (uncurry2 (fun a b c : G => a * (b * c)))
           (uncurry2 (fun a b c : G => a * (c * b)))
   => P (tr w)) (cglue (x, y, z))
  (a
     (uncurry2 (fun a b c : G => a * (b * c))
        (x, y, z))) =
a (uncurry2 (fun a b c : G => a * (c * b)) (x, y, z))
    refine (transport_compose _ _ _ _ @ _).
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (ab x)
c: forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
x, y, z: G
transport P (ap tr (cglue (x, y, z)))
  (a
     (uncurry2 (fun a b c : G => a * (b * c))
        (x, y, z))) =
a (uncurry2 (fun a b c : G => a * (c * b)) (x, y, z))
    apply c.
  Defined.

  (** The computation rule can also be proven. *)
  Definition Abel_ind_beta_ab_comm (P : Abel -> Type)
    `{forall x, IsHSet (P x)}(a : forall x, P (ab x))
    (c : forall x y z, DPath P (ab_comm x y z)
      (a (x * (y * z))) (a (x * (z * y))))
    (x y z : G) : apD (Abel_ind P a c) (ab_comm x y z) = c x y z.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (ab x)
c: forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
x, y, z: G
apD (Abel_ind P a c) (ab_comm x y z) = c x y z
  Proof.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (ab x)
c: forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
x, y, z: G
apD (Abel_ind P a c) (ab_comm x y z) = c x y z
    refine (apD_compose' tr _ _ @ ap _ _ @ concat_V_pp _ _).
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (ab x)
c: forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
x, y, z: G
apD
  (fun
     x : Coeq
           (uncurry2 (fun a b c : G => a * (b * c)))
           (uncurry2 (fun a b c : G => a * (c * b)))
   => Abel_ind P a c (tr x)) (cglue (x, y, z)) =
transport_compose P tr (cglue (x, y, z))
  (Abel_ind P a c (tr (coeq (x * (y * z))))) @ c x y z
    rapply Coeq_ind_beta_cglue.
  Defined.

  (** We also have a recursion princple. *)
  Definition Abel_rec (P : Type) `{IsHSet P} (a : G -> P)
    (c : forall x y z, a (x * (y * z)) = a (x * (z * y)))
    : Abel -> P.
G: Group
P: Type
IsHSet0: IsHSet P
a: G -> P
c: forall x y z : G,
a (x * (y * z)) = a (x * (z * y))
Abel -> P
  Proof.
G: Group
P: Type
IsHSet0: IsHSet P
a: G -> P
c: forall x y z : G,
a (x * (y * z)) = a (x * (z * y))
Abel -> P
    apply (Abel_ind _ a).
G: Group
P: Type
IsHSet0: IsHSet P
a: G -> P
c: forall x y z : G,
a (x * (y * z)) = a (x * (z * y))
forall x y z : G,
DPath (fun _ : Abel => P) (ab_comm x y z)
  (a (x * (y * z))) (a (x * (z * y)))
    intros; apply dp_const, c.
  Defined.

  (** Here is a simpler version of Abel_ind when our target is an HProp. This lets us discard all the higher paths. *)
  Definition Abel_ind_hprop (P : Abel -> Type) `{forall x, IsHProp (P x)} 
    (a : forall x, P (ab x)) : forall (x : Abel), P x.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHProp (P x)
a: forall x : G, P (ab x)
forall x : Abel, P x
  Proof.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHProp (P x)
a: forall x : G, P (ab x)
forall x : Abel, P x
    srapply (Abel_ind _ a).
G: Group
P: Abel -> Type
H: forall x : Abel, IsHProp (P x)
a: forall x : G, P (ab x)
forall x y z : G,
DPath P (ab_comm x y z) (a (x * (y * z)))
  (a (x * (z * y)))
    intros; apply path_ishprop.
  Defined.

  (** And its recursion version. *)
  Definition Abel_rec_hprop (P : Type) `{IsHProp P}
    (a : G -> P) : Abel -> P.
G: Group
P: Type
IsHProp0: IsHProp P
a: G -> P
Abel -> P
  Proof.
G: Group
P: Type
IsHProp0: IsHProp P
a: G -> P
Abel -> P
    apply (Abel_rec _ a).
G: Group
P: Type
IsHProp0: IsHProp P
a: G -> P
forall x y z : G, a (x * (y * z)) = a (x * (z * y))
    intros; apply path_ishprop.
  Defined.

End Abel.

(** The [IsHProp] argument of [Abel_ind_hprop] can usually be found by typeclass resolution, but [srapply] is slow, so we use this tactic instead. *)
Local Ltac Abel_ind_hprop x := snrapply Abel_ind_hprop; [exact _ | intro x].

(** We make sure that G is implicit in the arguments of ab and ab_comm. *)
Arguments ab {_}.
Arguments ab_comm {_}.

(** Now we can show that Abel G is in fact an abelian group. *)

Section AbelGroup.

  Context (G : Group).

  (** Firstly we derive the operation on Abel G. This is defined as follows:
        ab x + ab y := ab (x y)
      But we need to also check that it preserves ab_comm in the appropriate way. *)
  Global Instance abel_sgop : SgOp (Abel G).
G: Group
SgOp (Abel G)
  Proof.
G: Group
SgOp (Abel G)
    intro a.
G: Group
a: Abel G
Abel G -> Abel G
    srapply Abel_rec.
G: Group
a: Abel G
G -> Abel G
G: Group
a: Abel G
forall x y z : G, ?a (x * (y * z)) = ?a (x * (z * y))
    {
G: Group
a: Abel G
G -> Abel G intro b.
G: Group
a: Abel G
b: G
Abel G
      revert a.
G: Group
b: G
Abel G -> Abel G
      srapply Abel_rec.
G: Group
b: G
G -> Abel G
G: Group
b: G
forall x y z : G, ?a (x * (y * z)) = ?a (x * (z * y))
      {
G: Group
b: G
G -> Abel G intro a.
G: Group
b, a: G
Abel G
        exact (ab (a * b)). }
G: Group
b: G
forall x y z : G,
(fun a : G => ab (a * b)) (x * (y * z)) =
(fun a : G => ab (a * b)) (x * (z * y))
      intros a c d; hnf.
G: Group
b, a, c, d: G
ab (a * (c * d) * b) = ab (a * (d * c) * b)
      (* The pattern seems to be to alternate associativity and ab_comm. *)
      refine (ap _ (associativity _ _ _)^ @ _).
G: Group
b, a, c, d: G
ab (a * (c * d * b)) = ab (a * (d * c) * b)
      refine (ab_comm _ _ _ @ _).
G: Group
b, a, c, d: G
ab (a * (b * (c * d))) = ab (a * (d * c) * b)
      refine (ap _ (associativity _ _ _) @ _).
G: Group
b, a, c, d: G
ab (a * b * (c * d)) = ab (a * (d * c) * b)
      refine (ab_comm _ _ _ @ _).
G: Group
b, a, c, d: G
ab (a * b * (d * c)) = ab (a * (d * c) * b)
      refine (ap _ (associativity _ _ _)^ @ _).
G: Group
b, a, c, d: G
ab (a * (b * (d * c))) = ab (a * (d * c) * b)
      refine (ab_comm _ _ _ @ _).
G: Group
b, a, c, d: G
ab (a * (d * c * b)) = ab (a * (d * c) * b)
      refine (ap _ (associativity _ _ _)). }
G: Group
a: Abel G
forall x y z : G,
(fun b : G =>
 Abel_rec G (Abel G) (fun a : G => ab (a * b))
   (fun a c d : G =>
    ap ab (associativity a (c * d) b)^ @
    (ab_comm a (c * d) b @
     (ap ab (associativity a b (c * d)) @
      (ab_comm (a * b) c d @
       (ap ab (associativity a b (d * c))^ @
        (ab_comm a b (d * c) @
         ap ab (associativity a (d * c) b))))))
    :
    (fun a0 : G => ab (a0 * b)) (a * (c * d)) =
    (fun a0 : G => ab (a0 * b)) (a * (d * c))) a)
  (x * (y * z)) =
(fun b : G =>
 Abel_rec G (Abel G) (fun a : G => ab (a * b))
   (fun a c d : G =>
    ap ab (associativity a (c * d) b)^ @
    (ab_comm a (c * d) b @
     (ap ab (associativity a b (c * d)) @
      (ab_comm (a * b) c d @
       (ap ab (associativity a b (d * c))^ @
        (ab_comm a b (d * c) @
         ap ab (associativity a (d * c) b))))))
    :
    (fun a0 : G => ab (a0 * b)) (a * (c * d)) =
    (fun a0 : G => ab (a0 * b)) (a * (d * c))) a)
  (x * (z * y))
    intros b c d.
G: Group
a: Abel G
b, c, d: G
(fun b : G =>
 Abel_rec G (Abel G) (fun a : G => ab (a * b))
   (fun a c d : G =>
    ap ab (associativity a (c * d) b)^ @
    (ab_comm a (c * d) b @
     (ap ab (associativity a b (c * d)) @
      (ab_comm (a * b) c d @
       (ap ab (associativity a b (d * c))^ @
        (ab_comm a b (d * c) @
         ap ab (associativity a (d * c) b))))))
    :
    (fun a0 : G => ab (a0 * b)) (a * (c * d)) =
    (fun a0 : G => ab (a0 * b)) (a * (d * c))) a)
  (b * (c * d)) =
(fun b : G =>
 Abel_rec G (Abel G) (fun a : G => ab (a * b))
   (fun a c d : G =>
    ap ab (associativity a (c * d) b)^ @
    (ab_comm a (c * d) b @
     (ap ab (associativity a b (c * d)) @
      (ab_comm (a * b) c d @
       (ap ab (associativity a b (d * c))^ @
        (ab_comm a b (d * c) @
         ap ab (associativity a (d * c) b))))))
    :
    (fun a0 : G => ab (a0 * b)) (a * (c * d)) =
    (fun a0 : G => ab (a0 * b)) (a * (d * c))) a)
  (b * (d * c))
    revert a.
G: Group
b, c, d: G
forall a : Abel G,
(fun b : G =>
 Abel_rec G (Abel G) (fun a0 : G => ab (a0 * b))
   (fun a0 c d : G =>
    ap ab (associativity a0 (c * d) b)^ @
    (ab_comm a0 (c * d) b @
     (ap ab (associativity a0 b (c * d)) @
      (ab_comm (a0 * b) c d @
       (ap ab (associativity a0 b (d * c))^ @
        (ab_comm a0 b (d * c) @
         ap ab (associativity a0 (d * c) b))))))
    :
    (fun a1 : G => ab (a1 * b)) (a0 * (c * d)) =
    (fun a1 : G => ab (a1 * b)) (a0 * (d * c))) a)
  (b * (c * d)) =
(fun b : G =>
 Abel_rec G (Abel G) (fun a0 : G => ab (a0 * b))
   (fun a0 c d : G =>
    ap ab (associativity a0 (c * d) b)^ @
    (ab_comm a0 (c * d) b @
     (ap ab (associativity a0 b (c * d)) @
      (ab_comm (a0 * b) c d @
       (ap ab (associativity a0 b (d * c))^ @
        (ab_comm a0 b (d * c) @
         ap ab (associativity a0 (d * c) b))))))
    :
    (fun a1 : G => ab (a1 * b)) (a0 * (c * d)) =
    (fun a1 : G => ab (a1 * b)) (a0 * (d * c))) a)
  (b * (d * c))
    Abel_ind_hprop a; simpl.
G: Group
b, c, d, a: G
ab (a * (b * (c * d))) = ab (a * (b * (d * c)))
    refine (ap _ (associativity _ _ _) @ _).
G: Group
b, c, d, a: G
ab (a * b * (c * d)) = ab (a * (b * (d * c)))
    refine (ab_comm _ _ _ @ _).
G: Group
b, c, d, a: G
ab (a * b * (d * c)) = ab (a * (b * (d * c)))
    refine (ap _ (associativity _ _ _)^).
  Defined.

  (** We can now easily show that this operation is associative by associativity in G and the fact that being associative is a proposition. *)
  Global Instance abel_sgop_associative : Associative abel_sgop.
G: Group
Associative abel_sgop
  Proof.
G: Group
Associative abel_sgop
    intros x y.
G: Group
x, y: Abel G
forall z : Abel G,
abel_sgop x (abel_sgop y z) =
abel_sgop (abel_sgop x y) z
    Abel_ind_hprop z; revert y.
G: Group
x: Abel G
z: G
forall y : Abel G,
(fun x0 : Abel G =>
 abel_sgop x (abel_sgop y x0) =
 abel_sgop (abel_sgop x y) x0) (ab z)
    Abel_ind_hprop y; revert x.
G: Group
z, y: G
forall x : Abel G,
(fun x0 : Abel G =>
 (fun x1 : Abel G =>
  abel_sgop x (abel_sgop x0 x1) =
  abel_sgop (abel_sgop x x0) x1) (ab z)) (ab y)
    Abel_ind_hprop x; simpl.
G: Group
z, y, x: G
ab (x * (y * z)) = ab (x * y * z)
    apply ap, associativity.
  Defined.

  (** From this we know that Abel G is a semigroup. *)
  Global Instance abel_issemigroup : IsSemiGroup (Abel G) := {}.

  (** We define the unit as ab of the unit of G *)
  Global Instance abel_mon_unit : MonUnit (Abel G) := ab mon_unit.

  (** By using Abel_ind_hprop we can prove the left and right identity laws. *)
  Global Instance abel_leftidentity : LeftIdentity abel_sgop abel_mon_unit.
G: Group
LeftIdentity abel_sgop abel_mon_unit
  Proof.
G: Group
LeftIdentity abel_sgop abel_mon_unit
    Abel_ind_hprop x.
G: Group
x: G
(fun x : Abel G => abel_sgop abel_mon_unit x = x)
  (ab x)
    simpl; apply ap, left_identity.
  Defined.

  Global Instance abel_rightidentity : RightIdentity abel_sgop abel_mon_unit.
G: Group
RightIdentity abel_sgop abel_mon_unit
  Proof.
G: Group
RightIdentity abel_sgop abel_mon_unit
    Abel_ind_hprop x.
G: Group
x: G
(fun x : Abel G => abel_sgop x abel_mon_unit = x)
  (ab x)
    simpl; apply ap, right_identity.
  Defined.

  (** Hence Abel G is a monoid *)
  Global Instance ismonoid_abel : IsMonoid (Abel G) := {}.

  (** We can also prove that the operation is commutative! This will come in handy later. *)
  Global Instance abel_commutative : Commutative abel_sgop.
G: Group
Commutative abel_sgop
  Proof.
G: Group
Commutative abel_sgop
    intro x.
G: Group
x: Abel G
forall y : Abel G, abel_sgop x y = abel_sgop y x
    Abel_ind_hprop y.
G: Group
x: Abel G
y: G
(fun x0 : Abel G => abel_sgop x x0 = abel_sgop x0 x)
  (ab y)
    revert x.
G: Group
y: G
forall x : Abel G,
(fun x0 : Abel G => abel_sgop x x0 = abel_sgop x0 x)
  (ab y)
    Abel_ind_hprop x.
G: Group
y, x: G
(fun x : Abel G =>
 (fun x0 : Abel G => abel_sgop x x0 = abel_sgop x0 x)
   (ab y)) (ab x)
    refine ((ap ab (left_identity _))^ @ _).
G: Group
y, x: G
ab (mon_unit * (x * y)) = abel_sgop (ab y) (ab x)
    refine (_ @ (ap ab (left_identity _))).
G: Group
y, x: G
ab (mon_unit * (x * y)) = ab (mon_unit * (y * x))
    apply ab_comm.
  Defined.

  (** Now we can define the negation. This is just
        - (ab g) := (ab (g^-1))
      However when checking that it respects ab_comm we have to show the following:
        ab (- z * - y * - x) = ab (- y * - z * - x)
      there is no obvious way to do this, but we note that ab (x * y) is exactly the definition of ab x + ab y! Hence by commutativity we can show this. *)
  Global Instance abel_negate : Negate (Abel G).
G: Group
Negate (Abel G)
  Proof.
G: Group
Negate (Abel G)
    srapply Abel_rec.
G: Group
G -> Abel G
G: Group
forall x y z : G, ?a (x * (y * z)) = ?a (x * (z * y))
    {
G: Group
G -> Abel G intro g.
G: Group
g: G
Abel G
      exact (ab (-g)). }
G: Group
forall x y z : G,
(fun g : G => ab (- g)) (x * (y * z)) =
(fun g : G => ab (- g)) (x * (z * y))
    intros x y z; cbn.
G: Group
x, y, z: G
ab (- (x * (y * z))) = ab (- (x * (z * y)))
    rewrite ?negate_sg_op.
G: Group
x, y, z: G
ab (- z * - y * - x) = ab (- y * - z * - x)
    change (ab(- z) * ab(- y) * ab (- x) = ab (- y) * ab (- z) * ab(- x)).
G: Group
x, y, z: G
ab (- z) * ab (- y) * ab (- x) =
ab (- y) * ab (- z) * ab (- x)
    by rewrite (commutativity (ab (-z)) (ab (-y))).
  Defined.

  (** Again by Abel_ind_hprop and the corresponding laws for G we can prove the left and right inverse laws. *)
  Global Instance abel_leftinverse : LeftInverse abel_sgop abel_negate abel_mon_unit.
G: Group
LeftInverse abel_sgop abel_negate abel_mon_unit
  Proof.
G: Group
LeftInverse abel_sgop abel_negate abel_mon_unit
    Abel_ind_hprop x; simpl.
G: Group
x: G
ab (- x * x) = abel_mon_unit
    apply ap; apply left_inverse.
  Defined.

  Instance abel_rightinverse : RightInverse abel_sgop abel_negate abel_mon_unit.
G: Group
RightInverse abel_sgop abel_negate abel_mon_unit
  Proof.
G: Group
RightInverse abel_sgop abel_negate abel_mon_unit
    Abel_ind_hprop x; simpl.
G: Group
x: G
ab (x * - x) = abel_mon_unit
    apply ap; apply right_inverse.
  Defined.

  (** Thus Abel G is a group *)
  Global Instance isgroup_abel : IsGroup (Abel G) := {}.

  (** And since the operation is commutative, an abelian group. *)
  Global Instance isabgroup_abel : IsAbGroup (Abel G) := {}.

  (** By definition, the map ab is also a group homomorphism. *)
  Global Instance issemigrouppreserving_ab : IsSemiGroupPreserving ab.
G: Group
IsSemiGroupPreserving ab
  Proof.
G: Group
IsSemiGroupPreserving ab
    by unfold IsSemiGroupPreserving.
  Defined.

End AbelGroup.

(** We can easily prove that ab is a surjection. *)
Global Instance issurj_ab {G : Group} : IsSurjection (@ab G).
G: Group
IsConnMap (Tr (-1)) ab
Proof.
G: Group
IsConnMap (Tr (-1)) ab
  apply BuildIsSurjection.
G: Group
forall b : Abel G, merely (hfiber ab b)
  Abel_ind_hprop x.
G: Group
x: G
(fun x : Abel G =>
 trunctype_type (merely (hfiber ab x))) (ab x)
  cbn.
G: Group
x: G
Trunc (-1) (hfiber ab (ab x))
  apply tr.
G: Group
x: G
hfiber ab (ab x)
  exists x.
G: Group
x: G
ab x = ab x
  reflexivity.
Defined.

(** Now we finally check that our definition of abelianization satisfies the universal property of being an abelianization. *)

(** We define abel to be the abelianization of a group. This is a map from Group to AbGroup. *)
Definition abel : Group -> AbGroup.
Group -> AbGroup
Proof.
Group -> AbGroup
  intro G.
G: Group
AbGroup
  snrapply Build_AbGroup.
G: Group
Group
G: Group
Commutative group_sgop
  -
G: Group
Group srapply (Build_Group (Abel G)).
  -
G: Group
Commutative group_sgop exact _.
Defined.

(** The unit of this map is the map ab which typeclasses can pick up to be a homomorphism. We write it out explicitly here. *)
Definition abel_unit (X : Group)
  : GroupHomomorphism X (abel X).
X: Group
GroupHomomorphism X (abel X)
Proof.
X: Group
GroupHomomorphism X (abel X)
  snrapply @Build_GroupHomomorphism.
X: Group
X -> abel X
X: Group
IsSemiGroupPreserving ?f
  +
X: Group
X -> abel X exact ab.
  +
X: Group
IsSemiGroupPreserving ab exact _.
Defined.

(** Finally we can prove that our construction abel is an abelianization. *)
Global Instance isabelianization_abel {G : Group}
  : IsAbelianization (abel G) (abel_unit G).
G: Group
IsAbelianization (abel G) (abel_unit G)
Proof.
G: Group
IsAbelianization (abel G) (abel_unit G)
  intros A.
G: Group
A: AbGroup
IsSurjInj (group_precomp A (abel_unit G)) constructor.
G: Group
A: AbGroup
SplEssSurj (group_precomp A (abel_unit G))
G: Group
A: AbGroup
forall x y : abel G $-> A,
group_precomp A (abel_unit G) x $==
group_precomp A (abel_unit G) y -> x $== y
  {
G: Group
A: AbGroup
SplEssSurj (group_precomp A (abel_unit G)) intros h.
G: Group
A: AbGroup
h: G $-> A
{a : abel G $-> A &
group_precomp A (abel_unit G) a $== h} srefine (_;_).
G: Group
A: AbGroup
h: G $-> A
abel G $-> A
G: Group
A: AbGroup
h: G $-> A
(fun a : abel G $-> A =>
 group_precomp A (abel_unit G) a $== h) ?proj1
    {
G: Group
A: AbGroup
h: G $-> A
abel G $-> A snrapply @Build_GroupHomomorphism.
G: Group
A: AbGroup
h: G $-> A
abel G -> A
G: Group
A: AbGroup
h: G $-> A
IsSemiGroupPreserving ?f
      {
G: Group
A: AbGroup
h: G $-> A
abel G -> A srapply (Abel_rec _ _ h).
G: Group
A: AbGroup
h: G $-> A
forall x y z : G, h (x * (y * z)) = h (x * (z * y))
        intros x y z.
G: Group
A: AbGroup
h: G $-> A
x, y, z: G
h (x * (y * z)) = h (x * (z * y))
        refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
G: Group
A: AbGroup
h: G $-> A
x, y, z: G
h x * h (y * z) = h x * h (z * y)
        apply (ap (_ *.)).
G: Group
A: AbGroup
h: G $-> A
x, y, z: G
h (y * z) = h (z * y)
        refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
G: Group
A: AbGroup
h: G $-> A
x, y, z: G
h y * h z = h z * h y
        apply commutativity. }
G: Group
A: AbGroup
h: G $-> A
IsSemiGroupPreserving
  (Abel_rec G A h
     (fun x y z : G =>
      (grp_homo_op h x (y * z) @
       ap (sg_op (h x))
         ((grp_homo_op h y z @
           commutativity (h y) (h z)) @
          (grp_homo_op h z y)^)) @
      (grp_homo_op h x (z * y))^))
      intros y.
G: Group
A: AbGroup
h: G $-> A
y: abel G
forall y0 : abel G,
Abel_rec G A h
  (fun x y z : G =>
   (grp_homo_op h x (y * z) @
    ap (sg_op (h x))
      ((grp_homo_op h y z @ commutativity (h y) (h z)) @
       (grp_homo_op h z y)^)) @
   (grp_homo_op h x (z * y))^) (y * y0) =
Abel_rec G A h
  (fun x y z : G =>
   (grp_homo_op h x (y * z) @
    ap (sg_op (h x))
      ((grp_homo_op h y z @ commutativity (h y) (h z)) @
       (grp_homo_op h z y)^)) @
   (grp_homo_op h x (z * y))^) y *
Abel_rec G A h
  (fun x y z : G =>
   (grp_homo_op h x (y * z) @
    ap (sg_op (h x))
      ((grp_homo_op h y z @ commutativity (h y) (h z)) @
       (grp_homo_op h z y)^)) @
   (grp_homo_op h x (z * y))^) y0
      Abel_ind_hprop x; revert y.
G: Group
A: AbGroup
h: G $-> A
x: G
forall y : abel G,
(fun x : Abel G =>
 Abel_rec G A h
   (fun x0 y0 z : G =>
    (grp_homo_op h x0 (y0 * z) @
     ap (sg_op (h x0))
       ((grp_homo_op h y0 z @
         commutativity (h y0) (h z)) @
        (grp_homo_op h z y0)^)) @
    (grp_homo_op h x0 (z * y0))^) (y * x) =
 Abel_rec G A h
   (fun x0 y0 z : G =>
    (grp_homo_op h x0 (y0 * z) @
     ap (sg_op (h x0))
       ((grp_homo_op h y0 z @
         commutativity (h y0) (h z)) @
        (grp_homo_op h z y0)^)) @
    (grp_homo_op h x0 (z * y0))^) y *
 Abel_rec G A h
   (fun x0 y0 z : G =>
    (grp_homo_op h x0 (y0 * z) @
     ap (sg_op (h x0))
       ((grp_homo_op h y0 z @
         commutativity (h y0) (h z)) @
        (grp_homo_op h z y0)^)) @
    (grp_homo_op h x0 (z * y0))^) x) (ab x)
      Abel_ind_hprop y.
G: Group
A: AbGroup
h: G $-> A
x, y: G
(fun x0 : Abel G =>
 (fun x : Abel G =>
  Abel_rec G A h
    (fun x1 y z : G =>
     (grp_homo_op h x1 (y * z) @
      ap (sg_op (h x1))
        ((grp_homo_op h y z @
          commutativity (h y) (h z)) @
         (grp_homo_op h z y)^)) @
     (grp_homo_op h x1 (z * y))^) (x0 * x) =
  Abel_rec G A h
    (fun x1 y z : G =>
     (grp_homo_op h x1 (y * z) @
      ap (sg_op (h x1))
        ((grp_homo_op h y z @
          commutativity (h y) (h z)) @
         (grp_homo_op h z y)^)) @
     (grp_homo_op h x1 (z * y))^) x0 *
  Abel_rec G A h
    (fun x1 y z : G =>
     (grp_homo_op h x1 (y * z) @
      ap (sg_op (h x1))
        ((grp_homo_op h y z @
          commutativity (h y) (h z)) @
         (grp_homo_op h z y)^)) @
     (grp_homo_op h x1 (z * y))^) x) (ab x)) (ab y)
      apply grp_homo_op. }
G: Group
A: AbGroup
h: G $-> A
(fun a : abel G $-> A =>
 group_precomp A (abel_unit G) a $== h)
  (Build_GroupHomomorphism
     (Abel_rec G A h
        (fun x y z : G =>
         (grp_homo_op h x (y * z) @
          ap (sg_op (h x))
            ((grp_homo_op h y z @
              commutativity (h y) (h z)) @
             (grp_homo_op h z y)^)) @
         (grp_homo_op h x (z * y))^)))
    cbn.
G: Group
A: AbGroup
h: G $-> A
(fun x : G =>
 Coeq_ind
   (fun
      _ : Coeq
            (uncurry2 (fun a b c : G => a * (b * c)))
            (uncurry2 (fun a b c : G => a * (c * b)))
    => A) h
   (fun b : G * G * G =>
    transport_compose
      (fun
         _ : Trunc 0
               (Coeq
                  (uncurry2
                     (fun a b0 c : G => a * (b0 * c)))
                  (uncurry2
                     (fun a b0 c : G => a * (c * b0))))
       => A) tr
      (cglue (fst (fst b), snd (fst b), snd b))
      (h
         (uncurry2 (fun a b0 c : G => a * (b0 * c))
            (fst (fst b), snd (fst b), snd b))) @
    dp_const
      ((grp_homo_op h (fst (fst b))
          (snd (fst b) * snd b) @
        ap (sg_op (h (fst (fst b))))
          ((grp_homo_op h (snd (fst b)) (snd b) @
            commutativity (h (snd (fst b)))
              (h (snd b))) @
           (grp_homo_op h (snd b) (snd (fst b)))^)) @
       (grp_homo_op h (fst (fst b))
          (snd b * snd (fst b)))^)) (coeq x)) == h reflexivity. }
G: Group
A: AbGroup
forall x y : abel G $-> A,
group_precomp A (abel_unit G) x $==
group_precomp A (abel_unit G) y -> x $== y
  intros g h p.
G: Group
A: AbGroup
g, h: abel G $-> A
p: group_precomp A (abel_unit G) g $==
group_precomp A (abel_unit G) h
g $== h
  Abel_ind_hprop x.
G: Group
A: AbGroup
g, h: abel G $-> A
p: group_precomp A (abel_unit G) g $==
group_precomp A (abel_unit G) h
x: G
(fun x : Abel G =>
 (grp_homo_map (abel G) A
  :
  GroupHomomorphism (abel G) A -> abel G $-> A) g x =
 (grp_homo_map (abel G) A
  :
  GroupHomomorphism (abel G) A -> abel G $-> A) h x)
  (ab x)
  exact (p x).
Defined.

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.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
A ≅ B
Proof.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
A ≅ B
  destruct (esssurj (group_precomp B eta1) eta2) as [a ac].
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
A ≅ B
  destruct (esssurj (group_precomp A eta2) eta1) as [b bc].
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
A ≅ B
  srapply (Build_GroupIsomorphism _ _ a).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
IsEquiv a
  srapply (isequiv_adjointify _ b).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
a o b == idmap
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
b o a == idmap
  {
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
a o b == idmap refine (essinj (group_precomp B eta2)
                   (x := a $o b) (y := Id (A := Group) B) _).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
group_precomp B eta2 (a $o b) $==
group_precomp B eta2 (Id B)
    intros x; cbn in *.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: GroupHomomorphism A B
ac: (fun x : G => a (eta1 x)) == eta2
b: GroupHomomorphism B A
bc: (fun x : G => b (eta2 x)) == eta1
x: G
a (b (eta2 x)) = eta2 x
    refine (_ @ ac x).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: GroupHomomorphism A B
ac: (fun x : G => a (eta1 x)) == eta2
b: GroupHomomorphism B A
bc: (fun x : G => b (eta2 x)) == eta1
x: G
a (b (eta2 x)) = a (eta1 x)
    apply ap, bc. }
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
b o a == idmap
  {
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
b o a == idmap refine (essinj (group_precomp A eta1)
                   (x := b $o a) (y := Id (A := Group) A) _).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
group_precomp A eta1 (b $o a) $==
group_precomp A eta1 (Id A)
    intros x; cbn in *.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: GroupHomomorphism A B
ac: (fun x : G => a (eta1 x)) == eta2
b: GroupHomomorphism B A
bc: (fun x : G => b (eta2 x)) == eta1
x: G
b (a (eta1 x)) = eta1 x
    refine (_ @ bc x).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: GroupHomomorphism A B
ac: (fun x : G => a (eta1 x)) == eta2
b: GroupHomomorphism B A
bc: (fun x : G => b (eta2 x)) == eta1
x: G
b (a (eta1 x)) = b (eta2 x)
    apply ap, ac. }
Defined.

Theorem homotopic_isabelianization {G : Group} (A B : AbGroup)
  (eta1 : GroupHomomorphism G A) (eta2 : GroupHomomorphism G B)
  {isab1 : IsAbelianization A eta1} {isab2 : IsAbelianization B eta2}
  : eta2 == grp_homo_compose (groupiso_isabelianization A B eta1 eta2) eta1.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
eta2 ==
grp_homo_compose
  (groupiso_isabelianization A B eta1 eta2) eta1
Proof.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
eta2 ==
grp_homo_compose
  (groupiso_isabelianization A B eta1 eta2) eta1
  intros x.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
x: G
eta2 x =
grp_homo_compose
  (groupiso_isabelianization A B eta1 eta2) eta1 x
  exact (((esssurj (group_precomp B eta1) eta2).2 x)^).
Defined.

(** Hence any abelianization is surjective. *)
Global Instance issurj_isabelianization {G : Group}
  (A : AbGroup) (eta : GroupHomomorphism G A)
  : IsAbelianization A eta -> IsSurjection eta.
G: Group
A: AbGroup
eta: GroupHomomorphism G A
IsAbelianization A eta -> IsConnMap (Tr (-1)) eta
Proof.
G: Group
A: AbGroup
eta: GroupHomomorphism G A
IsAbelianization A eta -> IsConnMap (Tr (-1)) eta
  intros k.
G: Group
A: AbGroup
eta: GroupHomomorphism G A
k: IsAbelianization A eta
IsConnMap (Tr (-1)) eta
  pose (homotopic_isabelianization A (abel G) eta (abel_unit G)) as p.
G: Group
A: AbGroup
eta: GroupHomomorphism G A
k: IsAbelianization A eta
p:= homotopic_isabelianization A (abel G) eta
  (abel_unit G): abel_unit G ==
grp_homo_compose
  (groupiso_isabelianization A (abel G) eta
     (abel_unit G)) eta
IsConnMap (Tr (-1)) eta
  refine (@cancelL_isequiv_conn_map _ _ _ _ _ _ _
    (conn_map_homotopic _ _ _ p _)).
Defined.

Global Instance isabelianization_identity (A : AbGroup) : IsAbelianization A grp_homo_id.
A: AbGroup
IsAbelianization A grp_homo_id
Proof.
A: AbGroup
IsAbelianization A grp_homo_id
  intros B.
A, B: AbGroup
IsSurjInj (group_precomp B grp_homo_id) constructor.
A, B: AbGroup
SplEssSurj (group_precomp B grp_homo_id)
A, B: AbGroup
forall x y : A $-> B,
group_precomp B grp_homo_id x $==
group_precomp B grp_homo_id y -> x $== y
  -
A, B: AbGroup
SplEssSurj (group_precomp B grp_homo_id) intros h; exact (h ; fun _ => idpath).
  -
A, B: AbGroup
forall x y : A $-> B,
group_precomp B grp_homo_id x $==
group_precomp B grp_homo_id y -> x $== y intros g h p; exact p.
Defined.

Global Instance isequiv_abgroup_abelianization
  (A B : AbGroup) (eta : GroupHomomorphism A B) {isab : IsAbelianization B eta}
  : IsEquiv eta.
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
IsEquiv eta
Proof.
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
IsEquiv eta
  srapply isequiv_homotopic.
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
A -> B
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
IsEquiv ?f
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
?f == eta
  -
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
A -> B srapply (groupiso_isabelianization A B grp_homo_id eta).
  -
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
IsEquiv
  (groupiso_isabelianization A B grp_homo_id eta) exact _.
  -
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
groupiso_isabelianization A B grp_homo_id eta == eta symmetry; apply homotopic_isabelianization.
Defined.