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

The abelianisation $G^{ab}$ of a group $G$ is the universal abelian group with a map from $G :$ that is, the reflection of $G$ into the category of abelian groups.

Rather than constructing $G^{ab}$ as quotient group (by the commutator subgroup $[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 $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,$ 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} .$ 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},$ which will be our multiplication, satisfying
for any $a, x, y, z : G,$ an identification $f (a x yz) = f (a x zy)$ ( $f$ respects the first coequaliser)
for any $a, x, y, z : G,$ an identification $f ((x yz) a) = f ((x zy) 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 x y$ and $x, y \mapsto y x,$ 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: $x y = 1 x y = 1 y x = y x .$

  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} .$ To show this, we must prove that $(x yz)^{- 1}$ and $(x zy)^{- 1}$ are equal in $G_{0}^{ab} .$ 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,$ the group axioms are also inherited from $G!$

  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 i 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,$ we can factor it uniquely as

G i G^{ab} \hat{f} H

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

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) (apply 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 ·ₚ_)