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

open import Cat.Functor.Adjoint
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 $G\text{,}$ $G^{ab}\text{.}$ Rather than defining it a quotient group (by the commutator subgroup $[G,G]\text{),}$ we directly define a group structure on a set-coequaliser. To emphasise the difference between the groups and their underlying sets, we’ll write $G_0$ and $G_0^{ab}$ 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 $x\text{,}$ which will be necessary to prove that G^ab admits a group structure. We can recover the actual commutativity by choosing $x$ 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 $G_0\to G_0^{ab}\text{.}$ We can define the abelianised multiplication by coequaliser recursion, which “reduces” the problem of defining a map $G_0^{ab}\to G_0^{ab}\to G_0^{ab}$ to defining:

• A map $f:G\to G\to G_0^{ab}\text{,}$ which will be our multiplication, satisfying
• for any $a,x,y,z:G\text{,}$ an identification $f(axyz)=f(axzy)$ ($f$ respects the first coequaliser)
• for any $a,x,y,z:G\text{,}$ an identification $f((xyz)a)=f((xzy)a)$ ($f$ 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\mapsto xy$ and $x,y\mapsto yx\text{,}$ 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=yx\text{.}$

  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 $x\mapsto x^{-1}$ extends from a map $G_0\to G_0$ to a map $G_0^{ab}\to G_0^{ab}\text{.}$ To show this, we must prove that $(xyz{)}^{-1}$ and $(xzy{)}^{-1}$ are equal in $G_0^{ab}\text{.}$ 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 $y^{-1}$ and $z^{-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 $G^{ab}$ are all defined in terms of those of $G\text{,}$ the group axioms are also inherited from $G\text{!}$

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

for some $\hat{f}:G^{ab}\to H$ derived from $f\text{.}$

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 #ₚ_)