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.

A.

(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

 

B.

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 these ads
Explore posts in the same categories: Algebra

3 Comments on “Free monads and their algebras”

  1. Znawca Says:

    W jakiej kategorii?


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s


Follow

Get every new post delivered to your Inbox.

%d bloggers like this: