1 Introduction

Distributive laws were introduce by Jon Beck [1], they provide a canonical way to compose monads and also allow to lift functors/monads to the category of algebras for a functor/monad. The classical example is the distributive law of product over addition which defines a distributive law of the free monoid monad over the free abelian group monad. This distributive law allows to compose those two monads in order to obtain the free ring monad.

Distributive laws of a functor/monad over the powerset (monad) are of particular interest in computer science and category theory. In computer science, they are studied in automata theory [9], the so-called powerset construction or determinization, and in (guarded) structural operational semantics [10], SOS and GSOS. In category theory, they are of particular interest in the subject of relation lifting [5, 7].

There are well-known canonical laws over the powerset, such as the distributive law of the free monoid monad over the powerset monad given by the law \(A\cdot B\mapsto \{\, a\cdot b\mid a\in A,b\in B \,\}\). Such a canonical law over the powerset can be defined for any functor [5, Section 4] but in general is not a natural transformation. If the functor preserves weak pullbacks this canonical law is a natural transformation and it is distributive law of the functor over the powerset monad [5]. Additionally, if the functor has a monad structure in which the unit and the multiplication are weakly cartesian, meaning that each naturality square is a weak pullback, then this law is a distributive law between monads.

From the perspective of universal algebra, the previous canonical law, that lifts a basic operation to its subsets by choosing elements in each subset and then applies the basic operation, provides the construction of power algebras (also known as complex algebras or global algebras) [3, 4]. It is well-know that such construction only preserves regular linear identities [3, Theorem 5]. In particular, the non-linear axiom \(x\vee (x\wedge y)=x\) of absorption in the theory of lattices is not preserved. As a consequence, the previous canonical law is not a distributive law of the lattice monad over the powerset monad (in fact, it is not even a natural transformation!). Nevertheless, this does not rule out the existence of a distributive law of the free lattice monad over the powerset monad. In this paper, we show that there is no distributive law of the free lattice monad over the powerset monad and between some variants of them.

2 Preliminaries

Throughout this paper we work only in the category \({{\,\mathrm{Set}\,}}\) of sets and functions. A monad \((T,\eta ,\mu )\) (see [8, Chapter VI] for more details) is an endofunctor T together with natural transformations \(\eta :\mathrm {id}\Longrightarrow T\) (the unit) and \(\mu :TT\Longrightarrow T\) (the multiplication) such that the following diagrams commute:

figure a

The powerset monad \((\mathcal {P},\widehat{\eta },\widehat{\mu })\) is defined so that \(\mathcal {P}X\) is the set of all subsets of X, and:

$$\begin{aligned} \widehat{\eta }_X(x)=\{\, x \,\}, \qquad \widehat{\mu }_X(\Phi ) = \bigcup \Phi \qquad \text {for } x\in X, \Phi \subseteq \mathcal {P}X. \end{aligned}$$

As a source of examples for monads on \({{\,\mathrm{Set}\,}}\) we have the ones that are induced by equational theories [8, Chapter VI Section 8]. For instance, monoids, groups, rings, vector spaces, lattices and so on.

A lattice is an algebra on the signature \(\{\, \wedge ,\vee \,\}\), where \(\wedge \) and \(\vee \) are both binary operation symbols, that satisfies the following equations:

figure b

We denote by \((\mathcal {L},\eta ,\mu )\) the free lattice monad. That is, \(\mathcal {L}X\) is the underlying set of the free lattice on X, which is the set TX of terms over X on the signature \(\{\, \wedge ,\vee \,\}\) modulo the equational theory induced by the lattice axioms. The unit \(\eta _X\) maps an element \(x\in X\) to its equivalence class \(\eta _X(x)\) and the multiplication “flattens”, in a canonical way, each equivalence class whose parameters are also equivalence classes into a single equivalence class. Explicitly, if we use brackets to denote equivalence classes on TX, then \(\eta _X(x)=[x]\) and \(\mu _X\Big (\big [t([s_1],\dots ,[s_n])\big ]\Big )=[t(s_1,\dots ,s_n)]\), for \(x\in X\) and terms \(t,s_1,\dots ,s_n\) on the signature \(\{\, \wedge ,\vee \,\}\). In the sequel, we omit brackets for equivalence classes and only work with (canonical) representatives.

It is worth mentioning that the functor \(\mathcal {L}\) does not preserve weak pullbacks. Indeed, if we consider the pullback square

figure c

