Canonical Extensions, Esakia Spaces, and Universal Models

Abstract

In this chapter we survey some recent developments in duality for lattices with additional operations paying special attention to Heyting algebras and the connections to Esakia’s work in this area. In the process we analyse the Heyting implication in the setting of canonical extensions both as a property of the lattice and as an additional operation. We describe Stone duality as derived from canonical extension and derive Priestley and Esakia duality from Stone duality for maps. In preparation for this we show that the categories of Heyting and modal algebras are both equivalent to certain categories of maps between distributive lattices and Boolean algebras. Finally we relate the N-universal model of intuitionistic logic to the Esakia space of the corresponding Heyting algebra via bicompletion of quasi-uniform spaces.

In memory of Leo Esakia

This work was partially supported by ANR 2010 BLAN 0202 02 FREC

2.1 Introduction

With his study of duality for Heyting algebras and modal algebras, Esakia was one of the first to study duality for lattices with additional operations [12]. Jónsson and Tarski studied duality for Boolean algebras with additional operations in the form of canonical extensions very early on [34, 35]. In this chapter we highlight some of the main results of central importance for these works of Esakia, and Jónsson and Tarski, and indicate some further developments in duality theory for lattices with additional operations, mainly as they pertain to Heyting algebras.

The theory of canonical extensions, which recasts duality in a purely algebraic setting of lattice completions, was initiated by Jónsson and Tarski in their two papers [34, 35]. At first sight, one might think the purpose was to get rid of the topological nature of Stone duality, but this aspect is actually still very much present, though in a form more similar to the later developed point-free approach to topology. The main purpose for Jónsson and Tarski in recasting duality in algebraic form was to make it easier to identify what form the dual of an additional algebraic operation on a lattice should take. Thus in the first paper [34] they proved a general theorem about the extension of maps and preservation of equational properties, and the second paper [35] then specified the ensuing dual structures in which one can represent the original algebras.

The theory of canonical extensions has moved forward significantly since the seminal work of Jónsson and Tarski and is now applicable far beyond the original Boolean setting. It has the advantage of allowing a uniform and relatively transparent treatment of duality issues concerning additional operations. Since Esakia’s work on duality for Heyting and S4 modal algebras may be seen as special instances of duality for lattices with additional operations, the theory of canonical extensions has in fact allowed the generalisation of many of Esakia’s results and methods to a much wider setting. In this chapter we will show this while focussing mainly on Heyting algebras.

In Sect. 2.2 we give a brief introduction to canonical extension and show that it provides a point-free approach to duality for Heyting algebras. To this end, we show, in a constructive manner, that the canonical extension of any distributive lattice is a complete $\bigvee$-distributive lattice and thus also a Heyting algebra. Further, we show that the canonical embedding of a lattice in its canonical extension is conditionally Heyting and thus a Heyting algebra embedding if the original distributive lattice is a Heyting algebra. In Sect. 2.3 we explain how additional operations are treated in the theory of canonical extensions and illustrate this in the particular example of Heyting implication, viewed as an additional operation on a lattice.

Section 2.4 is purely algebraic and is a preparation for the duality results for Heyting and S4 modal algebras. Here we discuss Booleanisation of distributive lattices. In modern terms Booleanisation is the fact that the inclusion of the category of Boolean algebras in the category of distributive lattices has a left adjoint. This means, among other, that for any distributive lattice $D$, there is a unique Boolean algebra $D^-$ that contains $D$ as a sublattice, and that is generated by $D$ as a Boolean algebra. This implies that the category of distributive lattices is equivalent to the category of lattice inclusions $D\hookrightarrow D^-$ with commutative diagrams for which the maps between the domains are lattice maps and the maps between the codomains are Boolean algebra maps. One can then see Heyting algebras as the (non full) subcategory of those inclusions $D\hookrightarrow D^-$ which have an upper adjoint $g\text {:}\,D^-\rightarrow D$ and with commutative diagrams that also commute for the adjoint maps. Finally S4 modal algebras also live inside the category of lattice embeddings from distributive lattices to Boolean algebras as those lattice embeddings $e\text {:}\,D\rightarrow B$ that have an upper adjoint, and the maps are, as for Heyting algebras, the commutative diagrams that commute both for the embeddings and for their upper adjoints. That is, in this setting, one may see the category of Heyting algebras as the intersection of the category of distributive lattices and the category of S4 modal algebras. This point of view on distributive lattices, Heyting algebras, and S4 modal algebras allows one to see all of them as certain maps between distributive lattices and Boolean algebras. Now applying Stone duality to these maps yields Priestley duality for distributive lattices, and Esakia duality for Heyting algebras and modal algebras.

In Sect. 2.5 we show how Stone duality may be derived from the canonical extension results by ‘adding points’ in the sense of point-free topology. Further, we give an algebraic account of the duality for operators and the corresponding notion of bisimulation. This last topic is treated further in Sect. 2.7 where we discuss Esakia’s lemma and its generalisation as obtained in our paper [22] with Bjarni Jónsson. Finally, in Sect. 2.6, we derive both Priestley and Esakia duality from Stone duality with the help of the results of Sect. 2.4.

In Sect. 2.8, we briefly discuss set representations of distributive lattices and in particular the representation of the free $N$-generated Heyting algebra in the so-called $N$-universal model. In particular, we outline recent results from [19] which show that the Stone or Priestley space of a distributive lattice is the bicompletion of any set representation of the lattice, viewed as a quasi-uniform space.

I would like to thank the anonymous referee as well as Dion Coumans and Sam van Gool for carefully reading a draft of the chapter and making many useful comments which have improved the chapter greatly. I also want to thank Guram Bezhanishvili for detailed historical comments pointing out how my view point of Esakia duality here closely corresponds to Leo Esakia’s own derivation of the duality. These historical comments have been incorporated in Sects. 2.4 and 2.6 as appropriate. Finally I would like to thank Dick de Jongh for helpful discussions about the universal models for intuitionistic logic.

2.2 Canonical Extension

Canonical extensions were first introduced by Jónsson and Tarski [34] in order to deal with additional operations such as modalities and relation algebraic operations in the setting of Stone duality. The idea is the following: A topological space is a pair, $(X,\fancyscript{O})$ where $X$ is a set, and $\fancyscript{O}$ is a collection of downsets of $X$ (in the order on $X$ induced by $\fancyscript{O}$). Since the poset $X$ and the complete lattice, $\fancyscript{D}(X)$, of all downsets of $X$ are dual to each other via the discrete duality between posets and downset lattices, the information in giving $(X,\fancyscript{O})$ is exactly the same as the information in the embedding $\fancyscript{O}\hookrightarrow \fancyscript{D}(X)$. Further, in the case of Stone duality, since $\fancyscript{O}$ is generated by the dual lattice $D$, the data $\fancyscript{O}\hookrightarrow \fancyscript{D}(X)$, in turn, amounts to giving an embedding $D\hookrightarrow \fancyscript{D}(X)$. This latter formulation brings the entire duality within the setting of lattice theory, making the proper translation of additional structure such as operations on the lattice more transparent. The key insight needed here is that this embedding may be uniquely characterised among the completions of $D$.

Definition 1. Let $L$ be a lattice, a canonical extension of $L$ is a lattice completion $L\hookrightarrow L^\delta$ of $L$ with the following two properties:

density: $L$ is $\bigvee \bigwedge$- and $\bigwedge \bigvee$-dense in $L^\delta$, that is, every element of $L^\delta$ is both a join of meets and a meet of joins of elements of $L$;

compactness: given any subsets $S$ and $T$ of $L$ with $\bigwedge S \le \bigvee T$ in $L^\delta$, there exist finite sets $S' \subseteq S$ and $T' \subseteq T$ such that $\bigwedge S' \le \bigvee T'$ in $L$.

The fundamental facts about canonical extensions are the following.

Theorem 1. Every bounded lattice has a canonical extension and it is unique up to an isomorphism which commutes with the embedding of the original lattice in the extension.

Theorem 2. For any bounded distributive lattice $D$, the map $\eta \text {:}\,D\rightarrow \fancyscript{D}(X,\le )$ into the lattice of all downsets of the dual space $X$ of $D$ which sends each element $d\in D$ to the corresponding clopen downset $\eta (d)$ is a canonical extension of $D$.

In the original approach of Jónsson and Tarski for Boolean algebras [34] and Gehrke and Jónsson for bounded distributive lattices [22], Theorem 2 provided the existence part of Theorem 1. However, the canonical extension may also be obtained directly from the lattice without the use of the axiom of choice. This was first identified by Ghilardi and Meloni in the case of Heyting algebras in their work on intermediate logics [31]. A similar choice-free approach was used in [20] where Theorem 1 was first proved in the setting of arbitrary (i.e., not-necessarily-distributive) bounded lattices. There, it was shown that the lattice of Galois closed sets of the polarity $({\fancyscript{F}}, {\fancyscript{I}}, R)$, where $\fancyscript{F}$ is the collection of lattice filters of $L$ and $\fancyscript{I}$ is the collection of lattice ideals of $L$, and $FRI$ if and only if $F\cap I\not =\emptyset$, yields a canonical extension of $L$. This is actually part of a more general representation theorem for so-called $\Delta _1$-completions of a lattice. These are the completions satisfying the density condition in Definition 1. In [21] it was shown that any such completion may be obtained as the Galois closed subsets of a certain kind of polarity between a closure system of filters and a closure system of ideals of the original lattice. A different choice-free approach to the existence of canonical extensions for lattices via dcpo presentations was given in [26].

It follows from Theorem 2 that the canonical extension of any bounded distributive lattice is a downset lattice and therefore a complete Heyting algebra. We show here, in a choice-free manner, that the canonical extension of any bounded distributive lattice is a frame and thus also a complete Heyting algebra. Further, we show that the embedding of a bounded lattice in its canonical extension is conditionally Heyting, meaning that it preserves the implication whenever defined. Thus canonical extension also provides a constructive approach to Esakia duality.

We first need a few facts about canonical extensions. In working with topological spaces, the closed and the open subsets, obtained for a Boolean space by taking arbitrary intersections and arbitrary unions of basic clopens, respectively, play a very important role. For canonical extensions, the basic clopens are replaced by the image of the embedding $L\hookrightarrow L^\delta$ and the closures under infima and suprema play roles similar to those of closed and open subsets in topology. Also, from a lattice theoretic perspective, the density condition that is part of the abstract definition of canonical extension makes it clear that the meet and the join closures of $L$ in $L^\delta$ play a central role.

Definition 2. Let $L$ be a lattice, and $L^\delta$ a canonical extension of $L$. Define

$$\begin{aligned} F(L^\delta )&:= \{ \, x \in L^\delta \mid x \text { is a meet of elements from } L\,\}, \\ \\ I(L^\delta )&:= \{ \, y \in L^\delta \mid y \text { is a join of elements from } L\,\}. \end{aligned}$$

We refer to the elements of $F(L^\delta )$ as filter elements and to the elements of $I(L^\delta )$ as ideal elements.

The reason for this nomenclature is that the poset $F(L^\delta )$ of filter elements of $L^\delta$ is reverse order isomorphic to the poset Filt $(L)$ of lattice filters of $L$ via the maps $x\mapsto ({\uparrow }x)\cap L$ and $F\mapsto \bigwedge _{L^\delta } F$, and, dually, the poset $I(L^\delta )$ of ideal elements of $L^\delta$ is order isomorphic to the poset Idl $(L)$ of lattice ideals of $L$ via the maps $y\mapsto ({\downarrow }y)\cap L$ and $I\mapsto \bigvee _{L^\delta } I$. Establishing these isomorphisms is in fact the first step in proving the uniqueness of the canonical extension, see e.g. [21, Theorem 5.10]. Note that now we can reformulate the density condition for canonical extensions by saying that $F(L^\delta )$ is join dense in $L^\delta$ and $I(L^\delta )$ is meet dense in $L^\delta$.

We are now ready to prove that the canonical extension of a bounded distributive lattice satisfies the join-infinite distributive law.

