module Algebra.Group.Ab.Abelianisation where

AbelianisationsπŸ”—

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 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 =
    Coeq-elim-prop (Ξ» _ β†’ squash _ _) (Ξ» _ β†’ ap inc^ab G.inversel)
  Abelian-group-on-G^ab .idl =
    Coeq-elim-prop (Ξ» _ β†’ squash _ _) (Ξ» _ β†’ 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 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 = Abelianise G

  go .unit G .hom = inc^ab G
  go .unit G .preserves .is-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 = 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))       ∎
  go .universal f .preserves .is-group-hom.pres-⋆ =
    Coeq-elim-propβ‚‚ (Ξ» _ _ β†’ hlevel!) Ξ» _ _ β†’ f .preserves .is-group-hom.pres-⋆ _ _
  go .commutes f = trivial!
  go .unique p = ext (p #β‚š_)