module Algebra.Group.Ab.Abelianisation where

# Abelianisationsπ

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)           β‘
inc^ab ((a β x) β y β z) {- 1 -} β‘
inc^ab ((a β x) β z β y)
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)
inc^ab (x β (y β z) β a) β‘
inc^ab (x β a β y β z)   β‘
inc^ab (x β a β z β y)   β‘
inc^ab (x β (z β y) β a) β‘
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 = 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)
inc^ab (unit β x β y) β‘
inc^ab (unit β y β x)
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 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) β»ΒΉ)                             β‘
inc^ab ((y β z) β»ΒΉ β x)
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 β»ΒΉ)
(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)                             β‘
inc^ab ((z β y) β»ΒΉ β x)                             β‘
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 = Coeq-elim-propβ (Ξ» _ _ _ β squash _ _)
Ξ» _ _ _ β 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 =
Coeq-elim-prop (Ξ» _ β squash _ _) (Ξ» _ β ap inc^ab G.inversel)
Abelian-group-on-G^ab .idl =
Coeq-elim-prop (Ξ» _ β squash _ _) (Ξ» _ β 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

make-free-abelian : β {β} β make-left-adjoint (AbβͺGrp {β = β})
make-free-abelian {β} = go where
go : make-left-adjoint (AbβͺGrp {β = β})
go .free G = Abelianise G

go .unit G .hom = inc^ab G
go .unit G .preserves .is-group-hom.pres-β x y = refl

go .universal {x = G} {y = 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))       β‘
f # a H.* f # (b G.β c)     β‘
f # a H.* (f # b H.* f # c) β‘
f # a H.* (f # c H.* f # b) β‘Λ
f # a H.* f # (c G.β b)     β‘Λ
f # (a G.β (c G.β b))       β
go .universal f .preserves .is-group-hom.pres-β =
Coeq-elim-propβ (Ξ» _ _ β hlevel!) Ξ» _ _ β f .preserves .is-group-hom.pres-β _ _
go .commutes f = trivial!
go .unique p = ext (p #β_)