Theorem 3. Let $D$ be a bounded distributive lattice. Then $D^\delta$ is $\bigvee$-distributive.

Proof. As a first step we want to show for $x\in F(D^\delta )$ and $X\subseteq F(D^\delta )$ that

$$x\wedge \bigvee X\le \bigvee \{\,x\wedge x'\mid x'\in X\,\}.$$

To this end, let $z\in F(D^\delta )$ with $z\le x\wedge \bigvee X$ and $y\in I(D^\delta )$ with $\bigvee \{\,x\wedge x'\mid x'\in X\,\}\le y$. By the join density of $F(D^\delta )$ and the meet density of $I(D^\delta )$, it suffices to show that we must have $z\le y$.

The condition on $y$ implies that, for each $x'\in X$, we have $x\wedge x'\le y$, and thus, by compactness, there are $a,b\in D$ with $x\le a$, $x'\le b$ and $a\wedge b\le y$. As a consequence we have

$$ \bigvee X\le \bigvee \{\,b\in D\mid \exists x'\in X\,\exists a\in D\text { with }x\le a, x'\le b, \text { and } a\wedge b\le y\,\}. $$

This inequality, combined with $z\le x\wedge \bigvee X\le \bigvee X$ and compactness, now implies that there are $b_1,\ldots ,b_n\in D$, there are $x'_1,\ldots ,x'_n\in X$ with $x'_i\le b_i$, and there are $a_1,\ldots , a_n\in D$ with $x\le a_i$ and $a_i\wedge b_i\le y$ and $z\le b_1\vee \ldots \vee b_n$. Let $a=a_{1}\wedge \ldots \wedge a_{n}$ then, since $z\le x\wedge \bigvee X\le x$, we have

$$\begin{aligned} z&\le x\wedge (b_1\vee \ldots \vee b_n)\\&\le a\wedge (b_1\vee \ldots \vee b_n)\\&=(a\wedge b_{1})\vee \ldots \vee (a\wedge b_{n})\\&\le (a_{1}\wedge b_{1})\vee \ldots \vee (a_{n}\wedge b_{n})\le y. \end{aligned}$$

It follows that $x\wedge \bigvee X\le \bigvee \{\,x\wedge x'\mid x'\in X\,\}$ as desired. In order to prove that $L^\delta$ is $\bigvee$-distributive, it is enough to consider suprema of collections $X$ of filter elements since the filter elements are join dense in $L^\delta$. However, we need to know that for any $u\in L^\delta$, we have $u\wedge \bigvee X\le \bigvee \{\,u\wedge x'\mid x'\in X\,\}$. To this end we have

$$\begin{aligned} u\wedge \bigvee X&=\bigvee \{\,x\in F(L^\delta )\mid x\le u\wedge \bigvee X\,\}\\&\le \bigvee \{\,x\wedge \bigvee X\mid u\ge x\in F(L^\delta )\,\}\\&\le \bigvee \{\,\bigvee \{\,x\wedge x'\mid x'\in X\,\}\mid u\ge x\in F(L^\delta )\,\}\\&=\bigvee \{\,\bigvee \{\,x\wedge x'\mid u\ge x\in F(L^\delta ) \,\}\mid x'\in X\,\}\\&\le \bigvee \{\,u\wedge x'\mid x'\in X\,\}. \end{aligned}$$

This completes the proof.$\Box$

Note that, by order duality, it follows that the canonical extension of a distributive lattice also is $\bigwedge$-distributive, but this is not our focus here. Next we prove that the canonical embedding is conditionally Heyting.

Proposition 1. Let $L$ be a bounded lattice. The canonical extension $\eta \text {:}\,L\rightarrow L^\delta$ preserves any existing relative pseudocomplements.

Proof. Let $a,b\in L$ and suppose $a\rightarrow _Lb=\max \{c\in L\mid a\wedge c\le b\}$ exists. Let $x\in F(L^\delta )$ with $a\wedge x\le b$, then, by compactness, there is $c\in L$ with $a\wedge c\le b$ and $x\le c$. Thus $x\le a\rightarrow _Lb$. Since $F(L^\delta )$ is join dense in $L^\delta$, it follows that $a\rightarrow _Lb=\max \{u\in L^\delta \mid a\wedge u\le b\}$ and thus $a\rightarrow _{L^\delta }b$ exists and is equal to $a\rightarrow _Lb$.$\Box$

Corollary 1. Let $A$ be a Heyting algebra. The canonical extension of $A$ as a bounded lattice is a Heyting algebra embedding.

2.3 Implication as an Additional Operation

In the previous section, we saw that canonical extension, or equivalently, the representation given by topological duality for bounded lattices, restricts to Heyting algebras giving Heyting algebra representations. The theory of canonical extensions was developed to deal with additional operations that may not be determined by the order of the underlying lattice. As such, canonical extension for distributive lattices with additional operations may be seen as a generalisation (in algebraic form) of Esakia duality.

In this section, we give the general definitions of extensions of maps and relate these, in the case of Heyting algebras, to the Heyting implication on the canonical extension.

Definition 3. Let $K$ and $L$ be lattices, $f\text {:}\,K \rightarrow L$ any function. We define maps $f^\sigma$ and $f^\pi$ from $K^\delta$ into $L^\delta$ by

$$\begin{aligned} f^\sigma (u)&:= \bigvee \left\{ \bigwedge \{\,f(a) \mid a\in K\text { and } x\le a\le y\,\} \mid F(K^\delta )\ni x\le u\le y\in I(K^\delta )\right\} ,\\ f^\pi (u)&:= \bigwedge \left\{ \bigvee \{\, f(a) \mid a\in K \text { and } x\le a\le y\,\} \mid F(K^\delta )\ni x\le u\le y\in I(K^\delta )\right\} . \end{aligned}$$

The above definition, for arbitrary maps, was first given in the setting of distributive lattices and it was shown that these are in fact upper and lower envelopes with respect to certain topologies [23]. This is not always true in the general lattice setting, but it is still true for mono- and antitone maps and for arbitrary maps on lattices lying in finitely generated lattice varieties. For details, see Sect. 4 of [25] and the Ph.D. thesis of Jacob Vosmaer [47].

The two above extensions of a map $f$ are not always equal, but for maps that are join or meet preserving, or that turn joins into meets or vice versa, the two extensions agree and we say such maps are smooth, see e.g. [23, Corollary 2.25]. However, for binary operations, coordinate-wise preservation, or reversal, of join and/or meet is not sufficient to imply smoothness. Example 1 below shows that implication, viewed as an additional binary operation on the lattice underlying a Heyting algebra, need not be smooth.

In the example we will make use of two basic facts about canonical extensions of lattices which are useful when dealing with additional operations: First of all, the canonical extension of a finite product is, up to isomorphism, the product of the canonical extensions of the individual lattices. This allows one to compute coordinate-wise. Secondly, the operation $L\mapsto L^\partial$ which yields for each lattice the order dual lattice also commutes with canonical extension and the filter elements of $L^\delta$ are precisely the ideal elements of $(L^\partial )^\delta =(L^\delta )^\partial$ and vice versa.

Looking at the definitions of the extensions of maps, note that they are self dual in the order on the domain of the map. Thus we can take the order dual of the domain, or of any coordinate of the domain, and still obtain the same extension. Further note that, if the map is order preserving, then the upper bounds of the intervals on which we are taking meets, and the lower bounds of the intervals on which we are taking joins play no role. Accordingly, for $f:K \rightarrow L$ order-preserving we have

$$\begin{aligned} f^\sigma (u)&= \bigvee \left\{ \bigwedge \{\,f(a) \mid x\le a\in K\,\} \mid F(K^\delta )\ni x\le u\right\} , \end{aligned}$$

and, in particular, $f^\sigma (x)=\bigwedge \{\,f(a) \mid x\le a\in K\,\}$ for filter elements $x\in F(K^\delta )$.

Example 1. Let $A$ be the Heyting algebra consisting of a countable decreasing chain with a bottom added. Since $A$ is a chain it is a Heyting algebra in which the implication is given by

$$ f(a,b) =\left\{ \begin{array}{cc} 1 &{} \text {if } a \le b, \\ b &{} \text {if } a > b. \end{array}\right. $$

Since $f$ is order-preserving in its second coordinate and order-reversing in its first, it will be convenient to regard $f$ as a map from $A^\partial \times A$ to $A$; we then have an order-preserving map to work with. We label the canonical extensions of the two chains as in the figures below.

In $A^\delta$ there is a single element which is not a lattice element, namely the filter element $x$. The canonical extension of $A^\partial \times A$ is the product shown below. The only element which is neither a filter element nor an ideal element of the product is $(x,x)$ and this is where the two extensions take different values.

The value of $f^\sigma (x,x)$ is calculated by approaching $(x,x)$ from below with filter elements, and in the second coordinate $x$ is itself a filter element, while it is an ideal element of the dual lattice $A^\partial$. Also, in $A^\partial$, the only filter elements below $x$ are the actual lattice elements $a\in A^\partial$. Thus we get:

$$\begin{aligned} f^\sigma (x,x)&= \bigvee \{\, f^\sigma (a,x) \mid A^\partial \ni a\le ^\partial x\,\} \\&= \bigvee \left\{ \bigwedge \{\,f(a,b)\mid x\le b \in A \,\}\mid A^\partial \ni a\le ^\partial x\,\right\} \\&= \bigvee \left\{ \bigwedge \{\, b \mid x\le b\in A, b<a\,\}\mid x\le a\in A\,\right\} \\&= x. \end{aligned}$$

The value of $f^\pi (x,x)$ is calculated by approaching $(x,x)$ from above

$$\begin{aligned} f^\pi (x,x)&= \bigwedge \{ \,f^\pi (x,b) \mid x\le b\in A\,\} \\&= \bigwedge \left\{ \bigvee \{f(a,b)\mid A^\partial \ni a\le ^\partial x\,\}\mid x\le b\in A\,\right\} \\&= \bigwedge \left\{ 1 \mid x\le b\in A\,\right\} \\&= 1. \end{aligned}$$

We conclude that $f$ is not smooth.

It is clear from the above computation, that, if one of the extensions of the implication on $A$ is equal to the Heyting implication that exists on $A^\delta$, then it must be the $\pi$-extension, and that is indeed the case in general. This is actually just a special instance of the fact that, for an order preserving map $f$, if $g$ is the upper adjoint of $f$ with respect to some coordinate, then $g^\pi$ is the upper adjoint of $f^\sigma$ with respect to the same coordinate [24, Proposition 4.2].

Proposition 2. Let $(A,\rightarrow )$ be a Heyting algebra, then $(A^\delta ,(\rightarrow )^\pi )$  is a Heyting algebra.

Proof. Let $x,x'\in F(A^\delta )$, and $y\in I(A^\delta )$. Using the fact that $\rightarrow$ is order preserving as a map from $A^\partial \times A$, we have

$$x'\rightarrow ^\pi y=\bigvee \{a'\rightarrow b\mid x'\le a'\in A\ni b\le y\}. $$

Using the compactness property and the definition of filter and ideal elements we then obtain the following string of equivalences

$$\begin{aligned} x\wedge x'\le y&\iff \exists a,a',b\in A\ (x\le a, x'\le a', b\le y\text { and } a\wedge a'\le b)\\&\iff \exists a,a',b\in A\ (x\le a, x'\le a', b\le y\text { and } a\le a'\rightarrow b)\\&\iff x\,\le \, x'\rightarrow ^\pi y. \end{aligned}$$

Now let $u,v,w\in A^\delta$, then, using the density property, the fact that $A^\delta$ is $\bigvee$-distributive, and the definition of extension for additional operations we have the following string of equivalences

$$\begin{aligned}&u\wedge v\le w \\ \iff&\forall x,x'\in F(A^\delta )\,\forall y\in I(A^\delta ) \left[ \,(x\le u, x'\le v,\text {and}\, w\le y)\Rightarrow x\wedge x'\le y\,\right] \\ \iff&\forall x,x'\in F(A^\delta )\,\forall y\in I(A^\delta ) \left[ \,(x\le u, x'\le v, \text {and}\, w\le y)\Rightarrow x\le x'\rightarrow ^\pi y\,\right] \\ \iff&u\,\le \, v\rightarrow ^\pi w. \end{aligned}$$

$\Box$

2.4 The Connection Between Heyting Algebras and S4 Modal Algebras

The well-known equivalence between Heyting algebras and certain S4 modal algebras plays a fundamental role in Esakia duality, and in order to clarify the relationship of Esakia’s duality to Stone and Priestley duality and to canonical extension, we need a purely algebraic and categorical description of this classical connection. This is the purpose of the current section.

McKinsey and Tarski [38] initiated the rigorous study of the connection between Heyting algebras and S4 modal algebras. They worked with closed sets instead of opens and thus with closure algebras and what we now call co-Heyting algebras. In the 1950s, Rasiowa and Sikorski worked further in this area. Their work may be found in their influential monograph [42]. They are the ones who switched to working with the interior and open sets as it is done now. Another paper in the area that was important to Leo Esakia was the 1959 paper by Dummet and Lemmon [11]. The next period of activity occurred in the 1970s with the work of Esakia and Blok, the most relevant and important publications being [4, 5, 12–14]. In particular, one may find a treatment of the results presented in this section in Sect. 5 of Chap. II of Leo Esakia’s 1985 book [14]. This book is written in Russian, but it may soon be available in English translation. Esakia called the S4-algebras corresponding to Heyting algebras stencil algebras. These were also already studied by McKinsey-Tarski and Rasiowa-Sikorski. Blok (and Dwinger) also payed special attention to these. Finally, the fully categorical description of the relationship between S4 and Heyting may be found in the paper [37] by Makkai and Reyes from 1995.

This equivalence between the category of Heyting algebras and the category of what was called stencil S4-algebras is also at the heart of the Blok-Esakia theorem. This theorem states that the lattice of subvarieties of the variety of Heyting algebras is isomorphic to the lattice of subvarieties of the variety of Grzegorczyk algebras. In fact, the reason that the Blok-Esakia theorem is true is that all varieties of Grzegorczyk algebras are generated by the stencil algebras that they contain. The Blok-Esakia theorem is treated in detail in the chapter by Frank Wolter and Michael Zakharyaschev in this same volume.

Here we start from Booleanisation for distributive lattices in general, a theory which dates back to Peremans’ 1957 paper [39]. This is already responsible for the fact that distributive lattices alternatively may be seen as embeddings of distributive lattices into Boolean algebras that they generate. This fact is the algebraic counterpart to Priestley duality. In categorical terms, Booleanisation is the left adjoint of the inclusion of the category of Boolean algebras as a full subcategory of the category of bounded distributive lattices. More concretely, given a bounded distributive lattice $D$, its Booleanisation $D^-$ is the unique, up to isomorphism, Boolean algebra containing $D$ as a bounded sublattice and generated as a Boolean algebra by $D$. It may be obtained algebraically by a free construction [15, 39] or via duality (or otherwise) by embedding $D$ in the power set of its dual space (or in any other Boolean algebra) and generating a Boolean algebra with the image. The inclusion homomorphism $e_D\text {:}\,D\rightarrow D^-$ is the unit of the adjunction and thus the Booleanisation of a bounded lattice homomorphism $h\text {:}\,D\rightarrow E$ commutes with the inclusions $e_D$ and $e_E$ so that $h^-$ extends $h$. Note that the elements of $D^-$ can be written in the form $\bigwedge _{i=1}^n(\lnot a_i\vee b_i)$ where the $a_i$s and the $b_i$s all belong to $D$.

Next, Heyting algebras may be seen as those distributive lattices for which $e_D\text {:}\,D\rightarrow D^-$ has a left adjoint, and this extends to a categorical duality.

Proposition 3. A bounded distributive lattice $A$ is the reduct of a Heyting algebra if and only if the inclusion  $e\text {:}\,A\rightarrow A^-$ of $A$ in its Booleanisation has an upper adjoint $g\text {:}\,A^-\rightarrow A$. Furthermore, a lattice homomorphism $\,h\text {:}\,A_1\rightarrow A_2$ is a Heyting algebra homomorphism if and only if the following diagram commutes

where $g_i\text {:}\,A_i^-\rightarrow A_i$ is the upper adjoint of the embedding $e_i\text {:}\,A_i\rightarrow A_i^-$ for $i=1\,and\,2$.

Proof. Suppose $e\text {:}\,A\rightarrow A^-$ has an upper adjoint $g\text {:}\,A^-\rightarrow A$, and let $a,b,c\in A$. We have

Thus $A$ is a Heyting algebra with $b\rightarrow c:=g(\lnot e(b)\vee e(c))$.

Conversely, if $A$ is a Heyting algebra, the following string of equivalences, toggling carefully between the algebras $A$ and $A^-$, shows that the adjoint does exist and it gives an explicit way of calculating it. Let $a\in A$ and $u=\bigwedge _{i=1}^n(\lnot e(b_i)\vee e(c_i))\in A^-$ where $b_i,c_i\in A$ for each $i\in \{1,\ldots ,n\}\,$, then we have

$$\begin{aligned}&\qquad \qquad \qquad \qquad e(a)\ \le \bigwedge _{i=1}^n(\lnot e(b_i)\vee e(c_i))\\&\iff \qquad \qquad e(a)\ \le \lnot e(b_i)\vee e(c_i) \ \text { for all }i\in \{1,\ldots ,n\} \\&\iff \ e(a)\wedge e(b_i) \le e(c_i) \quad \qquad \qquad \text { for all }i\in \{1,\ldots ,n\}\\&\iff \qquad \qquad a\wedge b_i\ \le \ c_i \quad \quad \quad \, \text { for all }i\in \{1,\ldots ,n\}\\&\iff \qquad \qquad \qquad a\ \le b_i\rightarrow c_i\quad \text { for all }i\in \{1,\ldots ,n\}\\&\iff \qquad \qquad \qquad a\ \le \bigwedge _{i=1}^n( b_i\rightarrow c_i) \end{aligned}$$

Finally, given the formulas relating the upper adjoint of the inclusion and the Heyting implication, and using the fact that $h^-$ extends $h$, it is a simple calculation to see that the statement about morphisms is true.$\Box$

On the other hand, this is closely related to S4 modal algebras via the following observation.

Proposition 4. The category of S4 modal algebras is equivalent to the following category: The objects of the category are adjoint pairs $e:D\leftrightarrows B:g$ where $D$ is a bounded distributive lattice, $B$ is a Boolean algebra, and the lower adjoint $e$ is a lattice embedding; The morphisms of the category are pairs $(h,k)$, where $h\text {:}\,B\rightarrow B'$ is a homomorphism of Boolean algebras, $k\text {:}\,D\rightarrow D'$ is a bounded lattice homomorphism, and the resulting squares commute both for the upper and lower adjoints.

Proof. Given an S4 modal algebra $(B,\Box )$, it is easy to check that $\mathrm{Im}(\Box )$ is a bounded distributive sublattice of $B$, and that the map $g\text {:}\,B\rightarrow \mathrm{Im}(\Box )$ defined by $b\mapsto \Box (b)$ is upper adjoint to the inclusion map $e\text {:}\,\mathrm{Im}(\Box )\rightarrow B$. Conversely, given an object $e\text {:}\,D\leftrightarrows B\text {:}\,g$ in the category as described above, it is also easy to see that $(B, e\circ g)$ is an S4 modal algebra, as well as that the compositions of these two assignments bring us back to an object equal or isomorphic to the one we started with. For the morphisms the pertinent diagram is

Suppose the square commutes both up and down. We have

$$\begin{aligned} h\circ (e_1\circ g_1)&=(h\circ e_1)\circ g_1\\&=(e_2\circ k)\circ g_1\\&= e_2\circ (k\circ g_1)\\&= e_2\circ (g_2\circ h)\\&= (e_2\circ g_2)\circ h \end{aligned}$$

so that $h$ is a homomorphism for the corresponding modal algebras. Conversely, suppose that $h\text {:}\,B_1\rightarrow B_2$ satisfies $h\circ (e_1\circ g_1)=(e_2\circ g_2)\circ h$. We define $k\text {:}\,D_1\rightarrow D_2$ by $k=g_2\circ h\circ e_1$. Then we have

$$\begin{aligned} k\circ g_1= (g_2\circ h\circ e_1)\circ g_1=g_2\circ (e_2\circ g_2\circ h)=g_2\circ h \end{aligned}$$

and

$$\begin{aligned} e_2\circ k= e_2\circ (g_2\circ h\circ e_1)=\mathrm{id}_{D_2}\circ (h\circ e_1)=h\circ e_1 \end{aligned}$$

and thus both diagrams commute.$\Box$

Combining Proposition 3 and Proposition 4 we obtain the following corollary which is the algebraic counterpart of the famous Gödel translation in logic.

Corollary 2. The category of Heyting algebras is equivalent to the full subcategory of those S4 modal algebras $(B,\Box )$ for which $\mathrm{Im}(\Box )$ generates $B$.

2.5 From Canonical Extensions to Stone Duality

Historically Jónsson and Tarski obtained canonical extension as an algebraic description of Stone duality. However, in retrospect, canonical extension can be obtained directly and in a choice-free manner, and then the duality can be obtained from it by adding points (via Stone’s Prime Filter Theorem). This point of view is particularly advantageous when one wants to understand additional operations on lattices.

Given a distributive lattice $D$, the canonical extension $D^\delta$ is a complete distributive lattice, and, using Stone’s Prime Filter Theorem, one can prove that it has enough completely join prime elements. For completeness we give the argument here. Before we do this, note that completely join and meet prime elements of a complete lattice $C$ come in splitting pairs $(p,m)$ satisfying

$$ \forall u\in C\qquad \left( p\nleq u \ \iff \ u\le m\right) $$

and thus the correspondence between completely join and meet prime elements is given by $p\mapsto \kappa (p)=\bigvee \{u\in C\mid p\nleq u\}$. We denote the poset of completely join prime elements by $J^\infty (C)$ and the poset of completely meet prime elements by $M^\infty (C)$. It then follows that $\kappa :J^\infty (C)\rightarrow M^\infty (C)$ is an isomorphism of posets.

Proposition 5. Let $D$  be a bounded distributive lattice and $D^\delta$ its canonical extension. Then every element of $D^\delta$ is a join of completely join prime elements and a meet of completely meet prime elements.

Proof. It suffices to show that for $u,v\in D^\delta$ with $u\nleq v$ there is a splitting pair $(p,m)$ as described above with $p\le u$ and $v\le m$. By the density condition for canonical extensions, $u\nleq v$ implies that there are $x\in F(D^\delta )$ and $y\in I(D^\delta )$ with $x\le u$, $v\le y$, and $x\nleq y$. Let $F_x=({\uparrow } x)\cap D$ be the filter of $D$ corresponding to $x$ and $I_y=({\downarrow } y)\cap D$ be the ideal corresponding to $y$. If $a\in F_x\cap I_y$, then

$$ x=\bigwedge F_x\le a\le \bigvee I_y=y $$

which contradicts the choice of $x$ and $y$. Thus, by Stone’s Prime Filter Theorem, there is a prime filter $\mathfrak p$ of $D$ with $F_x\subseteq \mathfrak p$ and $I_x\subseteq D\setminus \mathfrak p$. Now, letting $p=\bigwedge \mathfrak p$ and $m=\bigvee (D\setminus \mathfrak p)$, where the extrema are taken in $D^\delta$, we see that $p\le x\le u$ and $v\le y\le m$.

It remains to show that $(p,m)$ is a splitting pair. To this end, suppose $u\in D^\delta$ and $p\nleq u$, then there is $y\in I(D^\delta )$ with $u\le y$ but $p\nleq y$. Now $p\nleq y$ means that $\mathfrak p\cap I_y=\emptyset$ where $I_y=({\downarrow } y)\cap D$. Thus we have $I_y\subseteq D\setminus \mathfrak p$ and $u\le y\le m$ as required. Conversely, since $\mathfrak p\cap (D\setminus \mathfrak p)=\emptyset$, we have $p\nleq m$, and thus $u\le m$ implies $p\nleq u$. $\Box$

Given the canonical extension of a bounded distributive lattice $D$, the Stone space of $D$ may be obtained by topologising the set $X=J^\infty (D^\delta )$ with the topology given by the ‘shadows’ of the ideal elements on $X$, that is, by the sets $y\mapsto \{p\in J^\infty (D^\delta )\mid p\le y\}$  for $y\in I(D^\delta )$. Since $I(D^\delta )$ is closed under finite meets and arbitrary joins and the elements of $X$ are completely join prime, it follows that these sets form a topology. One can then show that the sets $\hat{a}=\{p\in J^\infty (D^\delta )\mid p\le a\}$ for $a\in D$ are precisely the compact open subsets of this space and they generate the topology. This yields a compact sober space in which the compact-open sets form a basis, which is closed under finite intersection. These spaces are known as Stone spaces or spectral spaces. In case the lattice is Boolean, all join primes are atoms and the corresponding space is a compact Hausdorff space with a basis of clopen sets. These spaces are (unfortunately) also known as Stone spaces or, for some authors, as Boolean spaces. We call the spaces for distributive lattices Stone spaces and the ones for Boolean algebras Boolean spaces. As mentioned above, the elements of $D$ correspond to the compact open subsets of the Stone space, the ideal elements of $D^\delta$ correspond to the open subsets. Order dually, the filter elements of $D^\delta$ correspond, again via the assignment $x\mapsto \{p\in J^\infty (D^\delta )\mid p\le x\}$, to the closed sets in the Stone topology for the lattice $D^\partial$ that is order dual to $D$. One can also understand these sets directly relative to the Stone space of $D$ itself. For this purpose some concepts from stably compact spaces are needed (see [36, Sect. 2] for further details): A subset $S$ of a space $X$ is called saturated provided it is an intersection of opens (this will yield precisely the downsets of $X=J^\infty (D^\delta )$). Then the sets $\{p\in J^\infty (D^\delta )\mid p\le x\}$ for $x\in X$ are precisely the compact saturated subsets of of the Stone space of $D$.

The specialisation order of a topology on a set $X$ is usually defined by $x\le y$ if and only if $x\in \overline{\{y\}}$ if and only if for every open subset $U\subseteq X$, we have $x\in U$ implies $y\in U$. In this setting this yields the reverse order to the order on $J^\infty (D^\delta )$ as inherited from $D^\delta$. Since it is more convenient to work with the order that fits with $D^\delta$, we work with the dual definition of specialisation order: $x\le y$ if and only if $y\in \overline{\{x\}}$ if and only if for every open subset $U\subseteq X$, we have $y\in U$ implies $x\in U$. Thus opens are downsets here rather than upsets.

Given a modality $\Box \text {:}\,D\rightarrow E$ (that preserves $1$ and $\wedge$), the extension $\Box ^\sigma =\Box ^\pi \text {:}\,D^\delta \rightarrow E^\delta$ (which we call $\Box ^\delta$) is completely meet preserving, see [23, Theorem 2.21]. Accordingly, it is completely determined by its action on the completely meet prime elements of $D^\delta$. This action is encoded using pairs from the Cartesian product of $X_E=J^\infty (E^\delta )$ and $X_D=J^\infty (D^\delta )$ via the relation

$$ xSy \ \iff \ \kappa (x)\ge \Box ^\delta (\kappa (y))\ $$

The relations thus obtained are characterised by three properties:

• (B1) ${\ge }\circ S\circ {\ge }=S$;

• (B2) $S[x]=\{y\in X_D\mid xSy\}$ is compact saturated for each $x\in X_E$;

• (B3) $\Box _S(U)\text {:}=(S^{-1}[U^c])^c=\{x\in X_E\mid \forall y\in X_D\ ( xSy \implies y\in U\}$ is compact open for each compact open subset $U\subseteq X_D$.

The first property is clearly satisfied, the second corresponds to the fact that $\Box ^\delta$ sends completely meet prime elements to ideal elements, and the third property corresponds to the fact that $\Box ^\delta$ restricts to a map from $D$ to $E$ (we give the details of the correspondence below in the order dual case of join and $0$ preserving modality).

Recovering the modal operator from the relation is easily seen to work just as in Kripke semantics. In fact, this approach via canonical extension makes clear why the box operation given by a Kripke relation should be defined the way it is:

$$\begin{aligned} \widehat{\Box ^\delta (a)}&=\left\{ x\in X_E\mid x\le \Box ^\delta (a)\right\} \\&=\left\{ x\in X_E\mid \bigwedge \{\Box ^\delta (\kappa (y))\mid a\le \kappa (y)\}\nleq \kappa (x)\right\} \\&=\left\{ x\in X_E\mid \forall y\in X\ (y\nleq a\implies \Box ^\delta (\kappa (y))\nleq \kappa (x))\right\} \\&=\left\{ x\in X_E\mid \forall y\in X\ (xSy\implies y\in \hat{a})\right\} \\&=\Box _S(\hat{a}).\\ \end{aligned}$$

Dual statements of course hold for a modality $\Diamond \text {:}\,D\rightarrow E$ (that preserves $0$ and $\vee$). In particular, $\Diamond ^\sigma =\Diamond ^\pi \text {:}\,D^\delta \rightarrow E^\delta$, which we call $\Diamond ^\delta$, is completely join preserving and the dual relation is given by $R=\{(x,y)\in X_E\times X_D\mid x\le \Diamond ^\delta (y)\}$. This relation satisfies

• (D1)   ${\le }\circ R\circ {\le }=R$;

• (D2)   $R[x]=\{y\in X_D\mid xRy\}$ is closed for each $x\in X_E$;

• (D3)   $\Diamond _R(U)\text {:}\,=R^{-1}[U]=\{x\in X_E\mid \exists y\ (xRy \text { and } y\in U)\}$ is compact open for each compact open $U\subseteq X_D$.

Finally, we recover the operation from a relation $R$ with these properties via

$$ \widehat{\Diamond ^\delta (a)}=\Diamond _R(\hat{a})=\left\{ x\in X_E\mid \exists y\in X_D\ (xRy\text { and } y\in \hat{a})\right\} =R^{-1}[\hat{a}]. $$

The conditions given here are well-known to duality theorists and may be found, e.g. in [32], but we give an algebraic derivation here based on the canonical extension. To this end first note that it is a simple fact from discrete (Birkhoff) duality that $\bigvee$-preserving maps on downset lattices, $f\text {:}\,{\fancyscript{D}}(X)\rightarrow {\fancyscript{D}}(Y)$, are in one-to-one correspondence with relations $R\subseteq Y\times X$ satisfying $\le \circ R\circ \le =R$. Also, the canonical extension of an operation preserving finite joins is completely join preserving [23, Theorem 2.21]. Thus, it suffices to show that the extensions $\Diamond ^\delta \text {:}\,D^\delta \rightarrow E^\delta$ of $\vee$ and $0$ preserving maps $\Diamond \text {:}\,D\rightarrow E$ are characterised within the $\bigvee$-preserving maps from $D^\delta$ to $E^\delta$ by the conditions (D2) and (D3).

Proposition 6. Let $k\text {:}\,D\rightarrow E$ be an order preserving map. Then $k^\sigma \text {:}\,D^\delta \rightarrow E^\delta$ sends filter elements to filter elements and consequently, if $k^\sigma$ has an upper adjoint, then this upper adjoint sends ideal elements to ideal elements.

Proof. By definition

$$ k^\sigma (u) =\bigvee \left\{ \bigwedge \{\,k(a) \mid a\in D\text { and } x\le a\le y\,\} \mid F(D^\delta )\ni x\le u\le y\in I(D^\delta )\right\} . $$

Thus for $u=x\in F(D^\delta )$ this definition reduces to

$$ k^\sigma (x) =\bigvee \left\{ \bigwedge \{\,k(a) \mid a\in D\text { and } x\le a\le y\,\} \mid x\le y\in I(D^\delta )\right\} , $$

and since $k$ is order preserving and $D\hookrightarrow D^\delta$ is compact this is the same as

$$ k^\sigma (x) =\bigwedge \{\,k(a) \mid a\in D\text { and } x\le a\,\}. $$

Thus $k^\sigma (x)\in F(D^\delta )$. Now suppose $g\text {:}\,E^\delta \rightarrow D^\delta$ is an upper adjoint to $k^\sigma$ and that $x\in J^\infty (E^\delta )$ and $y\in I(D^\delta )$, then we have

$$\begin{aligned} x\le g(y)&\iff k^\sigma (x)\le y\\&\iff \bigwedge _{x\le a\in D} k(a) \le y\\&\iff \exists a\in D\ (x\le a\text { and }k(a)\le y)\\&\ \implies \exists a\in D\ (x\le a\le g(y)). \end{aligned}$$

Now since $g(y)$ is the join of all the $x\in J^\infty (E^\delta )$ below it, it follows that it is the join of all the $a\in D$ below it and thus it is an ideal element. $\Box$

Theorem 4. Let  $f\text {:}\,D^\delta \rightarrow E^\delta$ be a $\bigvee$ -preserving map. Then $f=\Diamond ^\delta$ for some $\Diamond \text {:}\,D\rightarrow E$  if and only if the following conditions are met:

• 1. The upper adjoint of  $f$  sends completely meet prime elements to ideal elements;

• 2. $f$  sends elements of  $D$  to elements of $D$.

Proof If $f=\Diamond ^\delta$ for some $\Diamond \text {:}\,D\rightarrow E$, then it follows from Proposition 6 and the fact that $M^\infty (D^\delta )\subseteq I(D^\delta )$ that the upper adjoint of $f$ sends completely meet prime elements to ideal elements. The second condition is clearly also satisfied as $f$ restricted to $D$ is $\Diamond$.

For the converse, suppose $f\text {:}\,D^\delta \rightarrow E^\delta$ is $\bigvee$-preserving and satisfies the two conditions in the theorem. Define $\Diamond \text {:}\,D\rightarrow E$ by $\Diamond (a)\text {:}=f(a)$ for $a\in D$. Then certainly $\Diamond ^\delta =f$ on $D$. Now let $x\in F(D^\delta )$. Then

$$ \Diamond ^\delta (x)=\bigwedge \{\Diamond a\mid x\le a\in D\}=\bigwedge \{f(a)\mid x\le a\in D\}\ge f(x) $$

since $f$ is order preserving. On the other hand, if $m\in M^\infty (D^\delta )$ and $f(x)\le m$, then $x\le g(m)$ where $g\text {:}\,E^\delta \rightarrow D^\delta$ is the upper adjoint of $f$. Now since, by the first condition, $g(m)$ is an ideal element, there is $a\in D$ with $x\le a\le g(m)$. Thus $f(a)\le m$ and now, as $\Diamond$ is order-preserving

$$ \Diamond ^\delta (x)\le \Diamond (a)=f(a)\le m. $$

By the meet density of $M^\infty (D^\delta )$ in $D^\delta$, it follows that $\Diamond ^\delta (x)=f(x)$ and thus $\Diamond ^\delta =f$ on $F(D^\delta )$. Finally since both functions are $\bigvee$-preserving, it now follows that $\Diamond ^\delta =f$ on all of $D^\delta$. $\Box$

We are now ready to verify that the two conditions in the theorem correspond dually to the conditions (D2) and (D3) given above.

Proposition 7. Let $D$ and $E$ be bounded distributive lattices with dual spaces  $X_D$ and $X_E$ , respectively.  Let $f\text {:}\,D^\delta \rightarrow E^\delta$  be a $\bigvee$ -preserving map and $R\subseteq X_E\times X_D$  the corresponding dual relation. Then the following hold:

• 1. The upper adjoint of $f$ sends completely meet prime elements to ideal elements if and only if $R$  satisfies condition (D2);

• 2. $f$  sends elements of $D$  to elements of $D$  if and only if $R$ satisfies condition (D3).

Proof. Since the compact open subsets of $X_D$ are precisely the downsets in $X_D$ of elements of $D$, and since $f$ is obtained from $R$ as the map $U\mapsto R^{-1}[U]$ on downsets, or in other words as the map $u\mapsto \bigvee R^{-1}[{\downarrow } u\cap J^\infty (D^\delta )]$ on the canonical extensions, it is clear that $f$ sends elements of $D$ to elements of $D$ if and only if $R$ satisfies condition (D3). In order to prove the first equivalence, let $m\in M^\infty (E^\delta )$ and take $x'\in J^\infty (E^\delta )$ with $m=\kappa (x')$, then we have

$$\begin{aligned} \{x\in X_D\mid x\le g(m)\}&=\{x\in X_D\mid x\le g(\kappa (x'))\}\\&=\{x\in X_D\mid f(x)\le \kappa (x')\}\\&=\{x\in X_D\mid x'\nleq f(x)\}=(R[x])^c.\\ \end{aligned}$$

Thus $(R[x])^c$ is the downset in $X_D$ of $g(m)$ and this set is open if and only if $g(m)$ is an ideal element. $\Box$

The duality for homomorphisms is derivable in a similar manner. The pertinent facts are the following. Let $h\text {:}\,D\rightarrow E$ be a map between bounded distributive lattices. Then the following statements are equivalent:

• 1. $h$ is a bounded lattice homomorphism;

• 2. $h^\sigma =h^\pi$ is a complete lattice homomorphism;

• 3. $h^\sigma =h^\pi$ has a lower adjoint which sends completely join primes to completely join primes.

The dual of a bounded lattice homomorphism $h\text {:}\,D\rightarrow E$ is the map

$$ (h^\delta )^\flat \upharpoonright X_E: X_E\rightarrow X_D $$

and it is characterised by the property that, under this map, the pre-image of a compact open is always compact open. Such maps are usually called spectral maps or Stone maps. The dual of a spectral map $f\text {:}\,X_E\rightarrow X_D$ is given by inverse image and so is the canonical extension of the dual map.

If a lattice homomorphism also preserves an additional operation on the lattice, then one can derive, in the same way as we’ve done above, that the dual maps will satisfy bisimulation conditions with respect to the relation corresponding to the additional operation. We finish this section by considering this situation.

Consider a diagram

where $E_i$ and $D_i$ are bounded distributive lattices, the $h_i$ are lattice homomorphisms, and the maps $\Diamond _i$ are operators (the argument is similar for $n$-ary operators). We want to obtain the dual condition to the diagram commuting. If $D_1=D_2$, and $h_1$ is equal to $h_2$, this is simply the statement that it is a homomorphism with respect to the diamonds. To this end one may first show that the following statements are equivalent:

• 1. $h_2\circ \Diamond _1=\Diamond _2\circ h_1$;

• 2. $h_2^\delta \circ \Diamond _1^\sigma =\Diamond _2^\sigma \circ h_1^\delta$;

• 3. $\forall x\in X_{E_1}\ h_2^\delta (\Diamond _1^\sigma (x))=\Diamond _2^\sigma (h_1^\delta (x))$

• 4. $\forall x\in X_{E_1}\forall z\in X_{D_2}\ (z\le h_2^\delta (\Diamond _1^\sigma (x)) \ \iff \ z\le \Diamond _2^\sigma (h_1^\delta (x))).$

The equivalence of (1) and (2) follows from the fact that the first map is an operator and the second one order preserving on either side of the equality since this implies that $(h_2\circ \Diamond _1)^\sigma =h_2^\delta \circ \Diamond _1^\sigma$ and $(\Diamond _2\circ h_1)^\sigma =\Diamond _2^\sigma \circ h_1^\delta$, see [22, Theorem 4.3]. The equivalence of (2) and (3) follows because all the extended functions are completely join preserving and $X_{E_1}$ is join-dense in $E^\delta _1$. The last two are equivalent because $X_{D_2}$ is join-dense in $D_2^\delta$. Now denoting the dual of $h_i$ by $f_i$ and the dual of $\Diamond _i$ by $R_i$ for $i=1$ and $2$, we get

$$\begin{aligned} z\le h_2^\delta (\Diamond _1^\sigma (x))&\iff f_2(z)\le \Diamond _1^\sigma (x)\\&\iff f_2(z)R_1 x \end{aligned}$$

and

$$\begin{aligned} z\le \Diamond _2^\sigma (h_1^\delta (x))&\iff \exists z'\in X_{E_2}\ (z\le \Diamond _2^\sigma (z')\text { and } z'\le h_1^\delta (x)) \\&\iff \exists z'\in X_{E_2}\ (zR_2z'\text { and }f_1(z')\le x)\\ \end{aligned}$$

So the above diagram commutes if and only if

$$ \forall z\in X_{D_2}\forall x\in X_{E_1}\left[ f_2(z)R_1 x\iff \exists z'\in X_{E_2}\ (zR_2z' \text { and }f_1(z')\le x)\right] . $$

Note that the backward implication can be simplified as we can bring the quantifier outside to get

$$ \forall z\in X_{D_2}\forall z'\in X_{E_2}\forall x\in X_{E_1}\left[ (zR_2z'\text { and }f_1(z')\le x) \implies f_2(z)R_1 x\right] . $$

A special case of this condition is the one obtained by choosing $x=f_1(z')$:

$$ \forall z\in X_{D_2}\forall z'\in X_{E_2}\left[ zR_2z'\implies f_2(z)R_1 f_1(z')\right] . $$

On the other hand, since ${\le }\circ R_1\circ {\le }=R_1$ the latter condition also implies the previous one. So the diagram commutes if and only if the following two conditions hold:

($\Diamond$back):

$\forall z\in X_{D_2}\forall x\in X_{E_1}\left[ f_2(z)R_1 x\implies \exists z'\in X_{E_2}\ (zR_2z'\text { and }f_1(z')\le x)\right]$.

($\Diamond$forth):

$\forall z\in X_{D_2}\forall z'\in X_{E_2}\left[ zR_2z'\implies f_2(z)R_1 f_1(z')\right]$.

In the case where $h_1=h_2$ these are precisely the conditions dual to being a $\Diamond$-homomorphism between bounded distributive lattices. For box operations $\Box _1$ and $\Box _2$ with dual relations $S_1$ and $S_2$, respectively, we get order-dual dual conditions, namely:

($\Box$back):

$\forall z\in X_{D_2}\forall x\in X_{E_1}\left[ f_2(z)S_1 x\implies \exists z'\in X_{E_2}\ (zS_2z'\text { and }f_1(z')\ge x)\right]$.

($\Box$forth):

$\forall z\in X_{D_2}\forall z'\in X_{E_2}\left[ zS_2z'\implies f_2(z)S_1 f_1(z')\right]$.

2.6 From Canonical Extensions to Esakia Spaces

As we have seen in Proposition 2 of Sect. 2.3, ($\pi$-)canonical extension provides a choice free approach to duality for Heyting algebras. In Sect. 2.5 we have seen how to obtain Stone duality from canonical extension. In this section we spell out how to move between the canonical extension of a Heyting algebra and its Esakia dual space. In order to witness the Heyting implication, we will make use of the results of Sect. 2.4 relating Heyting algebras to pairs of adjoint maps. It can also be done directly as we will indicate at the end of this section, however, we feel that the approach via adjoint pairs of maps is the most transparent and reflects most directly the spirit of the work of Leo Esakia.

Accordingly we need the following correspondence results:

• 1. Sublattices $D\hookrightarrow E$ of bounded distributive lattices $E$ correspond dually to spectral quotients, but these can most simply be described not as certain equivalence relations but as certain quasi-orders on the dual Stone space [45]. A quasi-order gives rise to an equivalence relation and to an order on the quotient which will be the specialisation order of the spectral quotient space: Given a spectral space $X$, its spectral quotients are in one-to-one correspondence with the so-called compatible quasi-orders $\preceq \,\subseteq X\times X$ [17, Theorem 6]. A compatible quasi-order on a Stone space $X$ is a quasi-order on $X$ satisfying the following separation condition for all $x,y\in X$

  $$ x\not \preceq y \implies \exists U\subseteq X\ \ (U\text {compact open and a} \preceq \text {-downset, } y\in U\text { and } x\not \in U). $$

  Here $U$ is a $\preceq$-downset provided for all $z,z'\in X$ we have $z\preceq z'\in U$ implies $z\in U$. Given a sublattice $D\hookrightarrow E$, the corresponding quasi-order is given by $\preceq _D\,=\{(x,y)\in X_E\times X_E\mid \forall a\in D\ (y\le a \implies x\le a)\}$ where the comparisons of $x$ and $y$ with $a$ are made in $E^\delta$ (note $D\subseteq D^\delta \hookrightarrow E^\delta$). Given a compatible quasi-order, $\preceq$ on $X_E$, the dual space of the corresponding sublattice of $E$ is the quotient space $X_D=(X_E/{\approx }, \tau _\preceq )$, where ${\approx }={\preceq }{\cap }{\succeq }$ and $\tau _\preceq$ is given by those open subsets of the space $X_E$ which are also ${\preceq }$-downsets. We will denote the space $(X/{\approx }, \tau _{\preceq })$ given by a given compatible order $\preceq$ on a Stone space $X$ by $X/{\preceq }$. The map dual to the embedding $D\hookrightarrow E$ is the quotient map $X_E\twoheadrightarrow X_E/{\preceq }$ and the relation $R$ corresponding to $D\hookrightarrow E$ viewed as a $0$ and $\vee$ preserving map from $D$ to $E$ is the relation $xR[x']_\approx$ iff $x\preceq x'$.

• 2. A pair of maps $\Diamond \text {:}\,D\leftrightarrows E\text {:}\,\Box$ is an adjoint pair with $\Diamond$ the lower adjoint and $\Box$ the upper adjoint if and only if the relation $R$ dual to $\Diamond$ and the relation $S$ dual to $\Box$ are converse to each other. That is, $S=R^{-1}$. The interesting direction of this fact is true because of the following string of equivalences:

  $$\begin{aligned} xRx'&\iff x\le \Diamond ^\delta (x')\\&\iff \kappa (x)\ngeq \Diamond ^\delta (x')\\&\iff \Box ^\delta (\kappa (x))\ngeq x'\\&\iff \kappa (x')\ge \Box ^\delta (\kappa (x))\iff x'Sx. \end{aligned}$$

Now we just need one more correspondence result before we can get the Esakia duality for Heyting algebras. The following proposition is a generalisation of Theorem 4.5 of Chap. III in Esakia’s book [14], which proves the same statement, but just for Heyting algebras. In addition (the hard direction) is the algebraic dual of the result needed in Priestley duality that each clopen downset comes from a lattice element.

Proposition 8. Let $B$  be a Boolean algebra with dual space  $X_B$ , and let  $D$  be a sublattice of $B$  with corresponding compatible quasi-order $\preceq$ on $X_B$.  Then $D$ generates $B$ as a Boolean algebra if and only if $\preceq$ is antisymmetric and thus a partial order.

Proof. Suppose $D$ generates $B$ as a Boolean algebra, and let $x,x'\in X_B$ with $x\ne x'$. Since $x$ and $x'$ are filter elements of $B^\delta$, there is $b\in B$ with $x\le b$ but $x'\nleq b$. Since $D$ generates $B$ as a Boolean algebra, $b=\bigvee _{i=1}^n(\bigwedge _{j=1}^{m_i} a_{ij})$, where each $a_{ij}$ is either an element of $D$ or the complement of one. Now $x\le b$ and $x$ an atom implies $x\le \bigwedge _{j=1}^{m_i} a_{ij}$ for some $i$. Rewriting the latter conjunction in the form $(\bigwedge _{j=1}^k a_j)\wedge (\bigwedge _{j=k+1}^{m_i} \lnot a_j)$, we obtain from $x'\nleq b$ that $x'\nleq (\bigwedge _{j=1}^k a_j)\wedge (\bigwedge _{j=k+1}^{m_i} \lnot a_j)$ and thus there is a $j\in \{1,\ldots ,k\}$ with $x'\nleq a_j$ or there is $j\in \{k+1,\ldots ,m_i\}$ with $x'\nleq \lnot a_j$. In the first case we obtain $x\le a_j$ and $x'\nleq a_j$ and in the second case we obtain $x\nleq a_j$ and $x'\le a_j$. Thus, by the definition of $\preceq$, either $x'\not \preceq x$ or $x\not \preceq x'$ and thus $\preceq$ is antisymmetric.

For the converse, fix first $x\in X_E$. For each $y\in X_E$ with $x\not \preceq y$, there is $a_y\in D$ with $y\le a_y$ but $x\nleq a_y$, and for each $y\in X_E$ with $y\not \preceq x$, there is $c_y\in D$ with $x\le c_y$ but $y\nleq c_y$. And thus the equivalence classes of ${\approx }={\preceq }\cap {\succeq }$ are given by

$$ \bigvee [x]_\approx =\left( \bigwedge _{x\not \preceq y\in X_E}\lnot a_y\right) \wedge \left( \bigwedge _{y\not \preceq x\in X_E} c_y\right) $$

where the joins and meets are of course taken in $E^\delta$.

Now suppose $\preceq$ is antisymmetric. Then $[x]_\approx =\{x\}$ and thus $\bigvee [x]_\approx =x$ for each $x\in X_E$. Thus, for $b\in B$ and for each $x\in X_E$ with $x\le b$ we get

$$ b\ge x=\left( \bigwedge _{x\not \preceq y\in X_E}\lnot a_y\right) \wedge \left( \bigwedge _{y\not \preceq x\in X_E} c_y\right) \!\!. $$

Let ${<}D{>}$ denote the Boolean subalgebra of $B$ generated by $D$. Applying compactness of $E^\delta$ to the fact that $\left( \bigwedge _{x\not \preceq y\in X_E}\lnot a_y\right) \wedge \left( \bigwedge _{y\not \preceq x\in X_E} c_y\right)$ is below $b$, we conclude that there is a finite submeet which gets below $b$. That is, there is $b_x\in {<}D{>}$ with $x\le b_x\le b$. Since $X_E$ is join-dense in $B$ it follows that

$$ b=\bigvee _{b\ge x\in X_E}b_x. $$

Again by compactness of $E^\delta$, there are $x_1,\ldots ,x_n\in X_E$ with $x_i\le b$ and $b\le \bigvee _{i=1}^nb_{x_i}$. Since each $b_x\le b$ we actually have equality and thus $b\in {<}D{>}$. $\Box$

Theorem 5. (Priestley duality [41]) The category of bounded distributive lattices is dually equivalent to the category whose objects are Boolean spaces each equipped with a compatible partial order and whose morphisms are continuous and order preserving maps.

Proof. This follows from the above results and the fact that the category of distributive lattices is equivalent to the category of lattice embeddings $D\hookrightarrow B$ such that $D$ generates $B$ with pairs of maps making commutative diagrams, e.g.

where the topology on the lower spaces are those that are downsets of the respective partial orders that are open in the respective topologies of the upper spaces. Saying that the diagram on the left commutes is equivalent to saying that the one on the right commutes, and this in turn is the same as saying that the maps $f$ and $f'$ are equal as set maps and that they are continuous both in the Boolean topology of the spaces on the top and in the spectral topology of the spaces on the bottom. This in turn is easily seen to be equivalent to saying that $f=f'$ is both continuous in the Boolean topology and order preserving. $\Box$

The ordered spaces $(X,\le )$ where $X$ is a Boolean space and $\le$ is a compatible partial order on $X$ are of course well known by now as Priestley spaces and the maps $f\text {:}\,(X,\le )\rightarrow (Y,\le )$ which are both continuous and order preserving are the Priestley maps. For the Esakia duality we need also the notion of a bounded morphism. A map $f\text {:}\,X\rightarrow Y$ between Priestley spaces is called a bounded morphism provided it is continuous, order preserving, and for each $x\in X$ and each $y\in Y$ with $y\le f(x)$, there is $z\in X$ with $z\le x$ and $y=f(z)$.

Theorem 6. (Esakia Duality [12]) The category of Heyting algebras is dually equivalent to the category whose objects are Priestley spaces $(X,\le )$  such that, for each clopen subset $U$ of $X$,  the set ${\uparrow }U$  is also clopen and whose morphisms are the bounded morphisms.

Proof. For objects, we use the fact that a Heyting algebra corresponds to an adjoint pair $e\text {:}\,D\rightleftarrows B\text {:}\,g$ where $e$ is an embedding whose image generates $B$. The dual of these embeddings $e$ are precisely the Priestley spaces $(X,\le )$ and the relation $R$ corresponding to the quotient map $X\twoheadrightarrow (X,\le )$ is, as remarked above, the relation

$$ xR\{x'\}(=[x']_\approx )\quad \iff \quad x\le x'. $$

Accordingly, we think of $R$ simply as being $\le$ (identifying $\{x\}$ with $x$ for each $x\in X$). Note that, since the relation $R=\le$ is the relation corresponding to the embedding $e$ (as stated in item 1 in the beginning of this section), $\le$ satisfies (D1) through (D3) (this is a consequence of the requirements for being a compatible quasi-order). The fact that $e$ has an upper adjoint is, by the second item in the list at the beginning of this section, equivalent to the fact that the reverse relation ${R^{-1}}={\ge }$ satisfies conditions (B1) through (B3). The condition (B1), $\ge \circ \ge \circ =$ being equal to $\ge$, is vacuously true. Condition (B2) states that ${\downarrow }x$ is closed in $X$ and this also always holds because

$$ {\downarrow }x=\bigcap \{U\mid x\in U, U\text { a clopen downset}\} $$

is compact saturated by (D3). Finally (B3) requires that for each clopen subset $U$ of $X$, the set $({\uparrow }U)^c$ is a clopen downset, and this is equivalent to saying that for each clopen subset $U$ of $X$, the set ${\uparrow }U$ itself is clopen. Therefore this last condition is the only additional condition on the Priestley space $(X,\le )$.

Homomorphisms between Heyting algebras correspond to commutative diagrams

The commutativity on the algebraic side with respect to the maps $e_i$ is just the Priestley map condition that $f=f'$ is continuous in the Boolean topologies and is order preserving. The commutativity of the diagram with respect to the maps $g_i$ is precisely of the form treated at the very end of Sect. 2.5 for $\Box$ operations. Thus the additional requirements for this continuity are:

($\Box$back):

$\forall z\in X_{D_2}\forall x\in X_{B_1}\left[ f'(z)\ge _1 x\implies \exists z'\in X_{B_2}\ (z\ge _2z'\text { and }f(z')= x)\right]$.

($\Box$forth):

$\forall z\in X_{D_2}\forall z'\in X_{B_2}\left[ z\ge _2z'\implies f'(z)\ge _1 f(z')\right]$.

Now replacing $id_i\text {:}\,X_{B_i}\rightarrow X_{D_i}$ by the corresponding Priestley space $(X_i,\le _i)$ and using the fact that $f'=f$, we obtain the Esakia dual map

which is order preserving and continuous and satisfies the conditions:

($\Box$back):

$\forall z\in X_2\forall x\in X_1\left[ f(z)\ge _1 x\implies \exists z'\in X_2\ (z\ge _2z'\text { and }f(z')= x)\right]$.

($\Box$forth):

$f$ is order preserving.

However, since $f$ is already required to be order preserving and continuous, all that remains is the ($\Box$back) condition, which is precisely the condition defining bounded morphisms. $\Box$

Remark 1. In the same manner as we have derived the Priestley and Esakia dualities from our descriptions of the corresponding categories of maps, we could derive the duality for S4 modal algebras as the duals of adjoint pairs $h\text {:}\,D\rightleftarrows B\text {:}\,e$, that is, Boolean spaces with a compatible quasi-order such that, for each clopen subset $U$, the set ${\uparrow }U$ is also clopen with continuous quasi-order preserving (quasi)bounded morphisms.

Remark 2. A more direct approach to duality for Heyting algebras is to take as dual space for a Heyting algebra $A$, the dual of the underlying lattice equipped with the ternary Kripke relation obtained from the binary implication operation with spectral maps that are bounded morphisms for this ternary relation. This is not as nice a presentation but is completely equivalent. We show here how to derive the ternary relation corresponding to implication on a Heyting algebra. Let $A$ be a Heyting algebra and $\rightarrow \text {:}\,A^\partial \times A\rightarrow A$. Here $A^\partial$ stands for the order dual of $A$. With this flip in the first coordinate, $\rightarrow$ is a dual operator and we can compute the corresponding relation $S=S_\rightarrow$ using the $\pi$-canonical extension of $\rightarrow$. As we’ve already seen in the unary case we get the same relation, with some switching of the order of coordinates as for its lower adjoint $\wedge$. For the following computation, one needs to know that the canonical extension of meet is the meet of the canonical extension [22, Lemma 4.4]. For all $x,y,z\in X_A$ we have

$$\begin{aligned} S(x,y,z)&\iff \kappa (x)\ge y\rightarrow ^\pi \kappa (z)\\&\iff x\nleq y\rightarrow ^\pi \kappa (z)\\&\iff x\wedge ^\sigma y\nleq \kappa (z)\\&\iff z\le x\wedge y\\&\iff z\le x \text { and } z\le y \end{aligned}$$

which is of course interderivable with the binary relation $\le$. We leave it as an exercise for the reader to check bounded morphisms for this ternary relation are precisely the same as those in the Esakia duality.

2.7 Esakia’s Lemma and Sahlqvist Theory

Esakia formulated and proved Esakia’s lemma in order to prove that the topological dual of a Heyting algebra homomorphism is a bounded morphism. Esakia’s lemma has since played an important role in modal and intuitionistic model theory. In particular, it was used by Sambin and Vaccaro in their simplified proof of Sahlqvist’s Theorem [44]. A generalisation of Esakia’s lemma, formulated in algebraic terms [22, Lemma 3.8], was the key idea in our proof with Bjarni Jónsson of a fact regarding compositionality of canonical extensions of maps. We then used this result to prove the functoriality of canonical extension (this corresponds to Esakia’s application of his lemma) as well as Sahlqvist-type theorems (corresponding to Sambin and Vaccaro’s application of Esakia’s Lemma).

We begin by stating Esakia’s Lemma as Esakia stated it [12, Lemma 3].

Lemma 1. If $(X,R)$ is an Esakia space and $\fancyscript{C}$ is a downward directed family of closed subsets of $X$, then

$$ R^{-1}\left[ \bigcap \fancyscript{C}\right] =\bigcap R^{-1}\left[ \fancyscript{C}\right] . $$

In canonical extension language, this translates as follows. Let $A$ be a Heyting algebra and let $B=A^-$ be its Booleanisation. Let $X=J^\infty (A^\delta )$, then $A^\delta =\fancyscript{D}(X)$ and $B^\delta =\fancyscript{P}(X)$. The subsets of $X$ that are closed in topological terms are precisely the filter elements of $B^\delta$. The relation $R$ on the Esakia space of $A$ is, as we have seen in the previous section, the relation $S_\Box$ dual to the box operation on $B$ given by

$$ \Box \text {:}\, B\mathop {\longrightarrow }\limits ^{g}A\mathop {\longrightarrow }\limits ^{e}B. $$

It is not hard to see that, on a Boolean algebra, a relation dual to a box operation is also dual to a diamond operation. Indeed the relation $R$ on the Boolean space underlying the Esakia space of $A$ is the relation $S_\Box$ for the above given box operation and it is also the relation $R_\Diamond$ for the conjugate diamond operation, $\Diamond =\lnot \Box \lnot$. For this operation, we saw in the previous section that $\Diamond ^\delta$ on $B^\delta$ is just the operation $S\mapsto R^{-1}[S]$ on $\fancyscript{P}(X)$. Thus Esakia’s lemma says that for any down-directed family $\fancyscript{C}$ of filter elements we have that

$$ \Diamond ^\delta \left( \bigwedge \fancyscript{C}\right) =\bigwedge \{\Diamond ^\delta (c)\mid c\in \fancyscript{C}\}, $$

where the infima are taken in $B^\delta$. That is, while $\Diamond ^\delta$ in general only preserves joins, it also preserves down-directed meets of filter elements. Order dually, of course this same statement also means that $\Box ^\delta$ preserves directed joins of ideal elements.

This lemma, which holds for the canonical extension of the box operation associated with a Heyting algebra actually holds for canonical extensions of order preserving maps between distributive lattices in general. That is the content of Lemma 3.8 in [22], which was stated as follows.

Lemma 2. Let $A$ and $B$ be bounded distributive lattices, and suppose $f\text {:}\,A\rightarrow B$ is isotone. For any down-directed set $\fancyscript{D}$ of filter elements of $A^\delta$,

$$ f^\sigma \left( \bigwedge \fancyscript{D}\right) =\bigwedge \{f^\sigma (x)\mid x\in \fancyscript{D}\}. $$

In [22], we used this lemma to prove that, for every $x\in X_B$ and for every element $u\in A^\delta$ that satisfies the inequality $x\le f^\sigma (u)$, there is a minimal such solution below $u$. This is the crucial fact used in [22] to prove that if $f$ is join preserving in each coordinate, then $f^\sigma$ is Scott continuous. This, in conjunction with the following theorem, then leads to a proof of functoriality of canonical extension and to Sahlqvist-type results.

Theorem 7. [22, Theorem 4.3] Let $g\text {:}\,A\rightarrow B$ be order preserving and $f\text {:}\, B\rightarrow C$ be such that $f^\sigma$ is continuous, then $(f\circ g)^\sigma = f^\sigma \circ g^\sigma$.

In order to prove functoriality of canonical extension one must show that $h\circ \Diamond _1=\Diamond _2\circ h$ implies that $h^\delta \circ \Diamond _1^\sigma =\Diamond _2^\sigma \circ h^\delta$. This is also crucial in the derivation of the description of bounded morphisms as we saw at the end of Sect. 2.5. The argument, on the basis of Theorem 7, goes as follows:

$$\begin{aligned}&h\circ \Diamond _1&=\Diamond _2\circ h\\ \implies \qquad&(h\circ \Diamond _1)^\sigma&=(\Diamond _2\circ h)^\sigma \\ \mathop {\implies }\limits ^{Th.7} \qquad&h^\sigma \circ (\Diamond _1)^\sigma&=(\Diamond _2)^\sigma \circ h^\sigma \\ \implies \qquad&h^\delta \circ (\Diamond _1)^\sigma&=(\Diamond _2)^\sigma \circ h^\delta . \end{aligned}$$

The method for showing that equational properties holding on a lattice with additional operations lift to the canonical extension is similar, and this is the subject of Sahlqvist theory. An equation may be seen as the equality of two compositions of maps that are either basic operations or juxtapositions of such ($f\text {:}\,A\rightarrow B$ and $g\text {:}\,C\rightarrow D$ yield $[f,g]\text {:}\,A\times C\rightarrow B\times D$). Showing that the equation lifts is then a matter of showing that canonical extension commutes with composition and juxtaposition. In our paper [23] with Bjarni Jónsson, we no longer relied (directly) on Esakia’s lemma for these kind of arguments, but developed a theory based on topology which allows a more transparent and uniform treatment of issues concerning the interaction of extending maps and composing them.

2.8 Esakia Spaces as Completions of Universal Models

One of the purposes of the dual space of a bounded distributive lattice is to supply a representation theorem: every bounded distributive lattice may be realised as a sublattice of a powerset lattice. For some lattices, one does not need something so complicated as the dual space to obtain such a representation. This is true, for example, in computer science in the study of classes of formal languages. By definition, these are given as sublattices of the powerset of the set of all words $A^*$ in some alphabet $A$. This is also true for lattices that have “enough" join prime elements in the sense that each element is a join of join prime elements. This is true, e.g., for free bounded distributive lattices where the pure conjunctions of generators join generate and are join prime. This is also true for (finitely generated) free Heyting algebras. This latter fact is at the lattice theoretic origin of the so-called universal models of intuitionistic propositional logic.

Let $N\in {\mathbb N}$, $N\ge 1$, and let $A=F_{HA}(N)$ be the free Heyting algebra on $N$ generators. Then $A$ is infinite, but, as a lattice, it may be built incrementally as the direct limit (or colimit in categorical terms) of the finite sublattices $A_n$ consisting of all elements of implicational rank less than or equal to $n$ (meaning that there is a term describing such an element in terms of the generators in which the maximum number of nested implications is less than or equal to $n$). This direct limit, and its dual inverse limit of finite posets, have been studied extensively by Ghilardi [27–30] and others [3, 7, 8]. The dual inverse limit may be built up in a uniform way as follows.

Given a poset $(X,\le )$, we say that a subset $S$ of $X$ is rooted if there exists $p\in S$ such that $q\le p$ for each $q\in S$. In this case, we call $p$ the root of $S$. It follows from the definition that a root of a rooted set is unique. We denote by ${\fancyscript{P}}_r(X)$ the set of all rooted subsets of $(X, \le )$. We also let $root: {\fancyscript{P}}_r(X) \rightarrow X$ be the map sending each rooted subset $S$ of $X$ to its root. Now define the sequence $\left\{ X_n\right\} _{n\in {\mathbb N}}$ of finite posets as follows:

$$\begin{aligned} X_0&=J(F_{DL}(N))(={\fancyscript{P}}(N))\qquad X_1 ={\fancyscript{P}}_r(X_0)\\ \text{ For } n\ge 1\quad X_{n+1}&=\{\tau \in {\fancyscript{P}}_r(X_n)\mid \forall T\in \tau \ \forall S\in X_n\ \\&\qquad \quad (S\le T\ \implies \ \exists T'\in \tau \ (T'\le T \text{ and } root(S)=root(T'))\}. \end{aligned}$$

The condition defining $X_{n+1}$, which was first given in [27] might seem strange but it can be derived using correspondence theory in a straight forward way [3].

One can then show that the functions $root\text {:}\, {\fancyscript{P}}_r(X_n) \rightarrow X_n$ remain surjective when one restricts the domains to $X_{n+1}$. We denote by $\nabla$ the sequence

The dual sequence

has (the lattice underlying) $A=F_{HA}(N)$ as its direct limit, and the maps $i_n$ are the duals of the root maps and are thus the upper adjoints of the forward image maps of the root maps. An observation, also dating back to Ghilardi, is that the maps in the sequence $\nabla$ have upper adjoints, or in other words that the maps $i_n$ send join primes to join primes and thus the join primes of the lattices $D_n$ remain join prime all the way up the chain and thus also in $A$, which is then join-generated by the set $J(A)$ of join prime elements of $A$.

The upper adjoint maps are the maps $X_n\rightarrow X_{n+1}, x\mapsto {\downarrow }x$. Thus $\nabla$ is both an inverse and a direct limit system

From the above analysis of the sequence $\nabla$, we see the following relationship:

$$\begin{aligned} \text{ The } \text{ Esakia } \text{ space } \text{ of } A \text{ is } \ X&=\varprojlim X_n\\ \text{ The } \text{ set } \text{ of } \text{ join } \text{ primes } \text{ of } A \text{ is } \ J(A)&=\mathrm{lim}_\rightarrow X_n. \end{aligned}$$

Here the inverse limit may be taken in topological spaces and we obtian the Esakia space with its topology. The direct limit (or co-limit in category theoretic terms) may be taken in posets to obtain the collection of all join-irreducibles in $A$ with the induced order. By the above analysis it is clear that $A$ may be given a set representation in $J(A)$ via the embedding $A\hookrightarrow \fancyscript{P}(J(A))$ where $a\in A$ is sent to $\{x\in J(A)\mid x\le a\}$. Note that the sets $\{x\in J(A)\mid x\le a\}$ for $a\in A$ are precisely the downsets of finite antichains in the poset $J(A)$. However, the poset $J(A)$ is fairly complicated and a smaller one suffices to obtain a set representation of $A$. This is the point of the so called (N-)universal model. The universal model, $U$, was already anticipated in [9] and originates with [43, 46]. See also [1, 33].The subject was revived in [2], where it was, among other, shown that the poset underlying the universal model consists of the finite height elements of the Esakia space of $A$ (see [2, Theorem 3.2.9]). The interpretation that is part of the universal model is precisely the map sending $a\in A$ to $\{x\in U\mid x\le a\}$. Also, the so-called de Jongh formulas show that the downset (in our order) (as well as the completement of the upset) of such a finite height element of the Esakia space $X$ is (are) clopen (see [2, Theorem 3.3.2]). It is easy to see that the downset of a point in a Priestley space is clopen if and only if the point corresponds to a principal prime filter (and thus to a join prime element of the dual lattice). Thus the poset underlying the universal model $U$ is contained in $J(A)$ and, as mentioned above, already the points in $U$ are enough to obtain a set representation of $A$ (see, e.g. [2, Theorem 3.2.20]). In this representation, an element $a\in A$ is of course sent to $\{x\in U\mid x\le a\}$, the so-called definable subsets of the universal model $U$. While $U$ is simpler than $J(A)$, no characterisation of the definable sets, $\{x\in U\mid x\le a\}$ for $a\in A$, is known.

The fact that A is representable as a lattice of subsets of $J(A)$ and of $U$ yields a connection between these posets and the Esakia space of $A$. This connection is a special case of results presented in [19] and this is the last topic in this survey of recent developments in duality theory as they relate to Esakia’s work. Thus we will outline here those results of [19] that are concerned just with set representations of lattices. For further details see [19, Sect. 1] and the forthcoming journal paper [18]. The key initial observation of [19], relative to set representations of lattices, is that a set representation $D\hookrightarrow \fancyscript{P}(X)$ may faithfully be seen as a special kind of quasi-uniform space.

A quasi-uniform space is a pair $(X,\fancyscript{U})$, where $X$ is a set, and $\fancyscript{U}$ is a collection of subsets of $X\times X$ having the following properties:

• 1. $\fancyscript{U}$ is a filter of subsets of $X\times X$ contained in the up-set of the diagonal $\Delta =\{(x,x)\mid x\in X\}$;

• 2. for each $U \in \fancyscript{U}$, there exists $V\in \fancyscript{U}$ such that $V\circ V\subseteq U$;

The collection $\fancyscript{U}$ is called a quasi-uniformity and its elements are called entourages and should be thought of as the epsilon-neighboorhoods of the diagonal in a quasi-metric space, i.e., sets of the form $U\supseteq \{(x,y)\mid d(x,y)<\epsilon \}$ for some $\epsilon >0$. The condition (2) corresponds to the triangle inequality. A quasi-uniform space is said to be a uniform space provided the converse, $U^{-1}$, of each entourage $U$ is again an entourage of the space (this corresponds to the symmetry axiom for metrics).

A function $f\text {:}\,(X,\fancyscript{U})\rightarrow (Y,\fancyscript{V})$ between quasi-uniform spaces is uniformly continuous provided $(f\times f)^{-1}(V)\in \fancyscript{U}$ for each $V\in \fancyscript{V}$. Sometimes we will write $f\text {:}\,X\rightarrow Y$ is $(\fancyscript{U},\fancyscript{V})$-uniformly continuous instead to express this fact. A quasi-uniform space $(X,\fancyscript{U})$ always gives rise to a topological space. This is the space $X$ with the induced topology, which is given by $V\subseteq X$ is open provided, for each $x\in V$, there is $U\in \fancyscript{U}$ such that $U(x)=\{y\in X\mid (x,y)\in U\}\subseteq V$. In general, several different quasi-uniformities on $X$ give rise to the same topology. We will assume that all spaces are Komolgorov, that is, the induced topology is $T_0$. This requirement is equivalent to the intersection of all the entourages in $\fancyscript{U}$ being a partial order rather than just a quasi-order on $X$. In case a quasi-uniform space $(X,\fancyscript{U})$ is not separated, it may be mapped to its so-called Komolgorov quotient which is given by the equivalence relation obtained by intersecting all the $U\cap U^{-1}$ for $U\in \fancyscript{U}$, or equivalently, given by the partial order reflection of the quasi-order corresponding to $\fancyscript{U}$. For the basic theory of uniform spaces and quasi-uniform spaces, we refer to [6, 16].

We are now ready to explain how set representations may be viewed, up to isomorphism, as certain quasi-uniform spaces, which we will call Pervin spaces. First of all, instead of working with lattice representations $e\text {:}\,D\hookrightarrow \fancyscript{P}(X)$, we will work with sublattices $\fancyscript{L}\subseteq \fancyscript{P}(X)$. Now, given a set $X$, we denote, for each subset $A\subseteq X$, by $U_A$ the subset

$$ (A^c\times X)\cup (X\times A)=\{(x,y)\mid x\in A\implies y\in A\} $$

of $X\times X$. Given a topology $\tau$ on $X$, the filter $\fancyscript{U}_\tau$ generated by the sets $U_A$ for $A\in \tau$ is a quasi-uniformity on $X$. The quasi-uniform spaces $(X,\fancyscript{U}_\tau )$ were first introduced by Pervin [40] and are now known in the literature as Pervin spaces. Given a sublattice, $\fancyscript{L}\subseteq \fancyscript{P}(X)$, we define $(X,\fancyscript{U}_{\fancyscript{L}})$ to be the quasi-uniform space whose quasi-uniformity is the filter generated by the entourages $U_{L}$ for $L\in \fancyscript{L}$. Here we will call this more general class of quasi-uniform spaces Pervin spaces. The lattice $\fancyscript{L}$ may be recovered from $(X,\fancyscript{U}_{\fancyscript{L}})$ as the blocks of the space. The blocks of a space $(X,\fancyscript{U})$ are the subsets $A\subseteq X$ such that $U_A$ is an entourage of the space, or equivalently, those for which the characteristic function $\chi _A\text {:}\,X\rightarrow 2$ is uniformly continuous with respect to the Sierpiński quasi-uniformity on $2$, which is the one containing just $2^2$ and $\{(0,0),(1,1),(1,0)\}$.

The Pervin spaces are transitive, that is, they have a basis of transitive entourages. In addition, they are totally bounded: for every entourage $U$, there exists a finite cover $\fancyscript{C}$ of the space $X$ such that $C\times C \subseteq U$ for each $C \in \fancyscript{C}$. It may also be shown that the Pervin spaces (as we define them here) are exactly the transitive and totally bounded quasi-uniform spaces. It is not hard to see that if $\fancyscript{M}\subseteq \fancyscript{P}(X)$ and $\fancyscript{L}\subseteq \fancyscript{P}(Y)$ are lattices of sets, then a map $f\text {:}\,(X,\fancyscript{U}_{\fancyscript{M}})\rightarrow (Y,\fancyscript{U}_{\fancyscript{L}})$ is uniformly continuous if and only if $f^{-1}$ induces a lattice homomorphism from $\fancyscript{L}$ to $\fancyscript{M}$ by restriction. Thus, the category of lattices of sets with morphisms that are commuting diagrams

where $\phi$ is a complete lattice homomorphism, is dually equivalent to the category of Pervin spaces with uniformly continuous maps.

Now we are ready to state the main result of Sect. 1 of [19]: The set representation of a lattice $D$ given by Stone/Priestley duality is obtainable from any set representation $e\text {:}\,D\hookrightarrow \fancyscript{P}(X)$ by taking the so-called bicompletion of the corresponding quasi-uniform Pervin space $(X,\fancyscript{U}_{Im(e)})$.

To be more precise, we have:

Theorem 8. [19, Theorem 1.6] Let $D$ be a bounded distributive lattice, and let $e\text {:}\,D\hookrightarrow \fancyscript{P}(X)$ be any embedding of $D$ in a power set lattice and denote by $\fancyscript{L}$ the image of the embedding $e$. Let $\,\widetilde{X}$ be the bicompletion of the Pervin space $\,(X,\fancyscript{U}_{\fancyscript{L}})$. Then $\widetilde{X}$ with the induced topology is the dual space of $D$.

We give a few details on this theorem. For more details on bicompleteness see [16, Chap. 3]. The theory of completions of uniform spaces is well-understood, see e.g. [6, Chap. II.3]. However, for quasi-uniform spaces, the situation is much more delicate. Two of the most accepted and well behaved completions, namely the bicompletion [16] (which is equivalent to the pair completion and the strong completion) and the $D$-completion [10], actually agree for Pervin spaces. The bicompletion is particularly appropriate to the representation theory of distributive lattices since it relates the representations of the lattice, its order dual, and its booleanisation. In addition, the bicompletion is the simplest, as it mainly reduces to the completion theory of uniform spaces.

Let $(X,\fancyscript{U})$ be a quasi-uniform space. The converse, $\fancyscript{U}^{-1}$, of the quasi-uniformity $\fancyscript{U}$, consisting of the converses $U^{-1}$ of the entourages $U\in \fancyscript{U}$, is again a quasi-uniformity on $X$. Further, the symmetrisation $\fancyscript{U}^s$, which is the filter generated by the union of $\fancyscript{U}$ and $\fancyscript{U}^{-1}$, is a uniformity on $X$. It is easy to verify that if $(X,\fancyscript{U}_{\fancyscript{L}})$ is a Pervin space, then $(X,\fancyscript{U}_{\fancyscript{L}}^{-1})$ is the Pervin space corresponding to the order dual of $\fancyscript{L}$ as embedded in $\fancyscript{P}(X)$ via $\fancyscript{L}^\partial \hookrightarrow \fancyscript{P}(X)$ obtained by taking complements in $\fancyscript{P}(X)$. Also $(X,\fancyscript{U}_{\fancyscript{L}}^s)$ is the uniform Pervin space corresponding to the representation ${\fancyscript{L}}^-\hookrightarrow \fancyscript{P}(X)$ of the booleanisation ${\fancyscript{L}}^-$ of ${\fancyscript{L}}$.

Now, a quasi-uniform space $(X,\fancyscript{U})$ is bicomplete if and only if $(X,\fancyscript{U}^s)$ is a complete uniform space. It has been shown by Fletcher and Lindgren that the full category of bicomplete quasi-uniform spaces forms a reflective subcategory of the category of quasi-uniform spaces with uniformly continuous maps, and thus, for each quasi-uniform space $(X,\fancyscript{U})$, there is a bicomplete quasi-uniform space $(\widetilde{X},\widetilde{\fancyscript{U}})$ and a uniformly continuous map $\eta _X\text {:}\,(X,\fancyscript{U})\rightarrow (\widetilde{X},\widetilde{\fancyscript{U}})$ with a universal property:

Theorem 9. [16, Chap. 3.3], Let $(X,\fancyscript{U})$ be a quasi-uniform space, $(Y,\fancyscript{V})$ a bicomplete quasi-uniform space and let $f \text {:}\, X\rightarrow Y$ be a $(\fancyscript{U},\fancyscript{V})$ -uniformly continuous function. Then there exists a unique $\widetilde{f}\text {:}\,\widetilde{X}\rightarrow Y$ which is $(\widetilde{\fancyscript{U}},\fancyscript{V})$ -uniformly continuous such that $f=\widetilde{f}\circ \eta _X$.

The bicompletion of a quasi-uniform space $(X,\fancyscript{U})$ is closely related to that of its symmetrisation in that the symmetrisation of the bicompletion is equal to the (bi)completion of the symmetrisation. In the case of a quasi-uniform Pervin space $(X,\fancyscript{U}_{\fancyscript{L}})$ the symmetrisation is the uniform Pervin space $(X,\fancyscript{U}_{{\fancyscript{L}}^-})$ of the booleanisation ${\fancyscript{L}}^-$ of ${\fancyscript{L}}$. It is not too hard to show that the (uniform=bi) completion of $(X,\fancyscript{U}_{{\fancyscript{L}}^-})$ is the Boolean space dual to ${\fancyscript{L}}^-$ given as a uniform space. That is, $\widetilde{X}=X_{{\fancyscript{L}}^-}$ is the set of ultrafilters of ${\fancyscript{L}}^-$ (or equivalently the set of prime filters of ${\fancyscript{L}}$), and the uniformity corresponding to ${\fancyscript{L}}^-$ is generated by the sets $U_B=(B^c\times \widetilde{X})\cup (\widetilde{X}\times B)$ for $B\subseteq \widetilde{X}$ clopen (in the topology for ${\fancyscript{L}}^-$, or equivalently, in the Priestley topology for ${\fancyscript{L}}$). This is the unique uniformity inducing the Boolean topology on $\widetilde{X}$ since this space is compact Hausdorff, see [6, Chapter II.4, Theorem 1]. Thus this uniform space carries no more information than that of the topological dual space of ${\fancyscript{L}}^-$.

The function $\eta _X\text {:}\,X\rightarrow \widetilde{X}$ underlying the embedding of $(X,\fancyscript{U}_{{\fancyscript{L}}^-})$ in $(\widetilde{X},\widetilde{\fancyscript{U}}_{{\fancyscript{L}}^-})$ is the map which sends $x\in X$ to the point of $X_{{\fancyscript{L}}^-}$ corresponding to the homomorphism $\chi _x\text {:}\,{\fancyscript{L}}^-\rightarrow 2$ given by $\chi _x(L)=1$ if and only if $x\in L$. Also, the $(\fancyscript{U}_{{\fancyscript{L}}^-},\widetilde{\fancyscript{U}}_{{\fancyscript{L}}^-})$-uniform continuity of this map comes about in a particularly simple way as one can show that $\eta _X^{-1}(U_{\widehat{L}})=U_{L}$ for each $L\in {\fancyscript{L}}^-$.

Now we can formulate, what the bicompletion of $(X,\fancyscript{U}_{\fancyscript{L}})$ is: It is based on the map $\eta _X\text {:}\,X\rightarrow \widetilde{X}$ as given above, but the quasi-uniformity on $\widetilde{X}$ is generated by the sets $U_{\widehat{L}}$ for $L\in {\fancyscript{L}}$ rather than by all the sets $\eta _X(U_{L})$ for $L\in {\fancyscript{L}}^-$. Thus the bicompletion of $(X,\fancyscript{U}_{\fancyscript{L}})$ is the Stone space of $D$ ‘in quasi-uniform form’. Alternatively, one can think of this space as an ordered uniform space and simply equip the Boolean space $(\widetilde{X},\widetilde{\fancyscript{U}}_{{\fancyscript{L}}^-})$ with the order obtained by $\bigcap _{L\in {\fancyscript{L}}}U_{\widehat{L}}$. This is then a uniform version of Priestley duality.

In closing, we record what this theory yields in the setting of finitely freely generated Heyting algebras. We have the following corollary to Theorem 8.

Corollary 3. Let $N$ be a positive natural number, and $A$ the free $N$-generated Heyting algebra. Then the following statements hold:

• 1. The Esakia space $X$ dual to $A$ is homeomorphic to the bicompletion of the quasi-uniform Pervin space $(J(A),\fancyscript{U}_{\fancyscript{L}})$ where $J(A)$ is the set of join prime elements of $A$ and $\fancyscript{L}$ is the lattice of all downsets of finite antichains in $J(A)$.

• 2. The Esakia space $X$ dual to $A$ is homeomorphic to the bicompletion of the quasi-uniform Pervin space $(U,\fancyscript{U}_{\fancyscript{D}})$ where $U$ is the frame underlying the $N$ -universal model of intuitionistic logic and $\fancyscript{D}$ is the lattice of all definable subsets of $U$.