where \(g(x)=a\), \(f(x)=f(y)=a\) and \(f(z)=b\), then \(\mathcal {L}f(x\wedge (y\vee z))=a=\mathcal {L}g(x)\), but there is no \(t\in \mathcal {L}\{\, (x,x),(x,y) \,\}\) such that \(\mathcal {L}\pi _2(t)=x\wedge (y\vee z)\). Furthermore, \(\eta \) is not weakly cartesian since, for the same f as above, \(\mathcal {L}f(x\wedge (y\vee z))=a=\eta _{\{\, a,b \,\}}(a)\), but there is no \(w\in \{\, x,y,z \,\}\) such that \(\eta _{\{\, x,y,z \,\}}(w)=x\wedge (y\vee z)\). This implies that the canonical law \(\lambda _X:\mathcal {L}\mathcal {P}X\rightarrow \mathcal {P}\mathcal {L}X\) defined in [5, Section 4] is not a natural transformation.

Let S and T be endofunctors on the category \({{\,\mathrm{Set}\,}}\). A natural transformation \(\lambda :TS\Longrightarrow ST\) is called a distributive law of T over S. Additionally, if \(\eta ^S:\mathrm {id}_{{{\,\mathrm{Set}\,}}}\Longrightarrow S\) and \(\eta ^T:\mathrm {id}_{{{\,\mathrm{Set}\,}}}\Longrightarrow T\) are natural transformations, we can ask whether the following unit laws hold or not:

figure d

Similarly, if \(\mu ^S:SS\Longrightarrow S\) and \(\mu ^T:TT\Longrightarrow T\) are natural transformations, we can also ask whether the following multiplication laws hold or not:

figure e

Depending on the laws that \(\lambda :TS \Longrightarrow ST\) satisfies, we include the respective natural transformations when mentioning a distributive law. For instance, a distributive law of \((T,\eta ^T)\) over \((S,\mu ^S)\) is a natural transformation \(\lambda :TS\Longrightarrow ST\) that satisfies the unit law (\(\mathtt {U}_2\)) for \(\eta ^T\) and the multiplication law (\(\mathtt {M}_1\)) for \(\mu ^S\), that is, \(\lambda \circ \eta ^T_S=S\eta ^T\) and \(\lambda \circ T\mu ^S=\mu ^ST\circ S\lambda \circ \lambda S\), respectively.

3 Lattices do not distribute over powerset

The main purpose of this section is to show the following.

Theorem 3.1

There is no distributive law of the free lattice monad \((\mathcal {L},\eta ,\mu )\) over the powerset monad \((\mathcal {P},\widehat{\eta },\widehat{\mu })\).

A key property that we use in our proof is the the following.

Lemma 3.2

Let \(\mathcal {V}\) be a lattice variety such that the two element linear order \(\mathbf {2}\) is in \(\mathcal {V}\) and let \(F_\mathcal {V}(X)\) the free lattice of \(\mathcal {V}\) generated by X. If X is the disjoint union of Y and Z, F(Y) is the filter of \(F_\mathcal {V}(X)\) generated by Y and I(Z) is the ideal of \(F_\mathcal {V}(X)\) generated by Z, then \(F_\mathcal {V}(X)\) is the disjoint union of F(Y) and I(Z).

Proof

It follows from [2, Lemma 1.2] and [2, Lemma 1.4. (4)]. \(\square \)

Varieties for which we can apply the previous lemma include: lattices, distributive lattices, modular lattices and their bounded versions, among others. The proof of Theorem 3.1 we present depends only on the lattice axioms and the conclusion of the previous lemma. Hence, Theorem 3.1 also holds if we consider, instead of the free lattice monad, any monad associated to a lattice variety containing \(\mathbf {2}\). For the sake of simplicity we do the proof for the monad \((\mathcal {L},\eta ,\mu )\) and state in Theorem 3.7 its generalization.

Throughout this section, \((\mathcal {P},\widehat{\eta },\widehat{\mu })\) denotes the powerset monad and \((\mathcal {L},\eta ,\mu )\) denotes the free lattice monad.

If \(\lambda :\mathcal {L}\mathcal {P}\Longrightarrow \mathcal {P}\mathcal {L}\) is a distributive law of the free lattice monad over the powerset monad, then for every set Y and elements \(y_1,y_2\in Y\) we have

$$\begin{aligned}&\lambda _Y(\{\, y_1,y_2 \,\})=\{\, y_1,y_2 \,\}\text { and} \end{aligned}$$
(3.1a)
$$\begin{aligned}&\lambda _Y(\{\, y_1 \,\}\wedge \{\, y_2 \,\})=\{\, y_1\wedge y_2 \,\}, \end{aligned}$$
(3.1b)

by the axioms (\(\mathtt {U}_2\)) and (\(\mathtt {U}_1\)) involving \(\eta \) and \(\widehat{\eta }\), respectively.

We have the following properties for the elements in \(\lambda \big (\{\, v,w \,\}\wedge \{\, x,y \,\}\big )\).

Lemma 3.3

Let \(\lambda :\mathcal {L}\mathcal {P}\Longrightarrow \mathcal {P}\mathcal {L}\) be a distributive law of \((\mathcal {L},\eta )\) over \((\mathcal {P},\widehat{\eta })\) and let \(X=\{\, v,w,x,y \,\}\). Then,

  1. (1)

    there exists \({\hat{s}}(v,w,x,y)\in \lambda _X(\{\, v,w \,\}\wedge \{\, x,y \,\})\) such that \({\hat{s}}(v,w,v,w)=v\).

Let \(s(v,w,x,y)\in \lambda _X(\{\, v,w \,\}\wedge \{\, x,y \,\})\), then

  1. (2)

    \(s(v,w,x,y)\le v\vee w\) and \(s(v,w,x,y)\le x\vee y\),

  2. (3)

    if \(s(v,w,v,w)=v\) then \(s(v,w,x,y)\ge v\wedge x\).

Proof

(1) follows by naturality of \(\lambda \) using the function \(g:X\rightarrow \{\, v,w \,\}\) such that \(g(v)=g(x)=v\) and \(g(w)=g(y)=w\), and by applying (3.1a).

To prove \(s(v,w,x,y)\le v\vee w\) in (2), consider the filter \(F(x,y)\subseteq \mathcal {L}X\) generated by \(\{\, x,y \,\}\) and the ideal \(I(v,w)\subseteq \mathcal {L}X\) generated by \(\{\, v,w \,\}\). By Lemma 3.2, \(\mathcal {L}X\) is the disjoint union of F(xy) and I(vw), hence either \(s(v,w,x,y)\in F(x,y)\) or \(s(v,w,x,y)\in I(v,w)\). In the former case, we obtain \(s(v,w,x,y)\ge x\wedge y\) and, by using naturality of \(\lambda \) with the function \(f:X\rightarrow \{\, v,x \,\}\) such that \(f(v)=f(w)=v\) and \(f(x)=f(y)=x\) plus (3.1b), we obtain \(v\wedge x=s(v,v,x,x)\ge x\), a contradiction. Therefore, \(s(v,w,x,y)\in I(v,w)\), which means that \(s(v,w,x,y)\le v\vee w\), as we wanted to prove. To prove \(s(v,w,x,y)\le x\vee y\) in (2), consider the filter \(F(v,w)\subseteq \mathcal {L}X\) generated by \(\{\, v,w \,\}\) and the ideal \(I(x,y)\subseteq \mathcal {L}X\) generated by \(\{\, x,y \,\}\) and proceed in a similar way as in the proof of \(s(v,w,x,y)\le v\vee w\).

To prove (3), assume that \(s(v,w,v,w)=v\). Then, by considering the partition of \(\mathcal {L}X\) given by the filter F(vx) and the ideal I(wy) we have that either \(s(v,w,x,y)\in F(v,x)\) or \(s(v,w,x,y)\in I(w,y)\). In the latter case, we obtain \(s(v,w,x,y){\le } w\vee y\) and this implies \(v{=}s(v,w,v,w)\le w\), a contradiction. Therefore, \(s(v,w,x,y){\in } F(v,x)\), which means that \(s(v,w,x,y){\ge } v\wedge x\). \(\square \)

We have the following dual version of the previous lemma.

Lemma 3.4

Let \(\lambda :\mathcal {L}\mathcal {P}\Longrightarrow \mathcal {P}\mathcal {L}\) be a distributive law of \((\mathcal {L},\eta )\) over \((\mathcal {P},\widehat{\eta })\) and let \(X=\{\, v,w,x,y \,\}\). Then,

  1. (1)

    there exists \({\tilde{s}}(v,w,x,y)\in \lambda _X(\{\, v,w \,\} \vee \{\, x,y \,\})\) such that \({\tilde{s}}(v,w,v,w)=v\).

Let \(s(v,w,x,y)\in \lambda _X(\{\, v,w \,\}\vee \{\, x,y \,\})\), then

  1. (2)

    \(s(v,w,x,y)\ge v\wedge w\) and \(s(v,w,x,y)\ge x\wedge y\),

  2. (3)

    if \(s(v,w,v,w)=v\) then \(s(v,w,x,y)\le v\vee x\).

Proof

Dual proof of Lemma 3.3. \(\square \)

The previous three lemmas are the main tool that we use in the sequel.

Our next step is to characterize the set \(\lambda (\{\, a,b \,\}\wedge \{\, a \,\})\) and the set \(\lambda (\{\, a,b \,\}\vee \{\, a \,\})\).

