module Algebra.Monoid.Category where
open Precategory open is-semigroup open is-monoid open is-magma open Monoid-hom open Monoid-on open Functor open _=>_ open _⊣_ private map : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → B) → List A → List B map = Meta.Idiom.map
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.
Mon↪Sets : ∀ {ℓ} → Functor (Monoids ℓ) (Sets ℓ) Mon↪Sets = Forget-structure (Monoid-structure _)
Free monoids🔗
We piece together some properties of lists to show that, if
is a set, then
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
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-monoid : ∀ {ℓ} → Functor (Sets ℓ) (Monoids ℓ) Free-monoid .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-monoid .F₁ f = total-hom (map f) record { pres-id = refl ; pres-⋆ = map-++ f } Free-monoid .F-id = ext map-id Free-monoid .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-monoid⊣Forget : ∀ {ℓ} → Free-monoid {ℓ} ⊣ Mon↪Sets Free-monoid⊣Forget .unit .η _ x = x ∷ [] Free-monoid⊣Forget .unit .is-natural x y f = refl Free-monoid⊣Forget .counit .η M = total-hom (fold _) record { pres-id = refl ; pres-⋆ = fold-++ } Free-monoid⊣Forget .counit .is-natural x y th = ext $ fold-natural (th .hom) (th .preserves) Free-monoid⊣Forget .zig {A = A} = ext $ fold-pure {X = A} Free-monoid⊣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-monoid⊣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-monoid⊣Forget {ℓ}) Monoid-is-monadic {ℓ} = ff+split-eso→is-equivalence it's-ff it's-eso where open import Cat.Diagram.Monad comparison = Comparison-EM (Free-monoid⊣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 .hom from alg .preserves .pres-id = happly (alg .preserves) [] 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 .preserves 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 .hom
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 to be the fold of the list
it's-eso : is-split-eso comparison it's-eso (A , alg) = monoid , the-iso where open Algebra-on import Cat.Reasoning (Eilenberg-Moore (R∘L (Free-monoid⊣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 .hom = λ x → x into .preserves = funext (λ x → recover x ∙ ap (alg .ν) (sym (map-id x))) from : Algebra-hom _ (A , alg) (comparison.₀ monoid) from .hom = λ x → x from .preserves = 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 trivial! trivial!