open import Algebra.Group.Cat.Base
open import Algebra.Group.Free
open import Algebra.Prelude
open import Algebra.Monoid
open import Algebra.Group

open import Cat.Functor.Adjoint.Monadic
open import Cat.Functor.Adjoint.Monad
open import Cat.Functor.Equivalence
open import Cat.Diagram.Monad
open import Cat.Functor.Base

import Algebra.Group.Cat.Base as Grp

import Cat.Reasoning

module Algebra.Group.Cat.Monadic {β„“} where

Monadicity of the category of groupsπŸ”—

We prove that the category GroupsΞΊ\ht{Groups}_\kappa is monadic over SetsΞΊ\sets_\kappa, or more specifically that the free group adjunction F⊣UF \dashv U is monadic. Rather than appealing to a monadicity theorem, we show this directly by calculation. This actually gives us a slightly sharper result, too: rather than showing that the comparison functor is an equivalence, we show directly that it is an isomorphism of categories. This doesn’t exactly matter since SetsΞΊ\sets_\kappa and GroupsΞΊ\ht{Groups}_\kappa are both univalent categories, but it’s interesting that it’s easier to construct an isomorphism than it is to construct an equivalence.

Let us abbreviate the monad induced by the free group adjunction by TT. What we must show is that any TT-algebra structure on a set GG gives rise to a group structure on GG, and that this process is reversible: If Ξ½\nu is our original algebra, applying our process then applying the comparison functor has to give Ξ½\nu back.

Algebra-onβ†’group-on : {G : Set β„“} β†’ Algebra-on (Sets β„“) T G β†’ Group-on ∣ G ∣
Algebra-on→group-on {G = G} alg = grp where
  open Algebra-on alg

  mult : ∣ G ∣ β†’ ∣ G ∣ β†’ ∣ G ∣
  mult x y = Ξ½ (inc x β—† inc y)

The thing to keep in mind is that a TT-algebra structure is a way of β€œfolding” a word built up from generators in the set GG, so that if we build a word from two generators x,yx, y, folding that should be the same thing as a binary multiplication xyxy. That’s the definition of the induced multiplication structure! We now must show that this definition is indeed a group structure, which is an incredibly boring calculation.

I’m not exaggerating, it’s super boring.
  abstract
    assoc : βˆ€ x y z β†’ mult (mult x y) z ≑ mult x (mult y z)
    assoc x y z =
      Ξ½ (inc (Ξ½ (inc x β—† inc y)) β—† inc z)                β‰‘βŸ¨ (Ξ» i β†’ Ξ½ (inc (Ξ½ (inc x β—† inc y)) β—† inc (Ξ½-unit (~ i) z))) βŸ©β‰‘
      Ξ½ (inc (Ξ½ (inc x β—† inc y)) β—† inc (Ξ½ (inc z)))      β‰‘βŸ¨ happly Ξ½-mult (inc _ β—† inc _) βŸ©β‰‘
      Ξ½ (T.mult.Ξ· G (inc (inc x β—† inc y) β—† inc (inc z))) β‰‘βŸ¨ ap Ξ½ (f-assoc _ _ _) βŸ©β‰‘
      Ξ½ (T.mult.Ξ· G (inc (inc x) β—† inc (inc y β—† inc z))) β‰‘Λ˜βŸ¨ happly Ξ½-mult (inc _ β—† inc _) βŸ©β‰‘Λ˜
      Ξ½ (inc (Ξ½ (inc x)) β—† inc (Ξ½ (inc y β—† inc z)))      β‰‘βŸ¨ (Ξ» i β†’ Ξ½ (inc (Ξ½-unit i x) β—† inc (Ξ½ (inc y β—† inc z)))) βŸ©β‰‘
      Ξ½ (inc x β—† inc (Ξ½ (inc y β—† inc z)))                ∎

    invl : βˆ€ x β†’ mult (Ξ½ (inv (inc x))) x ≑ Ξ½ nil
    invl x =
      Ξ½ (inc (Ξ½ (inv (inc x))) β—† inc x)                β‰‘βŸ¨ (Ξ» i β†’ Ξ½ (inc (Ξ½ (inv (inc x))) β—† inc (Ξ½-unit (~ i) x))) βŸ©β‰‘
      Ξ½ (inc (Ξ½ (inv (inc x))) β—† inc (Ξ½ (inc x)))      β‰‘βŸ¨ happly Ξ½-mult (inc _ β—† inc _) βŸ©β‰‘
      Ξ½ (T.mult.Ξ· G (inc (inv (inc x)) β—† inc (inc x))) β‰‘βŸ¨ ap Ξ½ (f-invl _) βŸ©β‰‘
      Ξ½ (T.mult.Ξ· G (inc nil))                         β‰‘βŸ¨βŸ©
      ν nil                                            ∎

    invr : βˆ€ x β†’ mult x (Ξ½ (inv (inc x))) ≑ Ξ½ nil
    invr x =
      Ξ½ (inc x β—† inc (Ξ½ (inv (inc x))))                β‰‘βŸ¨ (Ξ» i β†’ Ξ½ (inc (Ξ½-unit (~ i) x) β—† inc (Ξ½ (inv (inc x))))) βŸ©β‰‘
      Ξ½ (inc (Ξ½ (inc x)) β—† inc (Ξ½ (inv (inc x))))      β‰‘βŸ¨ happly Ξ½-mult (inc _ β—† inc _) βŸ©β‰‘
      Ξ½ (T.mult.Ξ· G (inc (inc x) β—† inc (inv (inc x)))) β‰‘βŸ¨ ap Ξ½ (f-invr _) βŸ©β‰‘
      Ξ½ (T.mult.Ξ· G (inc nil))                         β‰‘βŸ¨βŸ©
      ν nil                                            ∎

    idlβ€² : βˆ€ x β†’ mult (Ξ½ nil) x ≑ x
    idlβ€² x =
      Ξ½ (inc (Ξ½ nil) β—† inc x)            β‰‘βŸ¨ (Ξ» i β†’ Ξ½ (inc (Ξ½ nil) β—† inc (Ξ½-unit (~ i) x))) βŸ©β‰‘
      Ξ½ (inc (Ξ½ nil) β—† inc (Ξ½ (inc x)))  β‰‘βŸ¨ happly Ξ½-mult (inc _ β—† inc _) βŸ©β‰‘
      Ξ½ (T.mult.Ξ· G (nil β—† inc (inc x))) β‰‘βŸ¨ ap Ξ½ (f-idl _) βŸ©β‰‘
      Ξ½ (inc x)                          β‰‘βŸ¨ happly Ξ½-unit x βŸ©β‰‘
      x                                  ∎

  grp : Group-on ∣ G ∣
  grp .Group-on._⋆_ = mult
  grp .Group-on.has-is-group = to-group-on fg .Group-on.has-is-group where
    fg : make-group ∣ G ∣
    fg .make-group.group-is-set = G .is-tr
    fg .make-group.unit = Ξ½ nil
    fg .make-group.mul = mult
    fg .make-group.inv x = Ξ½ (inv (inc x))
    fg .make-group.assoc = assoc
    fg .make-group.invl = invl
    fg .make-group.invr = invr
    fg .make-group.idl = idlβ€²

