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 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 : 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β†’GabG \to G^{ab}, is a group homomorphism, and furthermore, it provides a universal way of mapping from GG to an abelian group, in that if HH is an abelian group, then a map f:Gβ†’Hf : G \to H factors through inc^ab in a unique way.

  : βˆ€ {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β†’Gabq : 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 .↓ .fst = inc^ab G
  init .↓ .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 HH and a map f:Gβ†’Hf : G \to H. We factor it through GabG^{ab} as follows: Since ff 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)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:Gab→Hh : G^{ab} \to H induced by ff is a group homomorphism, it suffices to assume that we have two honest-to-god elements x,y:Gx, y : G, and since hh is exactly ff on generators, the required identification f(xy)=f(x)f(y)f(xy) = f(x)f(y) follows from ff 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′h' is any other map which factors G↠qGab→h′HG \xepi{q} G^{ab} \xto{h'} H, since G→GabG \to G^{ab} is an epimorphism, we must have h=h′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