Lemma 3.5

Let \(\lambda :\mathcal {L}\mathcal {P}\Longrightarrow \mathcal {P}\mathcal {L}\) be a distributive law of \((\mathcal {L},\eta ,\mu )\) over \((\mathcal {P},\widehat{\eta })\) and let \(B=\{\, a,b \,\}\). Then:

$$\begin{aligned} \lambda _B(B\wedge \{\, a \,\})=\{\, a,b\wedge a \,\} \ \ \text { and }\ \ \lambda _B(B\vee \{\, a \,\})=\{\, a,b\vee a \,\}. \end{aligned}$$

Proof

Let \(X=\{\, v,w,x,y \,\}\). Then, by naturality of \(\lambda \), using the onto function \(f:X\rightarrow B\) such that \(f(v)=f(x)=f(y)=a\) and \(f(w)=b\), we have:

$$\begin{aligned} \lambda _B(B\wedge \{\, a \,\})=\{\, s(a,b,a,a)\mid s(v,w,x,y)\in \lambda _X(\{\, v,w \,\}\wedge \{\, x,y \,\}) \,\}. \end{aligned}$$

Now, by using item (2) from Lemma 3.3, we obtain that each s(abaa) in \(\lambda _B(B\wedge \{\, a\,\})\) satisfies \(s(a,b,a,a)\le a\vee a=a\) in \(\mathcal {L}B\), where \(\mathcal {L}B\) is the free lattice on two generators. Since \(\mathcal {L}B\) has only four elements, namely, a, b, \(a\vee b\) and \(a\wedge b\), and the only ones less than or equal to a are a and \(a\wedge b\) then \(\lambda _B(B\wedge \{\, a \,\})\subseteq \{\, a,a\wedge b \,\}\). Furthermore, by using the term \({\hat{s}}\) of Lemma 3.3 together with (3) of that lemma we have \({\hat{s}}(a,b,a,a)\ge a\), which implies \(a\in \lambda _B(B\wedge \{\, a \,\})\). Hence

$$\begin{aligned} \{\, a \,\}\subseteq \lambda _B(B\wedge \{\, a \,\})\subseteq \{\, a,a\wedge b \,\}. \end{aligned}$$

A dual argument, by using Lemma 3.4 instead of Lemma 3.3, gives us

$$\begin{aligned} \{\, a \,\}\subseteq \lambda _B(B\vee \{\, a \,\})\subseteq \{\, a,a\vee b \,\}. \end{aligned}$$

Therefore, we have the following cases:

  1. (1)

    \(\lambda _B(B\wedge \{\, a \,\})=\{\, a \,\}\) and \(\lambda _B(B\vee \{\, a \,\})=\{\, a \,\}\).

  2. (2)

    \(\lambda _B(B\wedge \{\, a \,\})=\{\, a \,\}\) and \(\lambda _B(B\vee \{\, a \,\})=\{\, a,a\vee b \,\}\).

  3. (3)

    \(\lambda _B(B\wedge \{\, a \,\})=\{\, a,a\wedge b \,\}\) and \(\lambda _B(B\vee \{\, a \,\})=\{\, a \,\}\).

  4. (4)

    \(\lambda _B(B\wedge \{\, a \,\})=\{\, a,a\wedge b \,\}\) and \(\lambda _B(B\vee \{\, a \,\})=\{\, a,a\vee b \,\}\).

Note that by using the axiom (\(\mathtt {M}_2\)) involving \(\mu \), if we let \(t(x,y)=x\vee y\), we have:

$$\begin{aligned} \lambda _B\circ \mu _{\mathcal {P}B} (t(B,B\wedge \{\, a \,\}))=\mathcal {P}\mu _B\circ \lambda _{\mathcal {L}B}\circ \mathcal {L}\lambda _B(t(B,B\wedge \{\, a \,\})) \end{aligned}$$

but using the absorption law we can calculate the left hand side as follows:

$$\begin{aligned} \lambda _B\circ \mu _{\mathcal {P}B} \big (t(B,B\wedge \{\, a \,\})\big )=\lambda _B\big ( B\vee (B\wedge \{\, a \,\})\big )=\lambda _B(B)\overset{(3.1a)}{=}B, \end{aligned}$$

which implies

$$\begin{aligned} \mathcal {P}\mu _B\circ \lambda _{\mathcal {L}B}\circ \mathcal {L}\lambda _B(t(B,B\wedge \{\, a \,\}))=B. \end{aligned}$$
(3.2)

Now, case (1) cannot happen since we would obtain

