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

open import Cat.Prelude

module Algebra.Group.Ab.Abelianisation where


# Abelianisationsπ

module _ {β} (Grp : Group β) where
private
module G = Group-on (Grp .snd)
G = β Grp β
open G


We define the abelianisation of a group Rather than defining it a quotient group (by the commutator subgroup we directly define a group structure on a set-coequaliser. To emphasise the difference between the groups and their underlying sets, weβll write and 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 which will be necessary to prove that G^ab admits a group structure. We can recover the actual commutativity by choosing 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 We can define the abelianised multiplication by coequaliser recursion, which βreducesβ the problem of defining a map to defining:

• A map which will be our multiplication, satisfying
• for any an identification ( respects the first coequaliser)
• for any an identification ( 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 and 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:

  ab*-comm : β x y β x ab* y β‘ y ab* x
ab*-comm = elim! 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 extends from a map to a map To show this, we must prove that and are equal in 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 (Ξ» 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 and 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 are all defined in terms of those of the group axioms are also inherited from

  ab*-associative : β x y z β x ab* (y ab* z) β‘ (x ab* y) ab* z
ab*-associative = elim! Ξ» _ _ _ β ap inc^ab associative

open make-abelian-group
Abelian-group-on-G^ab : make-abelian-group G^ab
Abelian-group-on-G^ab .ab-is-set = squash
Abelian-group-on-G^ab .1g  = abunit
Abelian-group-on-G^ab .mul = _ab*_
Abelian-group-on-G^ab .inv = abinv
Abelian-group-on-G^ab .assoc = ab*-associative
Abelian-group-on-G^ab .invl = elim! Ξ» _ β ap inc^ab G.inversel
Abelian-group-on-G^ab .idl = elim! Ξ» _ β ap inc^ab G.idl
Abelian-group-on-G^ab .comm = ab*-comm

Abelianise : Abelian-group β
Abelianise = to-ab Abelian-group-on-G^ab


## 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 inclusion map from a group to its abelianisation is universal among maps from groups to abelian groups. To wit: If is some other abelian group with a map we can factor it uniquely as

for some derived from

open Free-object

make-free-abelian : β {β} (G : Group β) β Free-object AbβͺGrp G
make-free-abelian G .free = Abelianise G
make-free-abelian G .unit .hom =  inc^ab G
make-free-abelian G .unit .preserves .is-group-hom.pres-β x y = refl
make-free-abelian G .fold {H} f .hom =
Coeq-elim (Ξ» _ β H.has-is-set) (f #_) (Ξ» (a , b , c) β resp a b c) where
module G = Group-on (G .snd)
module H = Abelian-group-on (H .snd)
open is-group-hom (f .preserves)
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.commutes β©β‘
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))       β
make-free-abelian G .fold {H} f .preserves .is-group-hom.pres-β =
elim! Ξ» _ _ β f .preserves .is-group-hom.pres-β _ _
make-free-abelian G .commute = trivial!
make-free-abelian G .unique f p = ext (p #β_)