We now show that this construction fits into defining an inverse (on the nose!) to the comparison functor. This is slightly easier than it sounds like: We must show that the functor is fully faithful, and that our mapping above is indeed invertible.

Fully faithfulness is almost immediate: a homomorphism of TT-algebras K(G)β†’K(H)K(G) \to K(H) preserves underlying multiplication because the algebra structure of K(G)K(G) (resp. K(H)K(H)) is defined in terms of that multiplication. Since we leave the underlying map intact, and being a homomorphism (either kind) is a property, the comparison functor is fully faithful.

Group-is-monadic : is-monadic F⊣U
Group-is-monadic = is-precat-iso→is-equivalence
  record { has-is-ff = ff ; has-is-iso = is-iso→is-equiv isom } where
  open Algebra-hom
  open Algebra-on

  k₁inv : βˆ€ {G H} β†’ Algebra-hom (Sets β„“) T (K.β‚€ G) (K.β‚€ H) β†’ Groups.Hom G H
  k₁inv hom .fst = hom .morphism
  k₁inv hom .snd .Group-hom.pres-⋆ x y = happly (hom .commutes) (inc x β—† inc y)

  ff : is-fully-faithful K
  ff = is-isoβ†’is-equiv $ iso k₁inv (Ξ» x β†’ Algebra-hom-path (Sets β„“) refl)
                                   (Ξ» x β†’ Grp.Forget-is-faithful refl)

To show that the object mapping of the comparison functor is invertible, we appeal to univalence. Since the types are kept the same, it suffices to show that passing between a multiplication and an algebra map doesn’t lose any information. This is immediate in one direction, but the other direction is by induction on β€œwords”.

  isom : is-iso K.β‚€
  isom .is-iso.inv (A , alg) = ∣ A ∣ , Algebra-onβ†’group-on alg
  isom .is-iso.linv x = sip Group-univalent $
    (_ , id-equiv) , record { pres-⋆ = Ξ» x y β†’ refl }
  isom .is-iso.rinv x = Ξ£-pathp ext (Algebra-on-pathp _ _ go) where
    open n-Type (x .fst) hiding (∣_∣)
    ext : el (∣ x .fst ∣) (x .fst .is-tr) ≑ x .fst
    ext i .∣_∣ = ∣ x .fst ∣
    ext i .is-tr = x .fst .is-tr

    alg = x .snd
    grp = Algebra-on→group-on alg
    rec = fold-free-group {G = ∣ x .fst ∣ , grp} (Ξ» x β†’ x)
    module G = Group-on grp

    alg-gh : Group-hom (Free-Group ∣ x .fst ∣) (_ , grp) (x .snd .ν)
    alg-gh .Group-hom.pres-⋆ x y = sym (happly (alg .Ξ½-mult) (inc _ β—† inc _))

    go : rec .fst ≑ x .snd .Ξ½
    go = funext $ Free-elim-prop _ (Ξ» _ β†’ hlevel 1)
      (Ξ» x β†’ sym (happly (alg .Ξ½-unit) x))
      (Ξ» x y p q β†’ rec .snd .Group-hom.pres-⋆ x y
                Β·Β· apβ‚‚ G._⋆_ p q
                Β·Β· happly (alg .Ξ½-mult) (inc _ β—† inc _))
      (Ξ» x p β†’ Group-hom.pres-inv (rec .snd) {x = x}
              Β·Β· ap G.inverse p
              Β·Β· sym (Group-hom.pres-inv alg-gh {x = x}))
      refl