Monads, Laws and Liftings

Now we have seen both the Kleisli and Eilenberg-Moore categories, it is interesting to consider how we might construct “nice” functors between them. To do so, we fix a pair of monads \mathbb{S} : \mathcal{C} \rightarrow \mathcal{C} and \mathbb{T} : \mathcal{D} \rightarrow \mathcal{D}, and a functor

H : \mathcal{C} \rightarrow \mathcal{D}

We shall then consider the Eilenberg-Moore and Kleisli constructions separately.

Eilenberg-Moore Laws

Can we construct a functor \overline{H} : \mathcal{C}^{\mathbb{S}} \rightarrow \mathcal{D}^{\mathbb{T}} in some natural way? This question gives us a bit too much freedom to narrow things down, so we restrict attention to functors that interact well with the forgetful functors, in that:

U^{\mathbb{T}} \circ \overline{H} = H \circ U^{\mathbb{S}}

We shall call such a functor an Eilenberg-Moore lifting of H. The condition above means

\overline{H}(A, \mathbb{S}(A) \xrightarrow{\alpha} A) = (H(A), \mathbb{T}(H(A)) \xrightarrow{\alpha'} H(A)) \qquad \overline{H}(h) = H(h)

Where we must determine a suitable \alpha'. Applying H to \alpha as an obvious first step yields:

H(\mathbb{S}(A)) \xrightarrow{H(\alpha)} H(A)

The domain is of the wrong type. If we had a morphism

\lambda : \mathbb{T}(H(A)) \rightarrow H(\mathbb{S}(A))

we could form a composite of the right type:

\mathbb{T}(H(A)) \xrightarrow{\lambda} H(\mathbb{S}(A)) \xrightarrow{H(\alpha)} H(A)

To do this uniformly for all Eilenberg-Moore algebras, we require \lambda be natural in A. The action of \overline{H} on objects is then:

(A,\alpha) \mapsto (H(A), H(\alpha) \circ \lambda_A)

If we attempt to establish the resulting structure map satisfies the unit and multiplication axioms, we find that \lambda must interact well with the monad structures, in that the following two axioms hold:

  1. Unit axiom: H(\eta^{\mathbb{S}}) = \lambda \circ \eta^{\mathbb{T}}_H.
  2. Multiplication axiom: \lambda \circ \mu^{\mathbb{T}}_H = H(\mu^{S}) \circ \lambda_H \circ H(\lambda).

Such a \lambda satisfying these axioms is referred to as an Eilenberg-Moore law. In fact, there is a bijective correspondence between:

  1. Eilenberg-Moore liftings of H
  2. Eilenberg-Moore laws \mathbb{T} \circ H \Rightarrow H \circ \mathbb{S}.

Verifying this is a bit fiddly, but routine once you figure out how to construct the components of an Eilenberg-Moore law from a lifting. We shall skip the details.

Kleisli Laws

We now consider how to lift H to a functor \underline{H} : \mathcal{C}_{\mathbb{S}} \rightarrow \mathcal{D}_{\mathbb{T}}. Again, we need to constrain the problem further. In this case it turns out to be best to consider functors that interact well with the free constructions, in that:

\overline{H} \circ F^{\mathbb{S}} = F^{\mathbb{T}} \circ H

We shall call such a functor a Kleisli lifting of H. The condition above forces that:

\underline{H}(A) = A \qquad \underline{H}(f : A \xrightarrow{f} \mathbb{S}(B)) = H(A) \xrightarrow{f'} \mathbb{T}(H(A))

Where it remains to determine a suitable f'. Having seen the drill for the Eilenberg-Moore construction, an intuitive plan is to form a composite:

H(A) \xrightarrow{H(f)} H(\mathbb{S}(A)) \xrightarrow{\lambda_A} \mathbb{T}(H(B))

for some natural transformation \lambda : H \circ \mathbb{S} \Rightarrow \mathbb{T} \circ H. Of course, we need to verify that this mapping is functorial. In doing so, we find the need for the following axioms:

  1. Unit axiom: \eta^{\mathbb{T}}_H = H(\eta^{\mathbb{S}}).
  2. Multiplication axiom: \lambda \circ H(\mu^{\mathbb{S}}) = \mu^{\mathbb{T}} \circ H(\lambda) \circ \lambda_H.

Such a \lambda is referred to as a Kleisli law. As we might expect from the previous construction, there is a bijection between:

  1. Kleisli liftings of H.
  2. Kleisli laws H \circ \mathbb{S} \Rightarrow \mathbb{T} \circ H.

Again, the proof requires a little bit of creativity to construct the components of a Kleisli law from a given lifting, and makes an instructive exercise.

There is also rather pleasing duality between the two results.

Leave a Reply

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

You are commenting using your 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 )

Connecting to %s

%d bloggers like this: