(cache) What is the correct definition of ideal monads?

This was the third and final lunch in my series about ideal monads. I talked about how to define ideal monads correctly. My talk was based on a discussion with Tarmo Uustalu.

One bad and one good definition

There is a common definition of ideal monads, which is used, for example, in the paper Coproducts of Ideal Monads by Neil Ghani and Tarmo. This definition basically says that a pair $(T', \mu')$ as introduced in the previous lunch is an ideal monad, if the derived triple $(T, \eta, \mu)$ is a monad.

Definition 1 Let $\mathcal C$ be a category with coproducts, and assume that $T' : \mathcal C \to \mathcal C$ , $T = \mathrm{Id} + T'$ , $\mu' : T'T \to T'$ , $\eta = \iota_1 : \mathrm{Id} \to T$ , and $\mu = [\mathrm{id}_T, \iota_2\mu'] : TT \to T$ . The pair $(T', \mu')$ is an ideal monad if and only if $(T, \eta, \mu)$ is a monad.

Unfortunately, this definition does not give us an equation that constrains the choice of $\mu'$ . So we develop another definition, which contains such an equation.

Definition 2 Let $\mathcal C$ be a category with coproducts, and assume that $T' : \mathcal C \to \mathcal C$ , $T = \mathrm{Id} + T'$ , $\mu' : T'T \to T'$ , $\eta = \iota_1 : \mathrm{Id} \to T$ , and $\mu = [\mathrm{id}_T, \iota_2\mu'] : TT \to T$ . The pair $(T', \mu')$ is an ideal monad if and only if

$\mu'(T'\eta) = \mathrm{id}_{T'} : T' \to T'$

and

$\mu'(\mu'T) = \mu'(T'\mu) : T'TT \to T'$ .

It is easy to show that an ideal monad according to Definition 2 is also an ideal monad according to Definition 1. It is not so obvious whether the converse is also true. Let us check. We assume that $(T', \mu')$ is an ideal monad according to Definition 1. This means that the derived triple $(T, \eta, \mu)$ is a monad, that is, the three monad equations for $\eta$ and $\mu$ hold. We have the following situation:

The equation

$\mu(\eta T) = \mathrm{id}_T : T \to T$

tells us nothing that we would not already know, since

$\mu(\eta T) = [\mathrm{id}_T, \iota_2\mu'](\iota_1T) = \mathrm{id}_T$

follows from the coproduct definition.
The equation

$\mu(T\eta) = \mathrm{id}_T : T \to T$

is more interesting. We have

$\begin{array}{rcl} \mu(T\eta) & = & \mu(\eta + T'\eta) \\ & = & [\mathrm{id}_T, \iota_2\mu'](\iota_1 + T'\eta) \\ & = & [\iota_1, \iota_2\mu'(T'\eta)] \end{array}$

and

$\mathrm{id}_T = [\iota_1, \iota_2]$ .

So the above monad equation is equivalent to

$\iota_2\mu'(T'\eta) = \iota_2 : T' \to T$ .

From this, we can derive the desired equation

$\mu'(T'\eta) = \mathrm{id}_{T'} : T' \to T'$

if $\iota_2 : T' \to T$ is a monomorphism. Unfortunately, this is not the case in general.
Let us finally look at the equation

$\mu(\mu T) = \mu(T\mu) : TTT \to T$ .

We have

$\begin{array}{rcl} \mu(\mu T) & = & \mu[\mathrm{id}_{TT}, \iota_2(\mu'T)] \\ & = & [\mu, \mu\iota_2(\mu'T)] \\ & = & [\mu, [\mathrm{id}_T, \iota_2\mu']\iota_2(\mu'T)] \\ & = & [\mu, \iota_2\mu'(\mu'T)] \end{array}$

and

$\begin{array}{rcl} \mu(T\mu) & = & \mu(\mu + T'\mu) \\ & = & [\mathrm{id}_T, \iota_2\mu'](\mu + T'\mu) \\ & = & [\mu, \iota_2\mu'(T'\mu)] \end{array}$ .

So the above monad equation is equivalent to

$\iota_2\mu'(\mu'T) = \iota_2\mu'(T'\mu) : T'TT \to T$ .

If $\iota_2 : T' \to T$ is a monomorphism, we can derive the desired equation

$\mu'(\mu'T) = \mu'(T'\mu) : T'TT \to T'$ .

