Free monads and their algebras

Today we are interested in the following theorem: The category of algebras of an endofunctor is isomorphic to the category of algebras of its free monad. It sounds complicated (and is rather not precise), so let me explain:

Free monads (arising from algebras). Let $\mathcal{C}$ be a category, $\Sigma$ be an endofunctor on $\mathcal C$ , and $\mathsf{Alg}(\Sigma)$ be the category of $\Sigma$ -algebras. We can define a forgetful functor $U : \mathsf{Alg}(\Sigma) \rightarrow \mathcal C$ as $U (X, f) = X$ on objects, and $U \beta = \beta$ on morphisms. Assume that $U$ has a left adjoint, which we call $F$ . As always in case of adjunctins, a monad arises. We call this monad the free monad generated by $\Sigma$ , and denote it by $\Sigma^*$ .

Free monads are initial algebras. If $\mathcal{C}$ has finite products, we can prove that $\Sigma^*X$ is equal to the initial algebra (if it exists) of the endofunctor $\Sigma(-) + X$ . We name the action of this initial algebra $\xi$ . So, the situation is:

$\Sigma(\mu Y. \Sigma Y + X) + X \stackrel{\xi}{\rightarrow} \mu Y. \Sigma Y + X$ .

We split $\xi$ into two components:

$\eta : X \rightarrow \Sigma^*X$
$\eta = \xi \cdot inr$

$\alpha : \Sigma\Sigma^*X \rightarrow \Sigma^*X$
$\alpha = \xi \cdot inl$

One can prove that $\xi$ (and so $\eta$ and $\alpha$ ) is natural in $X$ .

We can provide another natural transformation, which, intuitively, transforms a $\Sigma$ into its free monad:

$\psi : \Sigma X \rightarrow \Sigma^*X$
$\psi = \alpha \cdot \Sigma \eta$

Moreover, $\eta$ is the unit of the monad $\Sigma^*$ , and $\mu = ( \hspace{-0.8mm} [ \alpha , id ] \hspace{-0.8mm} ) : \Sigma^*\Sigma^* \stackrel{\bullet}{\rightarrow} \Sigma^*$ is the multiplication of the monad.

Eilenberg-Moore algebras. Let $(T, \mu^T, \eta^T)$ be a monad on $\mathcal C$ . We define an (Eilenberg-Moore) $T$ -algebra (aka “for $T$ qua monad”) as an algebra $(X \in \mathsf{Obj}(\mathcal C), f : TX \rightarrow X)$ , where

(1) $TTX \stackrel{\mu^T_X}{\longrightarrow} TX \stackrel{f}{\longrightarrow} X = TTX \stackrel{Tf}{\longrightarrow} TX \stackrel{f}{\longrightarrow} X$

(2) $X \stackrel{\eta^T_X}{\longrightarrow} TX \stackrel{f}{\longrightarrow} X = X \stackrel{\mathit{id}_X}{\longrightarrow} X$

By $\mathsf{EM}(T)$ we denote the category of Eilenberg-Moore $T$ -algebras.

The theorem can now be stated as:

$\mathsf{Alg}(\Sigma)$ is isomorphic to $\mathsf{EM}(\Sigma^*)$ .

Is there any use of such a theorem? It allows us to automatically transfer some properties from the simpler level of $\Sigma$ -algebras to the world of free monads and initial algebras. This theorem will appear at least once more in this blog, so don’t forget about it too soon.

How to prove it? One way is to use Beck’s monadicity theorem (the “evil” version from Mac Lane’s book). It exactly fits the conditions about existence of adjoints, and the unintuitive condition about $\Sigma$ creating coequalizers has a lot to do with (1). But we are (or at least I am) interested in something that can be encoded in Haskell more directly. So, let’s build an explicit isomorphism.

We define two functors (we should actually prove that they are really functors, but you know…):

$J : \mathsf{EM}(\Sigma^*) \rightarrow \mathsf{Alg}(\Sigma)$
$J (X, f : \Sigma^*X \rightarrow X) = (X, f \cdot \psi)$
$J g = g$

$J^{-1} : \mathsf{Alg}(\Sigma) \rightarrow \mathsf{EM}(\Sigma^*)$
$J^{-1} (X, f : \Sigma X \rightarrow X) = (X, ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) )$
$J^{-1} g = g$

