open import Algebra.Group.Cat.Base
open import Algebra.Group.Ab
open import Algebra.Prelude
open import Algebra.Group

open import Data.Set.Coequaliser

module Algebra.Group.Ab.Free where


# Free Abelian Groupsπ

module _ (Grp@(G , gst) : Group β) where
private module G = Group-on gst
open G


We define the abelianisation of a group $G$, $G^{ab}$. Rather than defining it a quotient group (by the commutator subgroup $[G,G]$), we directly define a group structure on a set-coequaliser. To emphasise the difference between the groups and their underlying sets, weβll write $G_0$ and $G^{ab}_0$ in the prose.

  G^ab : Type β
G^ab = Coeq {A = G Γ G Γ G} (Ξ» (x , y , z) β x β y β z)
(Ξ» (x , y , z) β x β z β y)

inc^ab : G β G^ab
inc^ab = inc

ab-comm : β x y z β inc^ab (x β y β z) β‘ inc^ab (x β z β y)
ab-comm x y z = glue (x , y , z)


The definition of ab-comm gives us extra flexibility in multiplying on the right by a fixed argument $x$, which will be necessary to prove that G^ab admits a group structure. We can recover the actual commutativity by choosing $x$ to be the unit. Letβs see how equipping G^ab works out:

  abunit : G^ab
abunit = inc^ab unit


The abelianised unit is the image of the group unit under the map $G_0 \to G^{ab}_0$. We can define the abelianised multiplication by coequaliser recursion, which βreducesβ the problem of defining a map $G^{ab}_0 \to G^{ab}_0 \to G^{ab}_0$ to defining:

• A map $f : G \to G \to G^{ab}_0$, which will be our multiplication, satisfying
• for any $a, x, y, z : G$, an identification $f(axyz) = f(axzy)$ ($f$ respects the first coequaliser)
• for any $a, x, y, z : G$, an identification $f((xyz)a) = f((xzy)a)$ ($f$ respects the second coequaliser)
  _ab*_ : G^ab β G^ab β G^ab
_ab*_ = Coeq-recβ squash (Ξ» x y β inc^ab (x β y)) l2 l1
where abstract


Showing these two conditions isnβt hard, but it does involve a lot of very tedious algebra. See for yourself:

      l1 : β a ((x , y , z) : G Γ G Γ G)
β inc^ab (a β x β y β z) β‘ inc^ab (a β x β z β y)
l1 a (x , y , z) =
inc^ab (a β x β y β z)           β‘β¨ ap inc^ab associative β©β‘
inc^ab ((a β x) β y β z) {- 1 -} β‘β¨ ab-comm _ _ _ β©β‘
inc^ab ((a β x) β z β y)         β‘β¨ ap inc^ab (sym associative) β©β‘
inc^ab (a β x β z β y)           β


That comment {- 1 -} marks the place where we had to use the extra generality ab-comm gives us; If we had simply coequalised $x, y \mapsto xy$ and $x, y \mapsto yx$, weβd be lost! Thereβs some more tedious but straightforward algebra to define the second coequaliser condition:

      l2 : β a ((x , y , z) : G Γ G Γ G)
β inc^ab ((x β y β z) β a) β‘ inc^ab ((x β z β y) β a)
l2 a (x , y , z) =
inc^ab ((x β y β z) β a) β‘β¨ ap inc^ab (sym associative) β©β‘
inc^ab (x β (y β z) β a) β‘β¨ ab-comm _ _ _ β©β‘
inc^ab (x β a β y β z)   β‘β¨ l1 _ (_ , _ , _) β©β‘
inc^ab (x β a β z β y)   β‘β¨ ab-comm _ _ _ β©β‘
inc^ab (x β (z β y) β a) β‘β¨ ap inc^ab associative β©β‘
inc^ab ((x β z β y) β a) β


Now we want to define the inverse, but we must first take a detour and prove that the operation weβve defined is commutative. This is still a bit tedious, but it follows from ab-comm: $xy = 1xy = 1yx = yx$.

  ab*-comm : β x y β x ab* y β‘ y ab* x
ab*-comm = Coeq-elim-propβ (Ξ» _ _ β squash _ _) l1
where abstract
l1 : β x y β inc^ab (x β y) β‘ inc^ab (y β x)
l1 x y =
inc^ab (x β y)        β‘β¨ ap inc^ab (apβ _β_ (sym G.idl) refl β sym G.associative) β©β‘
inc^ab (unit β x β y) β‘β¨ ab-comm _ _ _ β©β‘
inc^ab (unit β y β x) β‘β¨ ap inc^ab (G.associative β apβ _β_ G.idl refl) β©β‘
inc^ab (y β x)        β


Now we can define the inverse map. We prove that $x \mapsto x^{-1}$ extends from a map $G_0 \to G_0$ to a map $G^{ab}_0 \to G^{ab}_0$. To show this, we must prove that $(xyz)^{-1}$ and $(xzy)^{-1}$ are equal in $G^{ab}_0$. This is why we showed commutativity of _ab*_ before defining the inverse map. Here, check out the cute trick embedded in the tedious algebra:

  abinv : G^ab β G^ab
abinv = Coeq-rec squash (Ξ» x β inc^ab (x β»ΒΉ)) l1
where abstract
l1 : ((x , y , z) : G Γ G Γ G)
β inc^ab ((x β y β z) β»ΒΉ) β‘ inc^ab ((x β z β y) β»ΒΉ)
l1 (x , y , z) =
inc^ab ((x β y β z) β»ΒΉ)                             β‘β¨ ap inc^ab G.inv-comm β©β‘
inc^ab ((y β z) β»ΒΉ β x)                             β‘β¨ ap inc^ab (apβ _β_ G.inv-comm refl) β©β‘
inc^ab ((z β»ΒΉ β y) β x)                             β‘β¨β©


