module Algebra.Monoid.Category where

Category of monoids🔗

The collection of all Monoids relative to some universe level assembles into a precategory. This is because being a monoid homomorphism is a proposition, and so does not raise the h-level of the Hom-sets.

instance
  H-Level-Monoid-hom
    : ∀ {ℓ ℓ'} {s : Type ℓ} {t : Type ℓ'}
    → ∀ {x : Monoid-on s} {y : Monoid-on t} {f} {n}
    → H-Level (Monoid-hom x y f) (suc n)
  H-Level-Monoid-hom {y = M} = prop-instance λ x y i →
    record { pres-id = M .has-is-set _ _ (x .pres-id) (y .pres-id) i
           ; pres-⋆ = λ a b → M .has-is-set _ _ (x .pres-⋆ a b) (y .pres-⋆ a b) i
           }

It’s routine to check that the identity is a monoid homomorphism and that composites of homomorphisms are again homomorphisms; This means that Monoid-on assembles into a structure thinly displayed over the category of sets, so that we may appeal to general results about displayed categories to reason about the category of monoids.

Monoid-structure : ∀ ℓ → Thin-structure ℓ Monoid-on
Monoid-structure ℓ .is-hom f A B = el! $ Monoid-hom A B f

Monoid-structure ℓ .id-is-hom .pres-id = refl
Monoid-structure ℓ .id-is-hom .pres-⋆ x y = refl

Monoid-structure ℓ .∘-is-hom f g p1 p2 .pres-id =
  ap f (p2 .pres-id) ∙ p1 .pres-id
Monoid-structure ℓ .∘-is-hom f g p1 p2 .pres-⋆ x y =
  ap f (p2 .pres-⋆ _ _) ∙ p1 .pres-⋆ _ _

Monoid-structure ℓ .id-hom-unique mh _ i .identity = mh .pres-id i
Monoid-structure ℓ .id-hom-unique mh _ i ._⋆_ x y = mh .pres-⋆ x y i
Monoid-structure ℓ .id-hom-unique {s = s} {t = t} mh _ i .has-is-monoid =
  is-prop→pathp
    (λ i → hlevel {T = is-monoid (mh .pres-id i) (λ x y → mh .pres-⋆ x y i)} 1)
    (s .has-is-monoid)
    (t .has-is-monoid)
    i

Monoids : ∀ ℓ → Precategory (lsuc ℓ) ℓ
Monoids ℓ = Structured-objects (Monoid-structure ℓ)

Monoids-is-category : ∀ {ℓ} → is-category (Monoids ℓ)
Monoids-is-category = Structured-objects-is-category (Monoid-structure _)

By standard nonsense, then, the category of monoids admits a faithful functor into the category of sets.

Forget : ∀ {ℓ} → Functor (Monoids ℓ) (Sets ℓ)
Forget = Forget-structure (Monoid-structure _)

Free objects🔗

We piece together some properties of lists to show that, if $A$ is a set, then $\mathrm{List}(A)$ is an object of Monoids; The operation is list concatenation, and the identity element is the empty list.

List-is-monoid : ∀ {ℓ} {A : Type ℓ} → is-set A
              → Monoid-on (List A)
List-is-monoid aset .identity = []
List-is-monoid aset ._⋆_ = _++_
List-is-monoid aset .has-is-monoid .idl = refl
List-is-monoid aset .has-is-monoid .idr = ++-idr _
List-is-monoid aset .has-is-monoid .has-is-semigroup .has-is-magma .has-is-set =
  ListPath.is-set→List-is-set aset
List-is-monoid aset .has-is-monoid .has-is-semigroup .associative {x} {y} {z} =
  sym (++-assoc x y z)

We prove that the assignment $X \mapsto \mathrm{List}(X)$ is functorial; We call this functor Free, since it is a left adjoint to the Forget functor defined above: it solves the problem of turning a set into a monoid in the most efficient way.

Free : ∀ {ℓ} → Functor (Sets ℓ) (Monoids ℓ)
Free .F₀ A = el! (List ∣ A ∣) , List-is-monoid (A .is-tr)

The action on morphisms is given by map, which preserves the monoid identity definitionally; We must prove that it preserves concatenation, identity and composition by induction on the list.

Free .F₁ f = total-hom (map f) record { pres-id = refl ; pres-⋆  = map-++ f }
Free .F-id = ext map-id
Free .F-∘ f g = ext map-∘ where
  map-∘ : ∀ xs → map (λ x → f (g x)) xs ≡ map f (map g xs)
  map-∘ [] = refl
  map-∘ (x ∷ xs) = ap (f (g x) ∷_) (map-∘ xs)

We refer to the adjunction counit as fold, since it has the effect of multiplying all the elements in the list together. It “folds” it up into a single value.

fold : ∀ {ℓ} (X : Monoid ℓ) → List (X .fst) → X .fst
fold (M , m) = go where
  module M = Monoid-on m

  go : List M → M
  go [] = M.identity
  go (x ∷ xs) = x M.⋆ go xs