To prove the theorem, we show that (A) $J \cdot J^{-1} = Id_{\mathsf{Alg}(\Sigma)}$ and (B) $J^{-1} \cdot J = Id_{\mathsf{EM}(\Sigma^*)}$ . We concentrate on objects, arrows are easy.

$(J \cdot J^{-1}) (X, f) = (X, ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) \cdot \psi)$

Since the functors do not alter the carrier of the algebra, we focus on the action:

$( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) \cdot \psi$

= (def. of $\psi$ )

$( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) \cdot \alpha \cdot \Sigma \eta$

= (def. of $\alpha, \eta$ )

$( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) \cdot \xi \cdot inl \cdot \Sigma \xi \cdot \Sigma inr$

= (computation law)

$[f, id] \cdot (\Sigma ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) + id) \cdot inl \cdot \Sigma \xi \cdot \Sigma inr$

= (sum)

$[f \cdot \Sigma ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) , id \cdot id] \cdot inl \cdot \Sigma \xi \cdot \Sigma inr$

= (inl)

$f \cdot \Sigma ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) \cdot \Sigma \xi \cdot \Sigma inr$

= (comp. law)

$f \cdot \Sigma [ f, id ] \cdot \Sigma(\Sigma ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) + id) \cdot \Sigma inr$

= (sum + inr)

$f \cdot \Sigma id$

= (functor)

$f$

We first calculate:

$f \cdot \psi \cdot \Sigma f$

= (def. of $\psi$ )

$f \cdot \alpha \cdot \Sigma \eta \cdot \Sigma f$

= (naturality of $\eta$ )

$f \cdot \alpha \cdot \Sigma \Sigma^* f \cdot \Sigma \eta$

= (naturality of $\alpha$ )

$f \cdot \Sigma^* f \cdot \alpha \cdot \Sigma\eta$

= (1)

$f \cdot \mu \cdot \alpha \cdot \Sigma\eta$

= (def. of $\mu$ )

$f \cdot ( \hspace{-0.8mm} [ \alpha, id ] \hspace{-0.8mm} ) \cdot \alpha \cdot \Sigma\eta$

= (def. of $\psi$ )

$f \cdot ( \hspace{-0.8mm} [ \alpha, id ] \hspace{-0.8mm} ) \cdot \psi$

= (similarly to A)

$f \cdot \alpha$

We use this result in the following calculation:

$[f \cdot \psi, id] \cdot (\Sigma f + id)$

= (sum)

$[f \cdot \psi \cdot \Sigma f, id \cdot id]$

= (prev. calculation)

$[f \cdot \alpha, id \cdot id]$

= (2)

$[f \cdot \alpha, f \cdot \eta]$

= (sum)

$f \cdot [\alpha, \eta]$

= (def. of $\alpha, \eta$ )

$f \cdot \xi$

We use this result as a premise in the fusion law, hence:

$( \hspace{-0.8mm} [ f \cdot \psi, id ] \hspace{-0.8mm} )$

= (fusion)

$f \cdot ( \hspace{-0.8mm} [ \xi ] \hspace{-0.8mm} )$

= (reflection law)

$f$

We conclude:

$(J^{-1} \cdot J) (X, f) = (X, ( \hspace{-0.8mm} [ f \cdot \psi, id ] \hspace{-0.8mm} )) = (X, f)$

About Maciej Piróg

I am a functional programmer. I believe in large cardinals, axiom of choice, and that "P=NP" will not be solved in my lifetime. I think that category theory is abstract nonsense, and that is why it gives me this Monty-Python-style feeling of amusement.

View all posts by Maciej Piróg →

3 responses to “Free monads and their algebras”

Znawca

February 14, 2013 at 3:57 pm

W jakiej kategorii?

Reply ↓
- Maciej Piróg
  
  February 15, 2013 at 6:56 pm
  
  W każdej kategorii, która ma koprodukty i algebrę początkową opisaną w części “Free monads are initial algebras”
  
  Reply ↓
Znawca

February 25, 2013 at 6:36 pm

aha!

Reply ↓

maciejcs

Free monads and their algebras

About Maciej Piróg

3 responses to “Free monads and their algebras”

Leave a Reply Cancel reply

Pages

Subscribe

Posts so far

maciejcs

Free monads and their algebras

Share this:

Like this:

About Maciej Piróg

3 responses to “Free monads and their algebras”

Leave a Reply Cancel reply

Pages

Subscribe

Posts so far