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 GG, GabG^{ab}. Rather than defining it a quotient group (by the commutator subgroup [G,G][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 G0G_0 and G0abG^{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 xx, which will be necessary to prove that G^ab admits a group structure. We can recover the actual commutativity by choosing xx 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 G0β†’G0abG_0 \to G^{ab}_0. We can define the abelianised multiplication by coequaliser recursion, which β€œreduces” the problem of defining a map G0abβ†’G0abβ†’G0abG^{ab}_0 \to G^{ab}_0 \to G^{ab}_0 to defining:

  • A map f:Gβ†’Gβ†’G0abf : G \to G \to G^{ab}_0, which will be our multiplication, satisfying
  • for any a,x,y,z:Ga, x, y, z : G, an identification f(axyz)=f(axzy)f(axyz) = f(axzy) (ff respects the first coequaliser)
  • for any a,x,y,z:Ga, x, y, z : G, an identification f((xyz)a)=f((xzy)a)f((xyz)a) = f((xzy)a) (ff 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↦xyx, y \mapsto xy and x,y↦yxx, 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=yxxy = 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↦xβˆ’1x \mapsto x^{-1} extends from a map G0β†’G0G_0 \to G_0 to a map G0abβ†’G0abG^{ab}_0 \to G^{ab}_0. To show this, we must prove that (xyz)βˆ’1(xyz)^{-1} and (xzy)βˆ’1(xzy)^{-1} are equal in G0abG^{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βˆ’1y^{-1} and zβˆ’1z^{-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 GabG^{ab} are all defined in terms of those of GG, the group axioms are also inherited from GG!

  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 Gβ†’iGabG {\xrightarrow{i}} G^{ab} from a group to its abelianisation is universal among maps from groups to abelian groups. To wit: If HH is some other abelian group with a map f:Gβ†’Hf : G \to H, we can factor it uniquely as

G→iGab→f^H G {\xrightarrow{i}} G^{ab} {\xrightarrow{\hat f}} H

for some f^:Gab→H\hat f : G^{ab} \to H derived from ff.

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