$$\begin{aligned} \mathcal {P}\mu _B\circ \lambda _{\mathcal {L}B}\circ \mathcal {L}\lambda _B \big (t(B,B\wedge \{\, a \,\})\big )&=\mathcal {P}\mu _B\circ \lambda _{\mathcal {L}B}\Big (t\big (\lambda _B(B),\lambda _B(B\wedge \{\, a \,\})\big )\Big )\\&=\mathcal {P}\mu _B\circ \lambda _{\mathcal {L}B}\big (t(B,\{\, a \,\})\big )\\&=\mathcal {P}\mu _B\circ \lambda _{\mathcal {L}B}(B\vee \{\, a \,\})\\&=\mathcal {P}\mu _B(\{\, a \,\})\\&=\{\, a \,\} \end{aligned}$$

which contradicts (3.2). Similarly, case (2) cannot happen since it would give us \(B=\{\, a,a\vee b \,\}\), a contradiction. A dual argument to that of case (2) shows that (3) cannot happen either. Therefore, we are left with case (4) and the proof is finished. \(\square \)

Our last lemma is the following.

Lemma 3.6

Let \(\lambda :\mathcal {L}\mathcal {P}\Longrightarrow \mathcal {P}\mathcal {L}\) be a distributive law of \((\mathcal {L},\eta ,\mu )\) over \((\mathcal {P},\widehat{\eta },\widehat{\mu })\) and let \(C=\{\, a,b,c \,\}\). Then, \(a\wedge b\wedge c\in \lambda _C(\{\, a,b \,\}\wedge \{\, c \,\})\).

Proof

Let \(X=\{\, v,w,x,y \,\}\) and \(B=\{\, a,b \,\}\). By naturality of \(\lambda \), using the onto function \(g:X\rightarrow C\) such that \(g(v)=a\), \(g(w)=b\), and \(g(x)=g(y)=c\), we obtain:

$$\begin{aligned} \lambda _C(B\wedge \{\, c \,\})=\{\, s(a,b,c,c)\mid s(v,w,x,y)\in \lambda _X(\{\, v,w \,\}\wedge \{\, x,y \,\}) \,\}. \end{aligned}$$

Note that by item (2) from Lemma 3.3 each s(abcc) in the previous set satisfies

$$\begin{aligned} s(a,b,c,c)\le c. \end{aligned}$$
(3.3)

Now, by Lemma 3.5 and naturality of \(\lambda \), using the onto function \(f :X\rightarrow B\) such that \(f(v)=f(x)=f(y)=a\) and \(f(w)=b\), we have:

$$\begin{aligned} \{\, a,a\wedge b \,\}&=\lambda _B(B\wedge \{\, b \,\})\\&=\{\, s(a,b,a,a)\mid s(v,w,x,y)\in \lambda _X(\{\, v,w \,\}\wedge \{\, x,y \,\})\}. \end{aligned}$$

Thus, there exists \(s'(v,w,x,y)\in \lambda _X(\{\, v,w \,\}\wedge \{\, x,y \,\})\) such that \(s'(a,b,a,a)=a\wedge b\). Consider the partition of \(\mathcal {L}C\) given by F(ac) and I(b). If \(s'(a,b,c,c)\in F(a,c)\) then \(a\wedge c\le s'(a,b,c,c)\) which implies \(a\le s'(a,b,a,a)=a\wedge b\), a contradiction. Therefore, \(s'(a,b,c,c)\in I(b)\), that is, \(s'(a,b,c,c)\le b\), which together with (3.3) implies \(s'(a,b,c,c)\le b\wedge c\) and therefore

$$\begin{aligned} s'(a,b,c,c)=b\wedge c \ \ \ \text { or }\ \ \ s'(a,b,c,c)=a\wedge b\wedge c \end{aligned}$$
(3.4)

since \(\{\, z\in \mathcal {L}C\mid z\le b\wedge c \,\}=\{\,b\wedge c,a\wedge b\wedge c \,\}\) (because \(b\wedge c\) covers \(a\wedge b\wedge c\) in \(\mathcal {L}C\) [2, Corollary 1.7]).

Consider the term \(t(p,q)=p\wedge q\). Then, by the axiom (\(\mathtt {M}_2\)) involving \(\mu \), for \({\hat{B}}=\{\, b,c \,\}\), we have:

$$\begin{aligned} \mathcal {P}\mu _{{\hat{B}}}\circ \lambda _{\mathcal {L}{\hat{B}}}\circ \mathcal {L}\lambda _{{\hat{B}}}\big (t({\hat{B}},{\hat{B}}\vee \{\, c \,\})\big )=\lambda _{{\hat{B}}}\circ \mu _{\mathcal {P}{\hat{B}}}\big (t({\hat{B}},{\hat{B}}\vee \{\, c \,\})\big ) \end{aligned}$$

