Abelianization

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.

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.)

Here we define abelianization as a HIT. Specifically as a set-coequalizer of the following two maps fun '(a, b, c) ⇒ a × (b × c) and fun '(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) := | abel_in : G -> Abel G | abel_in_comm : forall x y z, abel_in (x * (y * z)) = abel_in (x * (z * y)). >>> We also derive abel_in and abel_in_comm from our coequalizer definition, and even prove the induction and computation rules for this HIT. This HIT was suggested by Dan Christensen.

Let G be a group.

We locally define a map uncurry2 that lets us uncurry A × B × C → D twice.

The type Abel is defined to be the set coequalizer of the following maps G^3 → G.

We have a natural map from G to Abel G.

This map satisfies the condition ab_comm. It's a form of commutativity in a right factor.

It is clear that Abel is a set.

We can derive the induction principle from the ones for truncation and the coequalizer.

The computation rule on point constructors holds definitionally.

The computation rule on paths.

We also have a recursion princple.

Here is a simpler version of Abel_ind when our target is an HProp. This lets us discard all the higher paths.

The IsHProp argument of Abel_ind_hprop can usually be found by typeclass resolution, but srapply is slow, so we use this tactic instead.

We make sure that G is implicit in the arguments of abel_in and abel_in_comm.

Now we can show that Abel G is in fact an abelian group. We will denote the operation in Abel G by the multiplicative × notation even though it is later shown to be commutative.

Firstly we define the operation on Abel G. This is defined as follows:

        abel_in x * abel_in y := abel_in (x * y)

But we need to also check that it preserves ab_comm in the appropriate way.

We can now easily show that this operation is associative by associativity in G and the fact that being associative is a proposition.

From this we know that Abel G is a semigroup.

We define the group unit as abel_in of the unit of G

By using Abel_ind_hprop we can prove the left and right identity laws.

Hence Abel G is a monoid

We can also prove that the operation is commutative! This will come in handy later.

Now we can define the inverse operation. This is just

        (abel_in g)^ := abel_in g^

However when checking that it respects ab_comm we have to show the following:

        abel_in (z^ * y^ * x^) = abel_in (y^ * z^ * x^)

there is no obvious way to do this, but we note that abel_in (x × y) is exactly the definition of abel_in x × abel_in y! Hence by commutativity we can show this.

Again by Abel_ind_hprop and the corresponding laws for G we can prove the left and right inverse laws.

Thus Abel G is a group

And furthermore, since the operation is commutative, it is an abelian group.

By definition, the map abel_in is also a group homomorphism.

We can easily prove that abel_in is a surjection.

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.

We don't wish for abel G to be unfolded when using simpl or cbn.

The unit of this map is the map abel_in which typeclasses can pick up to be a homomorphism. We write it out explicitly here.

Finally we can prove that our construction abel is an abelianization.

Hence any abelianization is surjective.

Functoriality