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 : 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 = 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 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) β»ΒΉ) β‘β¨ 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 = Coeq-elim-propβ (Ξ» _ _ _ β squash _ _) Ξ» _ _ _ β ap inc^ab (sym associative) Group-on-G^ab : make-group G^ab Group-on-G^ab .make-group.group-is-set = squash Group-on-G^ab .make-group.unit = abunit Group-on-G^ab .make-group.mul = _ab*_ Group-on-G^ab .make-group.inv = abinv Group-on-G^ab .make-group.assoc = ab*-associative Group-on-G^ab .make-group.invl = Coeq-elim-prop (Ξ» _ β squash _ _) (Ξ» _ β ap inc^ab G.inversel) Group-on-G^ab .make-group.invr = Coeq-elim-prop (Ξ» _ β squash _ _) (Ξ» _ β ap inc^ab G.inverser) Group-on-G^ab .make-group.idl = Coeq-elim-prop (Ξ» _ β squash _ _) (Ξ» _ β ap inc^ab G.idl) Abelianise : Group β Abelianise = to-group Group-on-G^ab Abelianise-is-abelian-group : is-abelian-group (to-group-on Group-on-G^ab) 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 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 open make-left-adjoint go : make-left-adjoint AbβGrp go .free G = restrict (Abelianise G) (Abelianise-is-abelian-group G) go .unit G .hom = inc^ab G go .unit G .preserves .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 = AbGrp H open 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.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)) β go .universal f .preserves .Group-hom.pres-β = Coeq-elim-propβ (Ξ» _ _ β hlevel!) Ξ» _ _ β f .preserves .Group-hom.pres-β _ _ go .commutes f = Homomorphism-path (Ξ» _ β refl) go .unique p = Homomorphism-path (Coeq-elim-prop (Ξ» _ β hlevel!) (Ξ» x β p #β x))