but using the absorption law we have

$$\begin{aligned} \lambda _{{\hat{B}}}\circ \mu _{\mathcal {P}{\hat{B}}}\big (t({\hat{B}},{\hat{B}}\vee \{\, c \,\})\big )=\lambda _{{\hat{B}}}\big ({\hat{B}}\wedge ({\hat{B}}\vee \{\, c \,\})\big )=\lambda _{{\hat{B}}}({\hat{B}})={\hat{B}} \end{aligned}$$

and using Lemma 3.5 we have

$$\begin{aligned} \mathcal {P}\mu _{{\hat{B}}}\circ \lambda _{\mathcal {L}{\hat{B}}}\circ \mathcal {L}\lambda _{{\hat{B}}} \big (t({\hat{B}},{\hat{B}}\vee \{\, c \,\})\big )&=\mathcal {P}\mu _{{\hat{B}}}\circ \lambda _{\mathcal {L}{\hat{B}}} \Big (t\big (\lambda _{{\hat{B}}}({\hat{B}}),\lambda _{{\hat{B}}}({\hat{B}}\vee \{\, c \,\})\big )\Big )\\&=\mathcal {P}\mu _{{\hat{B}}}\circ \lambda _{\mathcal {L}{\hat{B}}}\big (t({\hat{B}},\{\, c,b\vee c \,\})\big ) \end{aligned}$$

Hence, the last three equations give us

$$\begin{aligned} \mathcal {P}\mu _{{\hat{B}}}\circ \lambda _{\mathcal {L}{\hat{B}}}\Big (t\big ({\hat{B}},\{\, c,b\vee c \,\}\big )\Big )={\hat{B}}. \end{aligned}$$
(3.5)