We prove that fold is a monoid homomorphism, and that it is a natural transformation, hence worthy of being an adjunction counit.

fold-++ : ∀ {ℓ} {X : Monoid ℓ} (xs ys : List (X .fst))
        → fold X (xs ++ ys) ≡ Monoid-on._⋆_ (X .snd) (fold X xs) (fold X ys)
fold-++ {X = X} = go where
  module M = Monoid-on (X .snd)
  go : ∀ xs ys → _
  go [] ys = sym M.idl
  go (x ∷ xs) ys =
    fold X (x ∷ xs ++ ys)            ≡⟨⟩
    x M.⋆ fold X (xs ++ ys)          ≡⟨ ap (_ M.⋆_) (go xs ys) ⟩
    x M.⋆ (fold X xs M.⋆ fold X ys)  ≡⟨ M.associative ⟩
    fold X (x ∷ xs) M.⋆ fold X ys    ∎

fold-natural : ∀ {ℓ} {X Y : Monoid ℓ} f → Monoid-hom (X .snd) (Y .snd) f
             → ∀ xs → fold Y (map f xs) ≡ f (fold X xs)
fold-natural f mh [] = sym (mh .pres-id)
fold-natural {X = X} {Y} f mh (x ∷ xs) =
  f x Y.⋆ fold Y (map f xs) ≡⟨ ap (_ Y.⋆_) (fold-natural f mh xs) ⟩
  f x Y.⋆ f (fold X xs)     ≡⟨ sym (mh .pres-⋆ _ _) ⟩
  f (x X.⋆ fold X xs)       ∎
  where
    module X = Monoid-on (X .snd)
    module Y = Monoid-on (Y .snd)

Proving that it satisfies the zig triangle identity is the lemma fold-pure below.

fold-pure : ∀ {ℓ} {X : Set ℓ} (xs : List ∣ X ∣)
          → fold (List ∣ X ∣ , List-is-monoid (X .is-tr)) (map (λ x → x ∷ []) xs)
          ≡ xs
fold-pure [] = refl
fold-pure {X = X} (x ∷ xs) = ap (x ∷_) (fold-pure {X = X} xs)

Free⊣Forget : ∀ {ℓ} → Free {ℓ} ⊣ Forget
Free⊣Forget .unit .η _ x = x ∷ []
Free⊣Forget .unit .is-natural x y f = refl
Free⊣Forget .counit .η M = total-hom (fold _) record { pres-id = refl ; pres-⋆ = fold-++ }
Free⊣Forget .counit .is-natural x y th =
  ext $ fold-natural (th .hom) (th .preserves)
Free⊣Forget .zig {A = A} =
  ext $ fold-pure {X = A}
Free⊣Forget .zag {B = B} i x = B .snd .idr {x = x} i

This concludes the proof that Monoids has free objects. We now prove that monoids are equivalently algebras for the List monad, i.e. that the Free⊣Forget adjunction is monadic. More specifically, we show that the canonically-defined comparison functor is fully faithful (list algebra homomoprhisms are equivalent to monoid homomorphisms) and that it is split essentially surjective.

Monoid-is-monadic : ∀ {ℓ} → is-monadic (Free⊣Forget {ℓ})
Monoid-is-monadic {ℓ} = ff+split-eso→is-equivalence it's-ff it's-eso where
  open import Cat.Diagram.Monad hiding (Free⊣Forget)

  comparison = Comparison (Free⊣Forget {ℓ})
  module comparison = Functor comparison

  it's-ff : is-fully-faithful comparison
  it's-ff {x} {y} = is-iso→is-equiv (iso from from∘to to∘from) where
    module x = Monoid-on (x .snd)
    module y = Monoid-on (y .snd)

First, for full-faithfulness, it suffices to prove that the morphism part of comparison is an isomorphism. Hence, define an inverse; It suffices to show that the underlying map of the algebra homomorphism is a monoid homomorphism, which follows from the properties of monoids:

    from : Algebra-hom _ _ (comparison.₀ x) (comparison.₀ y) → Monoids ℓ .Hom x y
    from alg .hom = alg .Algebra-hom.morphism
    from alg .preserves .pres-id = happly (alg .Algebra-hom.commutes) []
    from alg .preserves .pres-⋆ a b =
      f (a x.⋆ b)                  ≡˘⟨ ap f (ap (a x.⋆_) x.idr) ⟩
      f (a x.⋆ (b x.⋆ x.identity)) ≡⟨ (λ i → alg .Algebra-hom.commutes i (a ∷ b ∷ [])) ⟩
      f a y.⋆ (f b y.⋆ y.identity) ≡⟨ ap (f a y.⋆_) y.idr ⟩
      f a y.⋆ f b                  ∎
      where f = alg .Algebra-hom.morphism