We get to something that is definitionally equal to our _ab*_ multiplication, which we know is commutative, so we can swap $y^{-1}$ and $z^{-1}$ around!

        (inc^ab (z β»ΒΉ) ab* inc^ab (y β»ΒΉ)) ab* inc^ab (x β»ΒΉ) β‘β¨ apβ _ab*_ (ab*-comm (inc^ab (z β»ΒΉ)) (inc^ab (y β»ΒΉ))) (Ξ» i β inc^ab (x β»ΒΉ)) β©β‘
(inc^ab (y β»ΒΉ) ab* inc^ab (z β»ΒΉ)) ab* inc^ab (x β»ΒΉ) β‘β¨β©


Thatβs a neat trick, isnβt it. We still need some Tedious Algebra to finish the proof:

        inc^ab ((y β»ΒΉ β z) β x)                             β‘β¨ ap inc^ab (apβ _β_ (sym G.inv-comm) refl ) β©β‘
inc^ab ((z β y) β»ΒΉ β x)                             β‘β¨ ap inc^ab (sym G.inv-comm) β©β‘
inc^ab ((x β z β y) β»ΒΉ)                             β


The beautiful thing is that, since the group operations on $G^{ab}$ are all defined in terms of those of $G$, the group axioms are also inherited from $G$!

  ab*-associative : β x y z β (x ab* y) ab* z β‘ x ab* (y ab* z)
ab*-associative = Coeq-elim-propβ (Ξ» _ _ _ β squash _ _)
Ξ» _ _ _ β ap inc^ab (sym associative)

Group-on-G^ab : Group-on G^ab
Group-on-G^ab = make-group squash abunit _ab*_ abinv ab*-associative
(Coeq-elim-prop (Ξ» _ β squash _ _) (Ξ» _ β ap inc^ab G.inversel))
(Coeq-elim-prop (Ξ» _ β squash _ _) (Ξ» _ β ap inc^ab G.inverser))
(Coeq-elim-prop (Ξ» _ β squash _ _) (Ξ» _ β ap inc^ab G.idl))

Abelianise : Group β
Abelianise = _ , Group-on-G^ab

Abelianise-is-abelian-group : is-abelian-group Abelianise
Abelianise-is-abelian-group = ab*-comm


## Universal propertyπ

This finishes the construction of an abelian group from a group. To show that this construction is correct, weβll show that it satisfies a universal property: The map inc^ab, which we write as being from $G \to G^{ab}$, is a group homomorphism, and furthermore, it provides a universal way of mapping from $G$ to an abelian group, in that if $H$ is an abelian group, then a map $f : G \to H$ factors through inc^ab in a unique way.

Abelianise-universal
: β {G : Group β} β Universal-morphism G AbβGrp
Abelianise-universal {β = β} {G = G} = m where
open Cat (const! {A = Groups β} G β AbβGrp)
open Initial
module G = Group-on (G .snd)


Our choice of initial object was already stated in the paragraph above β itβs the epimorphism $q : G \to G^{ab}$, i.e., the map which we call inc^ab.

  init : Ob
init .βObj.x = tt
init .βObj.y = Abelianise G , Abelianise-is-abelian-group G
init .βObj.map .fst = inc^ab G
init .βObj.map .snd .Group-hom.pres-β x y = refl

m : Initial
m .bot = init
m .hasβ₯ other = contr factor unique where


Now suppose we have an abelian group $H$ and a map $f : G \to H$. We factor it through $G^{ab}$ as follows: Since $f$ is a homomorphism into an abelian group, it βrespects commutativityβ, by which I mean that $f(ab) = f(a)f(b) = f(b)f(a) = f(ba)$, meaning in particular that it satisfies the requirements for mapping out of Abelianise at the level of sets.

    factor : Hom _ other
factor .βHom.Ξ± = tt
factor .βHom.Ξ² .fst = Coeq-elim (Ξ» _ β H.has-is-set) f (Ξ» (a , b , c) β resp a b c)
where abstract
resp : β a b c β f (a G.β (b G.β c)) β‘ f (a G.β (c G.β b))
resp a b c =
f (a G.β (b G.β c))   β‘β¨ pres-β _ _ β©β‘
f a H.β f (b G.β c)   β‘β¨ ap (f a H.β_) (pres-β _ _) β©β‘
f a H.β (f b H.β f c) β‘β¨ ap (f a H.β_) H.commutative β©β‘
f a H.β (f c H.β f b) β‘Λβ¨ ap (f a H.β_) (pres-β _ _) β©β‘Λ
f a H.β f (c G.β b)   β‘Λβ¨ pres-β _ _ β©β‘Λ
f (a G.β (c G.β b))   β


To show that the map $h : G^{ab} \to H$ induced by $f$ is a group homomorphism, it suffices to assume that we have two honest-to-god elements $x, y : G$, and since $h$ is exactly $f$ on generators, the required identification $f(xy) = f(x)f(y)$ follows from $f$ being a group homomorphism.

    factor .βHom.Ξ² .snd .Group-hom.pres-β =
Coeq-elim-propβ (Ξ» _ _ β H.has-is-set _ _) Ξ» x y β pres-β _ _
factor .βHom.sq = Forget-is-faithful refl


Now if $h'$ is any other map which factors $G \xepi{q} G^{ab} \xto{h'} H$, since $G \to G^{ab}$ is an epimorphism, we must have $h = h'$.

    unique : β h β factor β‘ h
unique x = βHom-path _ _ refl $Forget-is-faithful$ funext \$
Coeq-elim-prop (Ξ» _ β H.has-is-set _ _) Ξ» y i β x .βHom.sq i .fst y