In order to finish the proof, by using (3.4), we assume by contradiction that \(s'(a,b,c,c)=b\wedge c\), that is, we assume that \(b\wedge c\in \lambda _C(B\wedge \{\, c \,\})\). By the axiom (\(\mathtt {M}_1\)) involving \(\widehat{\mu }\) we have:

$$\begin{aligned} \widehat{\mu }_{\mathcal {L}\mathcal {L}{\hat{B}}}\circ \mathcal {P}\lambda _{\mathcal {L}{\hat{B}}}\circ \lambda _{\mathcal {P}\mathcal {L}{\hat{B}}} \Big (t\big (\{\, {\hat{B}} \,\}, \{\, \{\, c \,\},\{\, b\vee c \,\} \,\}\big )\Big )&=\lambda _{\mathcal {L}{\hat{B}}}\Big (t\big ({\hat{B}},\{\, c,b\vee c \,\}\big )\Big ) \end{aligned}$$

and by the assumption that \(b\wedge c\in \lambda _C(B\wedge \{\, c \,\})\), using the definition \(t(p,q)=p\wedge q\) above of the term t, we have:

$$\begin{aligned} {\hat{B}}\wedge \{\, c \,\}\in \lambda _{\mathcal {P}\mathcal {L}{\hat{B}}} \big (\{\,{\hat{B}}\,\}\wedge \{\, \{\, c \,\},\{\, b\vee c \,\} \,\}\big )=\lambda _{\mathcal {P}\mathcal {L}{\hat{B}}} \Big (t\big (\{\, {\hat{B}} \,\}, \{\, \{\, c \,\},\{\, b\vee c \,\} \,\}\big )\Big ), \end{aligned}$$

which implies

$$\begin{aligned} \lambda _{\mathcal {L}{\hat{B}}}({\hat{B}}\wedge \{\, c \,\})\in \mathcal {P}\lambda _{\mathcal {L}{\hat{B}}}\circ \lambda _{\mathcal {P}\mathcal {L}{\hat{B}}} \Big (t\big (\{\, {\hat{B}} \,\}, \{\, \{\, c \,\},\{\, b\vee c \,\} \,\}\big )\Big ), \end{aligned}$$

but by Lemma 3.5 we have \(\lambda _{\mathcal {L}{\hat{B}}}({\hat{B}}\wedge \{\, c \,\})=\{\, c,b\wedge c \,\}\) which implies

$$\begin{aligned} b\wedge c\in \widehat{\mu }_{\mathcal {L}\mathcal {L}{\hat{B}}}\circ \mathcal {P}\lambda _{\mathcal {L}{\hat{B}}}\circ \lambda _{\mathcal {P}\mathcal {L}{\hat{B}}} \Big (t\big (\{\, {\hat{B}} \,\}, \{\, \{\, c \,\},\{\, b\vee c \,\} \,\}\big )\Big )=\lambda _{\mathcal {L}{\hat{B}}}\big (t({\hat{B}},\{\, c,b\vee c \,\})\big ) \end{aligned}$$

and therefore

$$\begin{aligned} b\wedge c=\mu _{{\hat{B}}}(b\wedge c)\in \mathcal {P}\mu _{{\hat{B}}}\circ \lambda _{\mathcal {L}{\hat{B}}}\big (t({\hat{B}},\{\, c,b\vee c \,\})\big )\overset{(3.5)}{=}{\hat{B}}, \end{aligned}$$

a contradiction. \(\square \)

Now we proceed with the proof of the theorem.

Proof of Theorem 3.1

Assume by contradiction that there is a distributive law \(\lambda :\mathcal {L}\mathcal {P}\Longrightarrow \mathcal {P}\mathcal {L}\) of \((\mathcal {L},\eta ,\mu )\) over \((\mathcal {P},\widehat{\eta },\widehat{\mu })\). Let \(D=\{\, a,b,c,d \,\}\) and \(B=\{\, a,b \,\}\). By Lemma 3.6 we have:

$$\begin{aligned} B\wedge \{\, c \,\}\wedge \{\, d \,\}\in \lambda _{\mathcal {P}D}(\{\, B \,\}\wedge \{\, \{\, c \,\},\{\, d \,\} \,\}). \end{aligned}$$
(3.6)

Now, by using Lemma 3.6 again, we have \(a\wedge b\wedge (c\wedge d)\in \lambda _{\mathcal {L}D}(B\wedge \{\, c\wedge d \,\})\) and, using \(\mu _D(a\wedge b\wedge (c\wedge d))=a\wedge b\wedge c\wedge d\), we obtain

$$\begin{aligned} a\wedge b \wedge c\wedge d&\in \mathcal {P}\mu _D\circ \lambda _{\mathcal {L}D}(B\wedge \{\, c\wedge d \,\})\nonumber \\&=\mathcal {P}\mu _D\circ \lambda _{\mathcal {L}D}\big (\lambda _D(B)\wedge \lambda _D(\{\, c \,\}\wedge \{\, d \,\})\big )\nonumber \\&=\mathcal {P}\mu _D\circ \lambda _{\mathcal {L}D}\circ \mathcal {L}\lambda _D\big (B\wedge (\{\, c \,\}\wedge \{\, d \,\})\big )\nonumber \\&=\lambda _D\circ \mu _{\mathcal {P}D}\big (B\wedge (\{\, c \,\}\wedge \{\, d \,\})\big )\nonumber \\&=\lambda _D(B\wedge \{\, c \,\}\wedge \{\, d \,\}), \end{aligned}$$
(3.7)

where the first equality follows from (3.1a) and (3.1b) and the third equality by the axiom (\(\mathtt {M}_2\)) involving \(\mu \). Now, (3.6) and (3.7) imply

$$\begin{aligned}&a\wedge b \wedge c\wedge d \in \widehat{\mu }_{\mathcal {L}D}\circ \mathcal {P}\lambda _D\circ \lambda _{\mathcal {P}D}\big (\{\, B \,\}\wedge \{\, \{\, c \,\},\{\, d \,\} \,\}\big )\nonumber \\&\quad =\lambda _D\circ \mathcal {L}\widehat{\mu }_D \big (\{\, B \,\}\wedge \{\, \{\, c \,\},\{\, d \,\} \,\}\big )\nonumber \\&\quad =\lambda _D\big (B\wedge \{\, c,d \,\}\big ). \end{aligned}$$
(3.8)

where the first equality follows by the axiom (\(\mathtt {M}_1\)) involving \(\widehat{\mu }\).

Finally, by naturality of \(\lambda \), using (3.8) and the function \(h :D\rightarrow B\) such that \(h(a)=h(c)=a\) and \(h(b)=h(d)=b\), we obtain \(a\wedge b\in \lambda _B(B)\overset{(3.1a)}{=}B\), a contradiction. \(\square \)

As we commented after Lemma 3.2, the proof of Theorem 3.1 we just made also works for any monad associated to a lattice variety that contains \(\mathbf {2}\). Also, since the proof above did not involve the empty set or infinite sets, we can also replace the powerset monad for its nonempty version and/or its finite version. We can summarize our results as follows.

Theorem 3.7

Let \((T,\eta ^T,\mu ^T)\) be a monad associated to a lattice variety that contains the two element linear order \(\mathbf {2}\) and let \((S,\eta ^S,\mu ^S)\) be any of the following monads:

  • the (nonempty) powerset monad,

  • the (nonempty) finite powerset monad.

Then there is no distributive law of \((T,\eta ^T,\mu ^T)\) over \((S,\eta ^S,\mu ^S)\). \(\square \)

Particular cases of the monad \((T,\eta ^T,\mu ^T)\) in the previous theorem include: the free (bounded) lattice monad, the free (bounded) distributive lattice monad and the free (bounded) modular lattice monad, among others.

4 Final remarks

Distributive laws between monads provide us a canonical way to compose monads [1]. The case of a distributive law over the powerset is of particular interest in the subject of relation lifting [7] and the so-called powerset construction or determinization [9]. It is known that a distributive law of a functor over the powerset (monad) always exists if the functor preserves weak pullbacks [5, Section 4]. Nevertheless, distributive laws of a functor that does not preserve weak pullbacks over the powerset are rare and the answer might depend on the kind of axioms we impose over such distributive law. For instance, it is shown in [6] that there is no distributive law of \((\mathcal {P},\widehat{\eta })\) over \((\mathcal {P},\widehat{\eta })\), correcting a mistake that appeared a couple of times in the literature claiming the opposite [6, Section 5], but, on the other hand, distributive laws of \((\mathcal {P},\widehat{\eta },\widehat{\mu })\) over \(\mathcal {P}\) and distributive laws of \(\mathcal {P}\) over \((\mathcal {P},\widehat{\eta },\widehat{\mu })\) do exist (just take \(\mathcal {P}\widehat{\eta }\circ \widehat{\mu }\) and \(\widehat{\eta }\mathcal {P}\circ \widehat{\mu }\), respectively).

Other negative examples of distributive laws have been also shown in the literature. In [11, Proposition 3.2.], is shown that there is no distributive law of the probability distribution monad over the powerset monad, whose proof idea was due to Gordon Plotkin. In [6, Theorem 2.4.], we generalized Plotkin’s idea to show that if a functor T preserves preimages and admits a non-trivial idempotent term then there is no distributive law of \((T,\eta )\) over \((\mathcal {P},\widehat{\eta })\). As expected, [6, Theorem 2.4.] does not apply for the case of lattices since the functor \(\mathcal {L}\) does not preserve preimages. Indeed, the pullback square in Section 2 that is not preserved by \(\mathcal {L}\) is a preimage. The recent paper [12] also generalizes Plotkin’s idea, and it provides theorems that give sufficient conditions for the nonexistence of certain distributive laws between monads, where monads considered are presented by algebraic terms. Again, the case of lattices over powerset is a case that cannot be handled with the results in [12]. Indeed, to apply any of the Theorems III.6, III.13, III.15, IV.10, or IV.15 in [12], for the case of lattices over powerset, we would require the property that for every lattice term \(t(x_1,\dots ,x_n)\) the identity \(t(x_1,\dots ,x_n)\approx x\) implies that x is the only variable that appears in \(t(x_1,\dots ,x_n)\), which is not true since the the absorption law \(x\vee (x\wedge y)\approx x\) does not satisfy this property. Furthermore, the only theorem that does not require this property is Theorem IV which, for the case of lattices over powerset, would require the equational representation of powerset to have at least two constants, which is not true, and would require each of the operations \(\wedge \) and \(\vee \) to have a constant in the theory that is the identity element for the operation, which is not true either if the lattice is not bounded.

To the best of our knowledge, characterizations for the existence of a distributive law over the powerset monad are not known. As in the case of powerset over powerset, its existence depends on the kind of distributive law we are considering. Our main purpose of considering lattices was in the search of an example of a monad whose functor part does not preserve weak pullbacks that could have a distributive law over the powerset monad. As it turned out, it was a challenging question that we solved in the negative way. Another instance we considered which cannot be handled with any of the results in [6, 12] was the group monad \((G,\eta ,\mu )\). Indeed, if we consider the preimage given in Section 2, then we have \(Gf(xy^{-1})=e=Gf(e)\), where e is the identity element, but there is no \(t\in G\{\,(x,x),(x,y)\,\}\) such that \(G\pi _2(t)=xy^{-1}z\), which shows that we cannot apply [6, Theorem 2.4.]. On the other hand, the identity \(yy^{-1}x\approx x\) holds in the theory of groups but the term \(yy^{-1}x\) contains other variables different than x, which means that we cannot apply the theorems in [12] either. In this case, we found that there is no distributive law of \((G,\eta )\) over \((\mathcal {P},\widehat{\eta })\), whose proof, similar to the lattice case, depends on the very specific setting of group theory. We conjecture that such an example of a distributive law of a monad, whose functor part does not preserve weak pullbacks, over the powerset monad does not exist and leave it as an open problem for further research.