So if $\iota_2 : T' \to T$ is monic, Definition 1 guarantees that the desired equations for $\mu'$ hold, but in general, this guarantee cannot be derived from Definition 1. So I consider Definition 1 inappropriate and regard Definition 2 as a correct definition of ideal monads. Tarmo shares this view.

A third definition

There is yet another definition of ideal monads, which is used by Stefan Milius in his paper On Iteratable Endofunctors. This definition is equivalent to Definition 1, except that it requires $(T', \iota_2)$ to be a subfunctor of $T$ .

Definition 3 An ideal monad is a pair $(T', \mu')$ that is an ideal monad according to Definition 1 and for which $(T', \iota_2)$ is a subfunctor of $\mathrm{Id} + T'$ .

By definition, $(T', \iota_2)$ is a subfunctor of $T$ if and only if for every $A \in \mathrm{Ob}(\mathcal C)$ , $\iota_2 : T'A \to TA$ is monic. If this is the case, then also the natural transformation $\iota_2 : T' \to T$ is monic. Therefore, an ideal monad according to Definition 3 is also an ideal monad according to Definition 2. The converse is not true, since we cannot expect $(T', \iota_2)$ to be a subfunctor for every $(T', \mu')$ that is an ideal monad according to Definition 2.

In $\mathbf{Set}$ as well as in $\mathbf{Hask}$ , all injections are monic. So Definition 3 might still seem to be okay. However, Definition 3 does not lead to a good definition of ideal comonads, which are the duals of ideal monads. The duals of injections are projections, and the duals of monomorphisms are epimorphisms. So a definition of ideal comonads that is analog to Definition 3 would require the relevant projections to be epic. In the case of $\mathbf{Set}$ , the epimorphisms are the surjective functions. However, projections $\pi_2 : \emptyset \times A \to A$ are not surjective for $A \neq \emptyset$ .

Mistakes in my MFPS ’12 paper

I have to admit that I used Definition 1 instead of Definition 2 in my paper Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming. And I made a few further mistakes, which are similar:

I defined ideal comonads analogously to Definition 1 instead of Definition 2.
I made an analogous mistake in the definition of $\mathcal U'$ -strong ideal monads. An ideal monad $(T', \mu')$ should be called strong with respect to an ideal cartesian comonad $(U', \delta', m', n')$ if and only if there is a natural transformation $s'$ with

$s' : U'A \times T'B \to T'(UA \times B)$

for which certain equations hold. However, I did not require these equations to hold, but required that the monad induced by $(T', \mu')$ and a certain natural transformation induced by $s'$ together form a $\mathcal U$ -strong monad, where $\mathcal U$ is the cartesian comonad induced by $(U', \delta', m', n')$ .
I made a similar mistake in the definition of temporal categories, which are models of an intuitionistic temporal logic and a flavor of FRP. A temporal category covers an ideal monad $(\Diamond', \mu')$ , from which we can infer a monad $(\Diamond, \eta, \mu)$ . To ensure that time is linear, I required that if we define $\odot$ and $\varpi_i$ by the equations

$\begin{array}{rcl} A \odot B & = & A \times B + A \times \Diamond'B + \Diamond'A \times B \\ \varpi_i & = & [\iota_1\pi_i, \iota_i\pi_i, \iota_{1 - i}\pi_i] \end{array}$ ,

then $\odot$ is a product in the Kleisli category of $(\Diamond, \eta, \mu)$ with projections $\varpi_1$ and $\varpi_2$ . This is equivalent to requiring that

$\langle\mu_A(\Diamond\varpi_1), \mu_B(\Diamond\varpi_2)\rangle : \Diamond(A \odot B) \to \Diamond A \times \Diamond B$

is an isomorphism. However, we actually want the existence of an isomorphism

$\Diamond'(A \odot B) \cong \Diamond' A \times \Diamond' B$

with a definition similar to the above one, from which the above isomorphism property can be deduced.

I intend to present a corrected definition of temporal categories and the constructs they are based upon in a future paper.

One thought on “What is the correct definition of ideal monads?”

Pingback: Three talks about ideal monads « Wolfgang Jeltsch

Theory Lunch

Institute of Cybernetics, Tallinn

What is the correct definition of ideal monads?

One bad and one good definition

A third definition

Mistakes in my MFPS ’12 paper

One thought on “What is the correct definition of ideal monads?”

Leave a Reply Cancel reply

One bad and one good definition

A third definition

Mistakes in my MFPS ’12 paper

Share this:

Like this:

Related

One thought on “What is the correct definition of ideal monads?”

Leave a Reply Cancel reply