module Algebra.Group.Cat.Monadic {ℓ} where
private F : Functor (Sets ℓ) (Groups ℓ) F = free-objects→functor make-free-group F⊣U : F ⊣ _ F⊣U = free-objects→left-adjoint make-free-group K = Comparison-EM F⊣U T : Monad (Sets ℓ) T = Adjunction→Monad F⊣U module F = Functor F module T = Monad T module K = Functor K module Sets^T = Cat.Reasoning (Eilenberg-Moore T)
Monadicity of the category of groups🔗
We prove that the category is monadic over or more specifically that the free group adjunction 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 and 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 What we must show is that any structure on a set gives rise to a group structure on and that this process is reversible: If is our original algebra, applying our process then applying the comparison functor has to give 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 structure is a way of “folding” a word built up from generators in the set so that if we build a word from two generators folding that should be the same thing as a binary multiplication 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 x (mult y z) ≡ mult (mult x y) z assoc x y z = sym $ ν (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 ∎ 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.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 preserves underlying multiplication because the algebra structure of (resp. 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-on k₁inv : ∀ {G H} → Algebra-hom T (K.₀ G) (K.₀ H) → Groups.Hom G H k₁inv f .hom = f .hom k₁inv f .preserves .is-group-hom.pres-⋆ x y = happly (f .preserves) (inc x ◆ inc y) ff : is-fully-faithful K ff = is-iso→is-equiv $ iso k₁inv (λ x → trivial!) (λ x → Grp.Grp↪Sets-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 = ∫-Path (total-hom (λ x → x) (record { pres-⋆ = λ x y → refl })) id-equiv isom .is-iso.rinv x = Σ-pathp refl (Algebra-on-pathp _ _ go) where 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 : is-group-hom (Free-Group ⌞ x ⌟ .snd) grp (x .snd .ν) alg-gh .is-group-hom.pres-⋆ x y = sym (happly (alg .ν-mult) (inc _ ◆ inc _)) go : rec .hom ≡ x .snd .ν go = funext $ Free-elim-prop _ (λ _ → hlevel 1) (λ x → sym (happly (alg .ν-unit) x)) (λ x p y q → rec .preserves .is-group-hom.pres-⋆ x y ·· ap₂ G._⋆_ p q ·· happly (alg .ν-mult) (inc _ ◆ inc _)) (λ x p → is-group-hom.pres-inv (rec .preserves) {x = x} ·· ap G.inverse p ·· sym (is-group-hom.pres-inv alg-gh {x = x})) refl