Tag: distributive Laws

Example Laws and Liftings

We have now seen both Kleisli and Eilenberg-Moore laws, and their associated notions of lifted functor. Despite introducing the appropriate definitions, and sketching their key theoretical properties, we haven’t really seen any examples yet. That is the issue we now address.

A standard source of both Kleisli and Eilenberg-Moore laws are the monad morphisms \sigma : \mathbb{S} \rightarrow \mathbb{T}. This can be seen as both

  1. A Kleisli law of type \mathsf{Id} \circ \mathbb{S} \Rightarrow \mathbb{T} \circ \mathsf{Id}.
  2. An Eilenberg-Moore law of type \mathbb{S} \circ \mathsf{Id} \Rightarrow \mathsf{Id} \circ \mathbb{T}.

Therefore, each monad morphism \sigma induces both:

  1. A functor \underline{\mathsf{Id}} : \mathcal{C}_{\mathbb{S}} \rightarrow \mathcal{C}_{\mathbb{T}} such that \underline{\mathsf{Id}} \circ F_{\mathbb{S}} = F_{\mathbb{T}}.
  2. A functor \overline{\mathsf{Id}}: \mathcal{C}^{\mathbb{T}} \rightarrow \mathcal{C}^{\mathbb{S}} such that U_{\mathbb{S}} = U_{\mathbb{T}} \circ \overline{\mathsf{Id}}.

(Notice the difference in direction between the two).

Example: For every monad, the unit \eta : \mathsf{Id} \Rightarrow \mathbb{T} is a monad morphism. For the identity monad there are obvious isomorphisms:

\mathcal{C}_{\mathsf{Id}} \cong \mathcal{C} \cong \mathcal{C}^{\mathsf{Id}}

Up to composition with these isomorphisms, the functor \underline{\mathsf{Id}} : \mathcal{C}_{\mathsf{Id}} \rightarrow \mathcal{C}_{\mathbb{T}} is the usual Kleisli free functor, and the functor \overline{\mathsf{Id}} : \mathcal{C}^{\mathbb{T}} \rightarrow \mathcal{C}^{\mathsf{Id}} is the usual Eilenberg-Moore forgetful functor.

As is a recurring theme, we should always consider what a new feature of monad theory means in terms of algebra.

Example: Consider two equational presentations over the same signature (\Sigma, E), (\Sigma, E') such that E \subseteq E', with respective induced monads \mathbb{S}, \mathbb{T}. Then for a set A, every equivalence class of terms in \mathbb{S}(A) is contained in an equivalence class of terms in \mathbb{T}(A), as the latter theory satisfies more equations. This induces a monad morphism:

\mathbb{S} \Rightarrow \mathbb{T}

The induced functor \overline{\mathsf{Id}} : \mathsf{Set}^{\mathbb{T}} \rightarrow \mathsf{Set}^{\mathbb{S}} picks out the subcategory of \mathbb{T}-algebras (which satisfy more equations), within the larger category of \mathbb{S}-algebras. For example, every commutative monoid is a monoid.

As usual, we can consider the morphisms of \mathsf{Set}_{\mathbb{S}} and \mathsf{Set}_{\mathbb{T}} as families of equivalence classes of terms in the respective theories. From this point of view, every equivalence class in the weaker theory can be promoted to the enclosing one in the stronger theory. This is the behaviour of the induced functor \underline{\mathsf{Id}} : \mathsf{Set}_{\mathbb{S}} \rightarrow \mathsf{Set}_{\mathbb{T}}. For example, the term x + y in the theory of monoids will be mapped to an equivalence class including y + x in the theory of commutative monoids.

We can also find examples beyond monad morphisms to show the greater generality is useful.

Example: For every monad, the multiplication \mu : \mathbb{T} \circ \mathbb{T} \Rightarrow \mathbb{T} is both:

  1. A Kleisli law of type \mathbb{T} \circ \mathbb{T} \Rightarrow \mathsf{Id} \circ \mathbb{T}.
  2. An Eilenberg-Moore law of type \mathbb{T} \circ \mathbb{T} \Rightarrow \mathbb{T} \circ \mathsf{Id}.

Up to the isomorphisms discussed in the earlier example:

  1. The induced functor \underline{\mathbb{T}} : \mathcal{C}_{\mathbb{T}} \Rightarrow \mathcal{C}_{\mathsf{Id}} is the usual Kleisli forgetful functor.
  2. The induced functor \overline{\mathbb{T}} : \mathcal{C}^{\mathsf{Id}} \rightarrow \mathcal{C}^{\mathbb{T}} is the usual Eilenberg-Moore free functor.

Finally, we sketch a key source of examples that needs proper account at a later date.

Example: For a pair of monads \mathbb{S}, \mathbb{T} on the same base category, a natural transformation:

\lambda : \mathbb{S} \circ \mathbb{T} \Rightarrow \mathbb{T} \circ \mathbb{S}

which is simultaneously an Eilenberg-Moore and a Kleisli is known as a distributive law. This is an important notion, introduced by Beck, which allows us to build up monads in a principled way, by composing other monads together. Given such a \lambda, the endofunctor \mathbb{T} \circ \mathbb{S} carries the structure of a monad in a particularly well-behaved way. (In general, composing the underlying functors of two monads can result in a functor that carries no monad structure at all).

The existence of suitable distributive laws allows us to work with monads in a modular fashion. This topic is too important to skim over, so we shall postpone further discussions until more detailed future posts.

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^\mathbb{S}) \circ \lambda_\mathbb{S} \circ \mathbb{T}(\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:

\underline{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: \lambda \circ H(\eta^{\mathbb{S}}) = \eta^{\mathbb{T}}_H.
  2. Multiplication axiom: \lambda \circ H(\mu^{\mathbb{S}}) = \mu^{\mathbb{T}}_H \circ \mathbb{T}(\lambda) \circ \lambda_{\mathbb{S}}.

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.

Acknowledgements: Thanks to Stefania Damato for pointing out three (gulp!) typos in the Eilenberg-Moore and Kleisli law axioms which have now been fixed.