The proofs that this is a quasi-inverse is immediate, since both “being an algebra homomorphism” and “being a monoid homomorphism” are properties of the underlying map.

    from∘to : is-right-inverse from comparison.₁
    from∘to x = trivial!

    to∘from : is-left-inverse from comparison.₁
    to∘from x = trivial!

Showing that the functor is essentially surjective is significantly more complicated. We must show that we can recover a monoid from a List algebra (a “fold”): We take the unit element to be the fold of the empty list, and the binary operation $x \star y$ to be the fold of the list $[x,y]$ .

  it's-eso : is-split-eso comparison
  it's-eso (A , alg) = monoid , the-iso where
    open Algebra-on
    open Algebra-hom
    import Cat.Reasoning (Eilenberg-Moore _ (L∘R (Free⊣Forget {ℓ}))) as R

    monoid : Monoids ℓ .Ob
    monoid .fst = A
    monoid .snd .identity = alg .ν []
    monoid .snd ._⋆_ a b = alg .ν (a ∷ b ∷ [])

It suffices, through incredibly tedious calculations, to show that these data assembles into a monoid:

    monoid .snd .has-is-monoid = has-is-m where abstract
      has-is-m : is-monoid (alg .ν []) (monoid .snd ._⋆_)
      has-is-m .has-is-semigroup = record
        { has-is-magma = record { has-is-set = A .is-tr }
        ; associative  = λ {x} {y} {z} →
          alg .ν (⌜ x ⌝ ∷ alg .ν (y ∷ z ∷ []) ∷ [])               ≡˘⟨ ap¡ (happly (alg .ν-unit) x) ⟩
          alg .ν (alg .ν (x ∷ []) ∷ alg .ν (y ∷ z ∷ []) ∷ [])     ≡⟨ happly (alg .ν-mult) _ ⟩
          alg .ν (x ∷ y ∷ z ∷ [])                                 ≡˘⟨ happly (alg .ν-mult) _ ⟩
          alg .ν (alg .ν (x ∷ y ∷ []) ∷ ⌜ alg .ν (z ∷ []) ⌝ ∷ []) ≡⟨ ap! (happly (alg .ν-unit) z) ⟩
          alg .ν (alg .ν (x ∷ y ∷ []) ∷ z ∷ [])                   ∎
        }
      has-is-m .idl {x} =
        alg .ν (alg .ν [] ∷ ⌜ x ⌝ ∷ [])            ≡˘⟨ ap¡ (happly (alg .ν-unit) x) ⟩
        alg .ν (alg .ν [] ∷ alg .ν (x ∷ []) ∷ [])  ≡⟨ happly (alg .ν-mult) _ ⟩
        alg .ν (x ∷ [])                            ≡⟨ happly (alg .ν-unit) x ⟩
        x                                          ∎
      has-is-m .idr {x} =
        alg .ν (⌜ x ⌝ ∷ alg .ν [] ∷ [])            ≡˘⟨ ap¡ (happly (alg .ν-unit) x) ⟩
        alg .ν (alg .ν (x ∷ []) ∷ alg .ν [] ∷ [])  ≡⟨ happly (alg .ν-mult) _ ⟩
        alg .ν (x ∷ [])                            ≡⟨ happly (alg .ν-unit) x ⟩
        x                                          ∎

The most important lemma is that folding a list using this monoid recovers the original algebra multiplication, which we can show by induction on the list:

    recover : ∀ x → fold _ x ≡ alg .ν x
    recover []       = refl
    recover (x ∷ xs) =
      alg .ν (x ∷ fold _ xs ∷ [])               ≡⟨ ap₂ (λ e f → alg .ν (e ∷ f ∷ [])) (sym (happly (alg .ν-unit) x)) (recover xs) ⟩
      alg .ν (alg .ν (x ∷ []) ∷ alg .ν xs ∷ []) ≡⟨ happly (alg .ν-mult) _ ⟩
      alg .ν (x ∷ xs ++ [])                     ≡⟨ ap (alg .ν) (++-idr _) ⟩
      alg .ν (x ∷ xs)                           ∎

We must then show that the image of this monoid under Comparison is isomorphic to the original algebra. Fortunately, this follows from the recover lemma above; The isomorphism itself is given by the identity function in both directions, since the recovered monoid has the same underlying type as the List-algebra!

    into : Algebra-hom _ _ (comparison.₀ monoid) (A , alg)
    into .morphism = λ x → x
    into .commutes = funext (λ x → recover x ∙ ap (alg .ν) (sym (map-id x)))

    from : Algebra-hom _ _ (A , alg) (comparison.₀ monoid)
    from .morphism = λ x → x
    from .commutes =
      funext (λ x → sym (recover x) ∙ ap (fold _) (sym (map-id x)))

    the-iso : comparison.₀ monoid R.≅ (A , alg)
    the-iso = R.make-iso into from (Algebra-hom-path _ refl) (Algebra-hom-path _ refl)