Presenting de Groot duality of stably compact spaces

TL;DR

This paper provides a constructive, point-free approach to de Groot duality in stably compact spaces using strong proximity lattices and introduces strong continuous entailment relations for analyzing duals.

Contribution

It introduces strong continuous entailment relations as a new tool for representing and analyzing de Groot duals of stably compact spaces.

Findings

De Groot duals can be identified via duals of presentations.

Constructs powerlocales, patch topology, and valuation spaces.

Approach simplifies reasoning about duality in stably compact spaces.

Abstract

We give a constructive account of the de Groot duality of stably compact spaces in the setting of strong proximity lattice, a point-free representation of a stably compact space. To this end, we introduce a notion of strong continuous entailment relation, which can be thought of as a presentation of a strong proximity lattice by generators and relations. The new notion allows us to identify de Groot duals of stably compact spaces by analysing the duals of their presentations. We carry out a number of constructions on strong proximity lattices using strong continuous entailment relations and study their de Groot duals. The examples include various powerlocales, patch topology, and the space of valuations. These examples illustrate the simplicity of our approach by which we can reason about the de Groot duality of stably compact spaces.

Equations

$$\top$$

$$0$$

$$1$$

$$I=\underset{a\in I}{\bigvee }\downarrow a.$$

$$f_r(b)\stackrel{\text{def}}{=}{r}^{-}b.$$

$$f(I)\stackrel{\text{def}}{=}\underset{b\in I}{\bigvee }{f}_r(b)=r^{-}I.$$

$$0$$

$${\varnothing }^{\ast }$$

$$As\cdot rC\stackrel{\text{def}}{⟺}\exists \mathcal{V}\in \mathsf{Fin}(\mathsf{Fin}(S^{\prime }))\left[\forall B^{\prime }\in {\mathcal{V}}^{\ast }\left(Ar{B}^{\prime }\right)\&\forall B\in \mathcal{V}\left(BsC\right)\right].$$

$$a⊢a(\mathrm{R})\frac{A⊢B}{A^{\prime },A⊢B,B^{\prime }}(\mathrm{M})\frac{A⊢B,aa,A⊢B}{A⊢B}(\mathrm{T})$$

$$\mathcal{U}\tilde{r}\mathcal{V}\stackrel{\text{def}}{⟺}\forall A\in \mathcal{U}\forall B\in {\mathcal{V}}^{\ast }\left(ArB\right).$$

$$\mathcal{U}{=}_{⊢}\mathcal{V}\stackrel{\text{def}}{⟺}\mathcal{U}\widetilde{⊢}\mathcal{V}\&\mathcal{V}\widetilde{⊢}\mathcal{U}.$$

$$0$$

$$1$$

$$\widetilde{{⊢}^{\prime }}\circ \tilde{r}=\widetilde{{⊢}^{\prime }\cdot r}=\tilde{r}=\widetilde{r\cdot ⊢}=\tilde{r}\circ \widetilde{⊢}$$

$$A\hat{r}B$$

$$A({⊢}^{\prime }\cdot \hat{r})B$$

$$⟺\left\{A\right\}(\widetilde{{⊢}^{\prime }}\circ \tilde{\hat{r}}){\left\{B\right\}}^{\ast }$$

$$⟺\left\{A\right\}(\widetilde{{⊢}^{\prime }}\circ r){\left\{B\right\}}^{\ast }$$

$$⟺\left\{A\right\}r{\left\{B\right\}}^{\ast }$$

$$⟺A\hat{r}B.$$

$$A⊢B\stackrel{\text{def}}{⟺}\bigwedge A\le \bigvee B.$$

$$ar\mathcal{U}$$

$$D(S,0,\vee ,1,\wedge )\stackrel{\text{def}}{=}(S,⊢),$$

$$AD(r)B\stackrel{\text{def}}{⟺}\bigwedge Ar\bigvee B.$$

$$A\between B\stackrel{\text{def}}{⟺}\left(\exists a\in S\right)a\in A\cap B,$$

$$\begin{array}{c}a⊢\perp (\text{if a≺0}),c⊢a\vee b(\text{if c≺a′∨b′,a′≺a,b′≺b}),\\ \top ⊢1,a\wedge b⊢(a\wedge b),a⊢b(\text{if a≤b}),\\ a⊢b(\text{if a≺b}),a⊢\underset{b\prec a}{\bigvee }b.\end{array}$$

$$i_S(a)\stackrel{\text{def}}{=}{\downarrow }_{\prec }a.$$

$$0⊢\perp ,(a\vee b)⊢a\vee b,\top ⊢1,a\wedge b⊢(a\wedge b),a⊢b(\text{if a≤b}),$$

$$a⊢b(\text{if a≺b}),a⊢\underset{b\prec a}{\bigvee }b.$$

$$A{\le }^{\vee }B$$

$$A{\prec }_{L}B$$

$$0^{\vee }$$

$$1^{\vee }$$

$$A{\prec }^{\vee }B\stackrel{\text{def}}{⟺}\exists C{\prec }_{L}B\left(A{\le }^{\vee }C\right).$$

Full text

Keywords: stably compact space; de Groot duality; strong proximity lattice; entailment relation; locale

MSC2010: 06B35; 06D22; 03B70; 03F60

1 Introduction

De Groot duality of stably compact spaces induces a family of dualities on various powerdomain constructions. In the point-free setting, Vickers [24] showed that the de Groot dual of the upper powerlocale of a stably compact locale is the lower powerlocale of its dual.111Stably compact locales are also known as stably locally compact locales [10, Chapter VII, Section 4.6] or arithmetic lattices [16]. The upper and lower powerlocales of a locale correspond to the Smyth and Hoare powerdomains of the corresponding space, respectively. In the point-set setting, Goubault-Larrecq [8] showed that the dual of the Plotkin powerdomain of a stably compact space is the Plotkin powerdomain of its dual; the same holds for the probabilistic powerdomain.

In this paper, we give an alternative account of these results in the setting of strong proximity lattice [16], the Karoubi envelop of the category of spectral locales and locale maps. Strong proximity lattices have a structural duality which reflects the de Groot duality of stably compact spaces in a simple way (see Section 6). Moreover, a strong proximity lattice is just a distributive lattice with an extra structure, so it does not require infinitary joins inherent in the usual point-free approach. This provides us with a convenient setting to study the de Groot duality of stably compact spaces constructively.

To deal with stably compact spaces presented by generators and relations, we introduce a notion of strong continuous entailment relation, which can be thought of as a presentation of a strong proximity lattice by generators and relations by Scott’s entailment relations [18]. The notion is a variant of that of an entailment relation with the interpolation property due to Coquand and Zhang [4]. Here, the structure due to Coquand and Zhang is strengthened so that it has an intrinsic duality which reflects the de Groot duality of stably compact spaces. The resulting structure, strong continuous entailment relation, allows us to identify de Groot duals of stably compact locales presented by generators and relations by analysing the duals of their presentations. We illustrate the ease with which we can reason about de Groot duality by carrying out a number of constructions on strong proximity lattices using strong continuous entailment relations. The examples include various powerlocales, patch topology, and the space of valuations.

Throughout this paper, we work in the point-free setting, identifying stably compact spaces with their point-free counterparts, stably compact locales. This allows us to work constructively in the predicative sense as manifested in Aczel’s constructive set theory [1]. However, the point of this work is not the constructively but the simplicity of our approach by which we can analyse de Groot duals of various constructions on stably compact spaces.

Related works

Besides the work of Coquand and Zhang [4] and that of Jung and Sünderhauf [16] mentioned above, many authors studied stably compact spaces from the point-free perspective (see Escardó [6]; Jung, Kegelmann, and Moshier [15]; Vickers [24]). Among them, the notion of entailment system by Vickers [24], which develops the idea of Jung et al. [15], is particularly related to the notion of strong continuous entailment relation. These structures are equipped with structural dualities which reflects the de Groot duality of stably compact spaces.

The essential difference between our approach and that of Vickers is the following: the theory of strong continuous entailment relation is built on the fact that stably compact locales are the retracts of spectral locales and locale maps. Hence, the theory of strong continuous entailment relation essentially deals with the objects of the Karoubi envelop of the latter category. On the other hand, the theory of entailment system deals with the objects of the Karoubi envelop of the category of spectral locales and preframe homomorphisms (see Section 4).222More specifically, it suffices to consider only free frames rather than spectral locales. In this view, the former theory treats stably compact locales as locales while the latter theory treats them as preframes; this has to do with the simplicity of the treatment of joins in the geometric presentation of a locale represented by the former structure (see Section 5). Thus, if one is interested in the localic structure of stably compact locales rather than that of preframe, it would be more natural to work with strong continuous entailment relations. In particular, this could potentially facilitate some of the localic constructions on stably compact locales involving finite joins, such as patch topology and the Vietoris powerlocale, in the setting of strong continuous entailment relations, although proper comparison is needed.

Apart from the point-free approaches mentioned above, we are motivated by the corresponding results for stably compact spaces due to Goubault-Larrecq [8]. To derive these results, he used the notion of $\mathbf{A}$-valuation due to Heckmann [9]. It would be interesting to know if there is any connection between our approach and the $\mathbf{A}$-valuation approach. However, since we prefer to work constructively in the point-free setting, we do not compare the two approaches in this paper.

Organisation

In Section 2, we fix some basic notions on locales. In Section 3, we introduce the notion of proximity lattice as the Karoubi envelop of the category of spectral locales and preframe homomorphisms. In Section 4, we give an alternative representation for proximity lattices, called continuous entailment relation, based on the notion of entailment system. In Section 5, we strengthen the notion of proximity lattice to strong proximity lattice by looking into the Karoubi envelop of the category of spectral locales and locale maps. We also introduce the corresponding notion of strong continuous entailment relation. In Section 6, we formulate the duality of proximity lattices and continuous entailment relations, and show that these dualities reflect the de Groot duality of stably compact locales. In Section 7, we study the de Groot duals of various constructions on stably compact locales by exploiting the correspondence between strong proximity lattices and strong continuous entailment relations.

2 Preliminary on locales

A frame is a poset $(X,\wedge,\bigvee)$ with finite meets $\wedge$ and joins $\bigvee$ for all subsets of $X$ where finite meets distribute over all joins. A homomorphism from a frame $X$ to a frame $Y$ is a function $f\colon X\to Y$ which preserves finite meets and all joins. The category of locales is the opposite of the category of frames and frame homomorphisms. We write ${\mathrm{\Omega}(X})$ for the frame corresponding to a locale $X$, but we often regard a frame as a locale and vice versa without change of notation.

Given a set $S$ of generators, a geometric theory over $S$ is a set of axioms of the form $\operatorname*{{\textstyle{\bigwedge}}}A\mathrel{\vdash}\bigvee_{i\in I}\operatorname*{{\textstyle{\bigwedge}}}B_{i},$ where $A$ is a finite subset of $S$ and $(B_{i})_{i\in I}$ is a set-indexed family of finite subsets of $S$.333Here, finite means finitely enumerable. A set $A$ is finitely enumerable if there is a surjective function $f:\left\{0,\dots,n-1\right\}\to A$ for some natural number $n$. Finitely enumerable sets are also known as Kuratowski finite sets; see e.g., Johnstone [12, D5.4]. Single conjunctions and single disjunctions are identified with elements of $S$. We use the following abbreviations:

[TABLE]

An interpretation of a geometric theory $T$ (over $S$) in a locale $X$ is a function $f\colon S\to{\mathrm{\Omega}(X})$ such that $\operatorname*{{\textstyle{\bigwedge}}}_{a\in A}f(a)\leq_{X}\bigvee_{i\in I}\operatorname*{{\textstyle{\bigwedge}}}_{b\in B_{i}}f(b)$ for each axiom $\operatorname*{{\textstyle{\bigwedge}}}A\mathrel{\vdash}\bigvee_{i\in I}\operatorname*{{\textstyle{\bigwedge}}}B_{i}$ of $T$. There is a locale $\mathrm{Sp}(T)$ with a universal interpretation $i_{T}\colon S\to{\mathrm{\Omega}(\mathrm{Sp}(T)})$: for any interpretation $f\colon S\to{\mathrm{\Omega}(X})$ of $T$, there exists a unique frame homomorphism $\overline{f}\colon{\mathrm{\Omega}(\mathrm{Sp}(T)})\to{\mathrm{\Omega}(X})$ such that $\overline{f}\circ i_{T}=f$. In this case, $\mathrm{Sp}(T)$ is called the locale (or frame) presented by $T$. A model of a geometric theory $T$ over $S$ is a subset $\alpha\subseteq S$ such that $A\subseteq\alpha\;\rightarrow\>\exists i\in I\left(B_{i}\subseteq\alpha\right)$ for each axiom $\operatorname*{{\textstyle{\bigwedge}}}A\mathrel{\vdash}\bigvee_{i\in I}\operatorname*{{\textstyle{\bigwedge}}}B_{i}$ of $T$. If the models of $T$ form a distinguished class of objects, we call $\mathrm{Sp}(T)$ the locale whose models are members of that class.444 We differ from the standard distinction between “interpretation” and “model” wherein the former interprets the language (here generators) and the latter in addition satisfies the axioms of the theory over the language. In this paper, in contrast, both “interpretation” and “model” mean an interpretation which satisfies the axioms: the latter keeps the usual meaning of a model in the lattice of truth values, the powerset of a singleton $\left\{*\right\}$, whereas the former means an axiom preserving interpretation in a frame more general than that of the truth values. In locale theory, this can be expressed as the distinction between generalised points and global points (see Vickers [23]).

3 Proximity lattices

We recall the construction of Karoubi envelop (cf. [7, Chapter 2, Exercise B]).

Definition 3.1**.**

An idempotent in a category $\mathbb{C}$ is a morphism $f\colon A\to A$ such that $f\circ f=f$. The Karoubi envelop (or splitting of idempotents) of $\mathbb{C}$ is a category $\mathsf{\mathbf{Split}(\mathbb{C})}$ where objects are idempotents in $\mathbb{C}$ and morphisms $h\colon(f\colon A\to A)\to(g\colon B\to B)$ are morphisms $h\colon A\to B$ in $\mathbb{C}$ such that $g\circ h=h=h\circ f$.

One can show that if $\mathbb{C}$ is a full subcategory of $\mathbb{D}$ where every idempotent splits in $\mathbb{D}$ and every object in $\mathbb{D}$ is a retract of an object of $\mathbb{C}$, then $\mathbb{D}$ is equivalent to $\mathsf{\mathbf{Split}(\mathbb{C})}$.

It is well known that stably compact locales are exactly the retracts of spectral locales, whose frames are the ideal completions of distributive lattices [10, Chapter VII, Theorem 4.6]. Less well known is the fact that stably compact locales are exactly the preframe retracts of spectral locales [24, Section 3]555 To be precise, the results of Vickers [24] are stronger; the stably compact locales are preframe retracts of free frames (cf. footnote 2). so that the category of stably compact locales and preframe homomorphisms can be characterised as the Karoubi envelop of the category of spectral locales and preframe homomorphisms. Here, a preframe is a poset with directed joins (joins of directed subsets) and finite meets which distribute over directed joins. A preframe homomorphism between preframes is a function which preserves finite meets and directed joins. The latter fact leads to the notion of proximity lattice [16] by considering a finitary description of the dual of the category of spectral locales and preframe homomorphisms.

Definition 3.2**.**

Let $S$ and $S^{\prime}$ be distributive lattices. A proximity relation from $S$ to $S^{\prime}$ is a relation $r\subseteq S\times S^{\prime}$ such that

1. (ProxI)

$r^{-}b\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\left\{a\in S\mid a\mathrel{r}b\right\}$ is an ideal of $S$ for all $b\in S^{\prime}$, 2. (ProxF)

$ra\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\left\{b\in S^{\prime}\mid a\mathrel{r}b\right\}$ is a filter of $S^{\prime}$ for all $a\in S$.

Here, an ideal is a downward closed subset of $S$ closed under finite joints. A filter is an upward closed subset of $S$ closed under finite meets.

Let $\mathsf{DLat_{Prox}}$ be the category of distributive lattices and proximity relations: the identity on a distributive lattice $S$ is the order $\leq$ on $S$; the composition of proximity relations is the relational composition.

The ideal completion of a distributive lattice $S$, denoted by $\mathrm{Idl}(S)$, is the frame of ideals of $S$: the directed join of ideals is their union; finite joins and finite meets are defined by

[TABLE]

where $\mathord{\downarrow}a\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\left\{b\in S\mid b\leq a\right\},$ the principal ideal generated by $a$. Every ideal $I$ is a directed join of principal ideals:

[TABLE]

Proposition 3.3**.**

For any proximity relation $r\colon S\to S^{\prime}$, there exists a unique preframe homomorphism $f\colon\mathrm{Idl}(S^{\prime})\to\mathrm{Idl}(S)$ such that $f(\mathord{\downarrow}b)=r^{-}b$ for all $b\in S^{\prime}$. Moreover, this bijection preserves identities and compositions of proximity relations.

Proof.

It is easy to see that a proximity relation $r\colon S\to S^{\prime}$ uniquely extends to a meet-semilattice homomorphism $f_{r}\colon S^{\prime}\to\mathrm{Idl}(S)$ defined by

[TABLE]

By Vickers [20, Theorem 9.1.5 (i) (iv)], the function $f_{r}$ extends uniquely to a preframe homomorphism $f\colon\mathrm{Idl}(S^{\prime})\to\mathrm{Idl}(S)$ by

[TABLE]

The second statement follows from the first and (3.1). ∎

Let $\mathsf{Spectral_{Pre}}$ be the category of spectral locales and preframe homomorphisms: objects of $\mathsf{Spectral_{Pre}}$ are distributive lattices and morphisms are preframe homomorphisms between the ideal completions.

Theorem 3.4**.**

The category $\mathsf{DLat_{Prox}}$ is dually equivalent to $\mathsf{Spectral_{Pre}}$.

Proof.

Immediate from Proposition 3.3. ∎

Since $\mathsf{\mathbf{Split}(\mathsf{Spectral_{Pre}})}$ is equivalent to the category of stably compact locales and preframe homomorphisms, $\mathsf{\mathbf{Split}(\mathsf{DLat_{Prox}})}$ is dually equivalent to the latter category. The objects and morphisms of $\mathsf{\mathbf{Split}(\mathsf{DLat_{Prox}})}$ are called proximity lattices and proximity relations respectively (cf. Jung and Sünderhauf [16] and de Gool [19]). In what follows, we write $\mathsf{ProxLat}$ for $\mathsf{\mathbf{Split}(\mathsf{DLat_{Prox}})}$.

Notation 3.5*.*

We write $(S,\prec)$ for a proximity lattice, where $S$ is a distributive lattice and $\prec$ is an idempotent proximity relation on $S$. We write $r\colon(S,\prec)\to(S^{\prime},\prec^{\prime})$ for a proximity relation from $(S,\prec)$ to $(S^{\prime},\prec^{\prime})$, i.e., a proximity relation $r\colon S\to S^{\prime}$ between the underlying distributive lattices such that ${\prec^{\prime}}\circ r=r\circ{\prec}=r$.

Each proximity lattice $(S,\prec)$ represents a stably compact locale whose frame is the collection $\mathrm{RIdl}(S)$ of rounded ideals of $S$ ordered by inclusion [16, Theorem 11]. Here, an ideal $I\subseteq S$ is rounded if $a\in I\leftrightarrow\exists b\succ a\left(b\in I\right)$.666The notion of rounded ideal makes sense in the more general setting of information systems [21]. Directed joins and finite meets in $\mathrm{RIdl}(S)$ are calculated as in $\mathrm{Idl}(S)$; on the other hand, finite joins in $\mathrm{RIdl}(S)$ are defined by

[TABLE]

where $\mathord{\downarrow}_{\prec}a\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\left\{b\in S\mid b\prec a\right\}$. Every rounded ideal $I$ is a directed join of its members: $I=\bigvee_{a\in I}\mathord{\downarrow}_{\prec}a$. Let $\mathrm{Spec}(S)$ denote the locale whose frame is $\mathrm{RIdl}(S)$.

4 Continuous entailment relations

We give an alternative presentation of a proximity lattice in terms of Vickers’s entailment system [24]. We need some constructions on finite subsets. For any set $S$, let $\mathsf{Fin}(S)$ denote the set of finite subsets of $S$. For each $\mathcal{U}\in\mathsf{Fin}(\mathsf{Fin}(S))$, define $\mathcal{U}^{*}\in\mathsf{Fin}(\mathsf{Fin}(S))$ inductively by

[TABLE]

where $\mathsf{Fin}^{+}(A)$ denotes the set of inhabited finite subsets of $A$.777 In the notation of Vickers [24, Section 4], the set $\mathcal{U}^{*}$ is equal to $\left\{\mathrm{Im}\,\gamma\mid\gamma\in\mathrm{Ch}(\mathcal{U})\right\},$ where $\mathrm{Ch}(\mathcal{U})$ is the set of choices of $\mathcal{U}$ and $\mathrm{Im}\,\gamma$ is the image of a choice $\gamma$; see Definition 12 and Definition 13, and the proof of Proposition 14 in [24]. Writing $\mathrm{DL}(S)$ for the free distributive lattice over $S$, the mapping $\mathcal{U}\mapsto\mathcal{U}^{*}$ transforms a disjunction of conjunctions of generators in $\mathrm{DL}(S)$ to the conjunction of disjunctions of generators, or the other way around (cf. Vickers [23, Theorem 8.7]).

Definition 4.1**.**

Let $S,S^{\prime},S^{\prime\prime}$ be sets and $r,s$ be relations $r\subseteq\mathsf{Fin}(S)\times\mathsf{Fin}(S^{\prime})$ and $s\subseteq\mathsf{Fin}(S^{\prime})\times\mathsf{Fin}(S^{\prime\prime})$.

The relation $r$ is said to be upper if $A\mathrel{r}B\;\rightarrow\>A\cup A^{\prime}\mathrel{r}B\cup B^{\prime}$ for all $A,A^{\prime}\in\mathsf{Fin}(S)$ and $B,B^{\prime}\in\mathsf{Fin}(S^{\prime})$. 2. 2.

The cut composition $s\cdot r\subseteq\mathsf{Fin}(S)\times\mathsf{Fin}(S^{\prime\prime})$ is defined by

[TABLE]

Definition 4.2** (Vickers [24, Section 6]).**

An entailment system is a pair $(S,\ll)$ where $S$ is a set and $\ll$ is an upper relation on $\mathsf{Fin}(S)$ such that $\ll\cdot\ll{=}\ll$. A Karoubi morphism $r\colon(S,\ll)\to(S^{\prime},\ll^{\prime})$ of entailment systems is an upper relation $r\subseteq\mathsf{Fin}(S)\times\mathsf{Fin}(S^{\prime})$ such that $\ll^{\prime}\mathop{\cdot}r=r=r\mathop{\cdot}\ll\!.$

Let $\mathsf{Entsys}$ be the category of entailment systems and Karoubi morphisms between them: the identity on $(S,\ll)$ is $\ll$ and the composition of morphisms is the cut composition; see Vickers [24, Section 5 and Section 6] for the details. As shown in [24], $\mathsf{Entsys}$ is dually equivalent to the category of stably compact locales and preframe homomorphisms. An entailment system $(S,\ll)$ represents a stably compact locale (or frame) which is a preframe retract of the free frame over $S$, or equivalently, the spectral locale determined by the free distributive lattice over $S$. The relation $\ll$ then represents the retraction.

We now focus on the full subcategory of $\mathsf{Entsys}$ consisting of reflexive entailment systems [24, Section 6.1], also known as entailment relations [18, 2].

Definition 4.3**.**

An entailment relation on a set $S$ is a relation $\mathrel{\vdash}$ on $\mathsf{Fin}(S)$ such that

[TABLE]

for all $a\in S$ and $A,A^{\prime},B,B^{\prime}\in\mathsf{Fin}(S)$, where “$a$” denotes $\left\{a\right\}$ and “,” denotes the union.

Each entailment relation $(S,\mathrel{\vdash})$ is an entailment system; we write $\mathsf{EntRel}$ for the full subcategory of $\mathsf{Entsys}$ consisting of entailment relations. As noted by Vickers [24, Section 6.1], the category $\mathsf{EntRel}$ is dually equivalent to $\mathsf{Spectral_{Pre}}$. Hence $\mathsf{EntRel}$ is equivalent to $\mathsf{DLat_{Prox}}$, which we now elaborate.

Definition 4.4**.**

Let $S,S^{\prime}$ be sets and $r$ be a relation $r\subseteq\mathsf{Fin}(S)\times\mathsf{Fin}(S^{\prime})$. Define a relation ${\mathrel{\widetilde{r}}}\subseteq\mathsf{Fin}(\mathsf{Fin}(S))\times\mathsf{Fin}(\mathsf{Fin}(S^{\prime}))$ by

[TABLE]

Lemma 4.5**.**

Let $S,S^{\prime},S^{\prime\prime}$ be sets and $r,s$ be upper relations $r\subseteq\mathsf{Fin}(S)\times\mathsf{Fin}(S^{\prime})$ and $s\subseteq\mathsf{Fin}(S^{\prime})\times\mathsf{Fin}(S^{\prime\prime})$. Then $\mathrel{\widetilde{s\cdot r}}{=}\mathrel{\widetilde{s}}\circ\mathrel{\widetilde{r}}.$

Proof.

See Vickers [24, Proposition 22 and Proposition 31]. ∎

An entailment relation $(S,\mathrel{\vdash})$ determines a distributive lattice $\mathrm{DL}(S,\mathrel{\vdash})$ whose underlying set is $\mathsf{Fin}(\mathsf{Fin}(S))$ equipped with an equality defined by

[TABLE]

The lattice structure is defined as follows:

[TABLE]

It is easy to check that joins and meets are well-defined with respect to $=_{\mathrel{\vdash}}$ and that the order determined by $\mathrm{DL}(S,\mathrel{\vdash})$ is $\mathrel{\widetilde{\mathrel{\vdash}}}$.

If $r\colon(S,\mathrel{\vdash})\to(S^{\prime},\mathrel{\vdash}^{\prime})$ is a Karoubi morphism, then

[TABLE]

by Lemma 4.5. Then, it easy to see that $\mathrel{\widetilde{r}}$ is a proximity relation from $\mathrm{DL}(S,\mathrel{\vdash})$ to $\mathrm{DL}(S^{\prime},\mathrel{\vdash}^{\prime})$.

Proposition 4.6**.**

The assignment $r\mapsto{\mathrel{\widetilde{r}}}$ determines a functor $E\colon\mathsf{EntRel}\to\mathsf{DLat_{Prox}}$, which establishes equivalence of $\mathsf{EntRel}$ and $\mathsf{DLat_{Prox}}$.

Proof.

Functoriality of $E$ follows from the construction of $\mathrm{DL}(S,\mathrel{\vdash})$ and Lemma 4.5. Moreover, $E$ is faithful because $A\mathrel{r}B\leftrightarrow\left\{A\right\}\mathrel{\mathrel{\widetilde{r}}}\left\{B\right\}^{*}$. To see that $E$ is full, for any proximity relation $r\colon\mathrm{DL}(S,\mathrel{\vdash})\to\mathrm{DL}(S^{\prime},\mathrel{\vdash}^{\prime})$, define $\hat{r}\subseteq\mathsf{Fin}(S)\times\mathsf{Fin}(S^{\prime})$ by

[TABLE]

Similarly $\hat{r}\cdot{\mathrel{\vdash}}=\hat{r}$, so $\hat{r}$ is a Karoubi morphism. Thus $E$ is full. To see that $E$ is essentially surjective, for any distributive lattice $(S,0,\vee,1,\wedge)$, define an entailment relation $(S,\mathrel{\vdash})$ by

[TABLE]

Then, define relations $r\subseteq S\times\mathsf{Fin}(\mathsf{Fin}(S))$ and $s\subseteq\mathsf{Fin}(\mathsf{Fin}(S))\times S$ by

[TABLE]

It is straightforward to show that $r$ and $s$ are proximity relations between $S$ and $\mathrm{DL}(S,\mathrel{\vdash})$ and inverse to each other. ∎

Remark 4.7*.*

By the standard construction (Mac Lane [17, Chapter IV, Section 4, Theorem 1]), we can define a quasi-inverse $D\colon\mathsf{DLat_{Prox}}\to\mathsf{EntRel}$ of $E\colon\mathsf{EntRel}\to\mathsf{DLat_{Prox}}$ by

[TABLE]

where $\mathrel{\vdash}$ is defined by (4.1). The functor $D$ sends a proximity relation $r\colon S\to S^{\prime}$ to a Karoubi morphism $D(r)\colon D(S)\to D(S^{\prime})$ defined by

[TABLE]

By Proposition 4.6, the category $\mathsf{\mathbf{Split}(EntRel)}$ is equivalent to $\mathsf{ProxLat}$, and hence dually equivalent to the category of stably compact locales and preframe homomorphisms. Unfolding the definition of $\mathsf{\mathbf{Split}(\mathsf{EntRel})}$, we have the following characterisations of its objects and morphisms (Definition 4.8 and 4.9).

Definition 4.8**.**

A continuous entailment relation is an entailment relation $(S,\mathrel{\vdash})$ equipped with an idempotent Karoubi endomorphism $\ll\mathop{\subseteq}\mathsf{Fin}(S)\times\mathsf{Fin}(S)$ on $(S,\mathrel{\vdash})$. We write $(S,\mathrel{\vdash},\ll)$ for a continuous entailment relation.

Note that each continuous entailment relation $(S,\mathrel{\vdash},\ll)$ has an associated entailment system $(S,\ll)$.

Definition 4.9**.**

Let $(S,\mathrel{\vdash},\ll)$ and $(S^{\prime},\mathrel{\vdash}^{\prime},\ll^{\prime})$ be continuous entailment relations. A proximity map from $(S,\mathrel{\vdash},\ll)$ to $(S^{\prime},\mathrel{\vdash}^{\prime},\ll^{\prime})$ is a Karoubi morphism between entailment systems $(S,\ll)$ and $(S^{\prime},\ll^{\prime})$.

In the following, we write $\mathsf{ContEnt}$ for $\mathsf{\mathbf{Split}(\mathsf{EntRel})}$. Since an entailment system $(S,\ll)$ can be identified with a continuous entailment relation $(S,\between,\ll)$ where

[TABLE]

the category $\mathsf{Entsys}$ can be regarded as a full subcategory of $\mathsf{ContEnt}$. On the other hand, each continuous entailment relation $(S,\mathrel{\vdash},\ll)$ is isomorphic to $(S,\between,\ll)$ with $\ll$ being the isomorphism. Thus, we have the following.

Proposition 4.10**.**

The categories $\mathsf{ContEnt}$ and $\mathsf{Entsys}$ are equivalent. ∎

5 Strong proximity lattices

Proximity lattices and continuous entailment relations have nice structural duality, which will be elaborated in Section 6. However, stably compact locales represented by these structures do not seem to admit simple geometric presentations. In the case of a proximity lattice $(S,\prec)$, for example, $\mathrm{Spec}(S)$ can be presented by a geometric theory over $S$ with the following axioms:

[TABLE]

In the case of continuous entailment relations (or entailment systems), the presentations of the locales represented by these structures are more elaborate; see Vickers [24, Corollary 44]. To obtain a simpler presentation of $\mathrm{Spec}(S)$, we strengthen the notion of proximity lattice to strong proximity lattice [16], which can be obtained from the well-known fact that stably compact locales are the retracts of the spectral locales.

5.1 Strong proximity lattices

We start from a finitary description of locale maps between spectral locales.

Definition 5.1**.**

Let $S$ and $S^{\prime}$ be distributive lattices. A proximity relation $r\colon S\to S^{\prime}$ is said to be join-preserving if

1. (Prox[math])

$a\mathrel{r}0^{\prime}\;\rightarrow\>a=0$, 2. (Prox$\vee$)

$a\mathrel{r}(b\vee^{\prime}c)\;\rightarrow\>\exists b^{\prime},c^{\prime}\in S\left(a\leq b^{\prime}\vee c^{\prime}\>\&\>b^{\prime}\mathrel{r}b\>\&\>c^{\prime}\mathrel{r}c\right)$.

Proposition 3.3 restricts to join-preserving proximity relations and frame homomorphisms.

Proposition 5.2**.**

For any join-preserving proximity relation $r\colon S\to S^{\prime}$ between distributive lattices, there exists a unique frame homomorphism $f\colon\mathrm{Idl}(S^{\prime})\to\mathrm{Idl}(S)$ such that $f(\mathord{\downarrow}b)=r^{-}b$ for all $b\in S^{\prime}$.

Proof.

The proof is similar to Proposition 3.3. One only has to note that a join-preserving proximity relation $r\colon S\to S^{\prime}$ uniquely extends to a lattice homomorphism $f_{r}\colon S^{\prime}\to\mathrm{Idl}(S)$ defined as (3.2). The desired conclusion then follows from Vickers [20, Theorem 9.1.5 (iii) (iv)]. ∎

Let $\mathsf{DLat_{JProx}}$ be the subcategory of $\mathsf{DLat_{Prox}}$ where morphisms are join-preserving proximity relations. Let $\mathsf{Spectral}$ be the category of spectral locales and locale maps. The following is immediate from Proposition 5.2.

Theorem 5.3**.**

The category $\mathsf{DLat_{JProx}}$ is equivalent to $\mathsf{Spectral}$. ∎

Since $\mathsf{\mathbf{Split}(\mathsf{Spectral})}$ is equivalent to the category of stably compact locales and locale maps, $\mathsf{\mathbf{Split}(\mathsf{DLat_{JProx}})}$ is equivalent to the latter category. The objects and morphisms of $\mathsf{\mathbf{Split}(\mathsf{DLat_{JProx}})}$ are called $\vee$-strong proximity lattices and joint-preserving proximity relations respectively (cf. van Gool [19, Definition 1.2 and Definition 1.9]). We write $\mathsf{JSProxLat}$ for $\mathsf{\mathbf{Split}(\mathsf{DLat_{JProx}})}$ and adopt the similar notation as in Notation 3.5 for $\vee$-strong proximity lattices and join-preserving proximity relations between them.

As in the case of proximity lattices, each $\vee$-strong proximity lattice $(S,\prec)$ represents a stably compact locale by the collection $\mathrm{RIdl}(S)$ of rounded ideals. In this case, the locale $\mathrm{Spec}(S)$ can be presented by a simpler geometric theory than (5.1), as we now show.

Let $X$ and $Y$ be locales. A function $f\colon{\mathrm{\Omega}(X})\to{\mathrm{\Omega}(Y})$ is Scott continuous if it preserves directed joins. A Scott continuous function is a suplattice homomorphism if it preserves finite joins (and hence all joins).

Definition 5.4**.**

Let $(S,\prec)$ be a $\vee$-strong proximity lattice and $X$ be a locale. A dcpo interpretation of $(S,\prec)$ in $X$ is an order preserving function $f\colon S\to{\mathrm{\Omega}(X})$ such that $f(a)=\bigvee_{b\prec a}f(b).$ A dcpo interpretation $f\colon S\to{\mathrm{\Omega}(X})$ is called a suplattice (preframe) interpretation if it preserves finite joins (resp. finite meets); $f$ is called an interpretation if it preserves both finite joins and finite meets.

Any $\vee$-strong proximity lattice $(S,\prec)$ admits an interpretation $i_{S}\colon S\to\mathrm{RIdl}(S)$ defined by

[TABLE]

Proposition 5.5**.**

Let $(S,\prec)$ be a $\vee$-strong proximity lattice and $X$ be a locale. For any (dcpo, suplattice, preframe) interpretation $f\colon S\to{\mathrm{\Omega}(X})$, there exists a unique frame homomorphism (resp. Scott continuous function, suplattice homomorphism, preframe homomorphism) $\overline{f}\colon\mathrm{RIdl}(S)\to{\mathrm{\Omega}(X})$ such that $\overline{f}\circ i_{S}=f$.

Proof.

See Vickers [20, Theorem 9.1.5] where an analogous fact for spectral locales is presented. The unique extension of $f$ is defined by $\overline{f}(I)\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\bigvee_{a\in I}f(a)$. Since $f$ is a dcpo interpretation, we have $\overline{f}\circ i_{S}=f$. ∎

Remark 5.6*.*

For dcpo and preframe interpretations, Proposition 5.5 holds for proximity lattices as well. In this case, however, the function $i_{S}\colon S\to\mathrm{RIdl}(S)$ does not necessarily preserve finite joins, so it is only a preframe interpretation.

Corollary 5.7**.**

For any $\vee$-strong proximity lattice $(S,\prec)$, the locale $\mathrm{Spec}(S)$ is presented by a geometric theory over $S$ with the following axioms:101010The left part of axiom $(a\vee b)\mathrel{\vdash}a\vee b$ denotes the generator $a\vee b$, while the right part is the disjunction of two generators $a$ and $b$. The similar remark applies to $a\wedge b\mathrel{\vdash}(a\wedge b)$.

[TABLE]

Proof.

Immediate from the frame version of Proposition 5.5. ∎

Note that models of the geometric theory in Corollary 5.7 are rounded prime filters of $(S,\prec)$, i.e., those prime filters $F$ on $S$ such that $a\in F\leftrightarrow\exists b\prec a\left(b\in F\right)$.

Let $\mathsf{JSProxLat_{Prox}}$ be the full subcategory of $\mathsf{ProxLat}$ consisting of $\vee$-strong proximity lattices.

Theorem 5.8**.**

The category $\mathsf{JSProxLat_{Prox}}$ is equivalent to $\mathsf{ProxLat}$.

Proof.

Given a proximity lattice $(S,\prec)$, define a preorder $\leq^{\vee}$ on $\mathsf{Fin}(S)$ by

[TABLE]

Let $S^{\vee}$ be the set $\mathsf{Fin}(S)$ equipped with the equality $=^{\vee}$ determined by $\leq^{\vee}$, i.e., ${=^{\vee}}\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}{\leq^{\vee}\cap\geq^{\vee}}$, and define a lattice structure $(S^{\vee},0^{\vee},\vee^{\vee},1^{\vee},\wedge^{\vee})$ by

[TABLE]

It is straightforward to check that the above operations respect $=^{\vee}$ and that the lattice is distributive. Next, define a relation $\prec^{\vee}$ on $\mathsf{Fin}(S)$ by

[TABLE]

Again, it is straightforward to check that $\prec^{\vee}$ respects $=^{\vee}$. Since $\prec_{L}$ is idempotent and $\prec$ is a proximity relation, $\prec^{\vee}$ is an idempotent relation. We claim that $(S^{\vee},\prec^{\vee})\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}(S^{\vee},0^{\vee},\vee^{\vee},1^{\vee},\wedge^{\vee},\prec^{\vee})$ is a $\vee$-strong proximity lattice. For example, to see that $(S^{\vee},\prec^{\vee})$ is $\vee$-strong, suppose that $A\prec^{\vee}B\cup C$. Then, there exist $B^{\prime}\prec_{L}B$ and $C^{\prime}\prec_{L}C$ such that $A\leq^{\vee}B^{\prime}\vee^{\vee}C^{\prime}$. Since ${\prec_{L}}\subseteq{\prec^{\vee}}$, we have $B^{\prime}\prec^{\vee}B$ and $C\prec^{\vee}C$. Moreover, $A\prec^{\vee}0^{\vee}$ clearly implies $A\leq^{\vee}0^{\vee}$.

Define relations $r\subseteq S\times\mathsf{Fin}(S)$ and $s\subseteq\mathsf{Fin}(S)\times S$ by

[TABLE]

Then, $r$ and $s$ clearly respect $=^{\vee}$, so they are relations between $S$ and $S^{\vee}$. It is straightforward to show that $r$ and $s$ are proximity relations between $(S,\prec)$ and $(S^{\vee},\prec^{\vee})$ and are inverse to each other. ∎

By introducing $\vee$-strong proximity lattices, we have obtained a simpler geometric theory for $\mathrm{Spec}(S)$ (cf. Corollary 5.7). This, however, comes at the cost of the structural duality of proximity lattices. Nevertheless, the notion of $\vee$-strong proximity lattice is categorically equivalent to the one with a stronger self-dual structure than that of a proximity lattice.

Definition 5.9** (Jung and Sünderhauf [16, Definition 18]).**

A strong proximity lattice is a $\vee$-strong proximity lattice $(S,\prec)$ satisfying

1. (Prox1)

$1\prec a\;\rightarrow\>a=1$, 2. (Prox$\wedge$)

$b\wedge c\prec a\;\rightarrow\>\exists b^{\prime}\succ b\exists c^{\prime}\succ c\left(b^{\prime}\wedge c^{\prime}\leq a\right)$.

Let $\mathsf{SProxLat}$ and $\mathsf{SProxLat_{Prox}}$ be the full subcategories of $\mathsf{JSProxLat}$ and $\mathsf{JSProxLat_{Prox}}$, respectively, consisting of strong proximity lattices. In Section 5.3, we show that $\mathsf{SProxLat}$ and $\mathsf{SProxLat_{Prox}}$ are equivalent to the larger categories.

5.2 Strong continuous entailment relations

We characterise a full subcategory of $\mathsf{ContEnt}$, whose objects correspond to strong proximity lattices. The notion introduced below is a modification of that of entailment relation with the interpolation property by Coquand and Zhang [4], which satisfies only one direction of (5.5).

Definition 5.10**.**

A strong continuous entailment relation is an entailment relation $(S,\mathrel{\vdash})$ equipped with an idempotent relation ${\prec}\subseteq S\times S$ satisfying

[TABLE]

for all $A,B\in\mathsf{Fin}(S)$ where $\prec_{L}$ is defined as (5.3) and $\prec_{U}$ is defined by

[TABLE]

We write $(S,\mathrel{\vdash},\prec)$ for a strong continuous entailment relation.

Each strong continuous entailment relation $(S,\mathrel{\vdash},\prec)$ represents a stably compact locale by a geometric theory $T(S,\mathrel{\vdash},\prec)$ over $S$ with the following axioms:

[TABLE]

Theorem 5.11** (Coquand and Zhang [4]).**

For any strong continuous entailment relation $(S,\mathrel{\vdash},\prec)$, the locale presented by $T(S,\mathrel{\vdash},\prec)$ is stably compact. Moreover, any stably compact locale can be presented in this way.

Proof.

See Coquand and Zhang [4, Theorem 1]. ∎

In the following, we often identify a strong continuous entailment relation ${(S,\mathrel{\vdash},\prec)}$ with the theory $T(S,\mathrel{\vdash},\prec)$.

We relate strong continuous entailment relations to continuous entailment relations.

Lemma 5.12**.**

Let $S,S^{\prime},S^{\prime\prime},S^{\prime\prime\prime}$ be sets and $r,s,t$ be relations $r\subseteq\mathsf{Fin}(S)\times\mathsf{Fin}(S^{\prime})$, $s\subseteq\mathsf{Fin}(S^{\prime})\times\mathsf{Fin}(S^{\prime\prime})$, and $t\subseteq\mathsf{Fin}(S^{\prime\prime})\times\mathsf{Fin}(S^{\prime\prime\prime})$.

If $s$ is upper and $rA=\left\{B\in\mathsf{Fin}(S^{\prime})\mid A\mathrel{r}B\right\}$ is closed under finite joins for each $A\in\mathsf{Fin}(S)$, then $\left(t\cdot s\right)\circ r=t\cdot\left(s\circ r\right).$ 2. 2.

If $s$ is upper and $t^{-}D=\left\{C\in\mathsf{Fin}(S^{\prime\prime})\mid C\mathrel{t}D\right\}$ is closed under finite joins for each $D\in\mathsf{Fin}(S^{\prime\prime\prime})$, then $\left(t\circ s\right)\cdot r=t\circ\left(s\cdot r\right).$

Proof.

1. Suppose that $A\mathrel{t\cdot\left(s\circ r\right)}D$. Then there exists $\mathcal{V}\in\mathsf{Fin}(\mathsf{Fin}(S^{\prime\prime}))$ such that $\forall C^{\prime}\in\mathcal{V}^{*}\left(A\mathrel{s\circ r}C^{\prime}\right)$ and $\forall C\in\mathcal{V}\left(C\mathrel{t}D\right)$, so for each $C^{\prime}\in\mathcal{V}^{*}$ there exists $B_{C^{\prime}}\in\mathsf{Fin}(S^{\prime})$ such that $A\mathrel{r}B_{C^{\prime}}$ and $B_{C^{\prime}}\mathrel{s}C^{\prime}$. Put $B=\bigcup_{C^{\prime}\in\mathcal{V}^{*}}B_{C^{\prime}}$. Then $A\mathrel{r}B$ and $\forall C^{\prime}\in\mathcal{V}^{*}\left(B\mathrel{s}C^{\prime}\right)$, and hence $A\mathrel{\left(t\cdot s\right)\circ r}D$. The converse is easy.

2. The proof is dual of 1. ∎

For each strong continuous entailment relation $(S,\mathrel{\vdash},\prec)$, define a relation $\ll_{\mathrel{\vdash}}$ on $\mathsf{Fin}(S)$ by

[TABLE]

Proposition 5.13**.**

The structure $(S,\mathrel{\vdash},\ll_{\mathrel{\vdash}})$ is a continuous entailment relation.

Proof.

By item 1 of Lemma 5.12, we have

[TABLE]

Similarly ${\ll_{\mathrel{\vdash}}}\cdot{\mathrel{\vdash}}={\ll_{\mathrel{\vdash}}}$ by item 2 of Lemma 5.12. Then

[TABLE]

Hence ${\ll_{\mathrel{\vdash}}}$ is an idempotent Karoubi endomorphism on $(S,\mathrel{\vdash})$. ∎

Let $\mathsf{SContEnt_{Prox}}$ be a category where objects are strong continuous entailment relations and morphisms are proximity maps between the underlying continuous entailment relations. By the assignment $(S,\mathrel{\vdash},\prec)\mapsto(S,\mathrel{\vdash},\ll_{\mathrel{\vdash}})$, we can identify $\mathsf{SContEnt_{Prox}}$ with a full subcategory of $\mathsf{ContEnt}$.

In what follows, we show that $\mathsf{SContEnt_{Prox}}$ and $\mathsf{SProxLat_{Prox}}$ are equivalent. First, note that the functor $E\colon\mathsf{EntRel}\to\mathsf{DLat_{Prox}}$ (cf. Proposition 4.6) induces a functor

[TABLE]

which establishes equivalence of $\mathsf{ContEnt}$ and $\mathsf{ProxLat}$. The functor $F$ sends each continuous entailment relation $(S,\mathrel{\vdash},\ll)$ to a proximity lattice $(\mathrm{DL}(S,\mathrel{\vdash}),\mathrel{\widetilde{\ll}})$ and each proximity map $r$ to a proximity relation $\mathrel{\widetilde{r}}$. By Remark 4.7, $F$ has a quasi-inverse $G\colon\mathsf{ProxLat}\to\mathsf{ContEnt}$ which sends each proximity lattice $(S,\prec)$ to a continuous entailment relation $(S,\mathrel{\vdash},\ll)$, where $\mathrel{\vdash}$ is given by (4.1) and $\ll$ is defined by

[TABLE]

Lemma 5.14**.**

For each strong continuous entailment relation $(S,\mathrel{\vdash},\prec)$, the structure $F(S,\mathrel{\vdash},\ll_{\mathrel{\vdash}})=(\mathrm{DL}(S,\mathrel{\vdash}),\mathrel{\widetilde{\ll_{\mathrel{\vdash}}}})$ is a strong proximity lattice.

Proof.

We must show that $(\mathrm{DL}(S,\mathrel{\vdash}),\mathrel{\widetilde{\ll_{\mathrel{\vdash}}}})$ satisfies (Prox[math]), (Prox$\vee$), (Prox1), and (Prox$\wedge$). As a demonstration, we show (Prox$\vee$). Suppose that $\mathcal{U}\mathrel{\widetilde{\ll_{\mathrel{\vdash}}}}\mathcal{V}\vee\mathcal{W}$. For each $B\in\mathcal{V}^{*}$ and $C\in\mathcal{W}^{*}$, there exist $B^{\prime}\prec_{L}B$ and $C^{\prime}\prec_{L}C$ such that $A\mathrel{\vdash}B^{\prime}\cup C^{\prime}$ for all $A\in\mathcal{U}$. Put $\mathcal{V}^{\prime}=\left\{B^{\prime}\mid B\in\mathcal{V}^{*}\right\}^{*}$ and $\mathcal{W}^{\prime}=\left\{C^{\prime}\mid C\in\mathcal{W}^{*}\right\}^{*}$. Then, we have $\mathcal{U}\mathrel{\widetilde{\mathrel{\vdash}}}\mathcal{V}^{\prime}\vee\mathcal{W}^{\prime}$, $\mathcal{V}^{\prime}\mathrel{\widetilde{\ll_{\mathrel{\vdash}}}}\mathcal{V}$ and $\mathcal{W}^{\prime}\mathrel{\widetilde{\ll_{\mathrel{\vdash}}}}\mathcal{W}$. ∎

Lemma 5.15**.**

For each strong proximity lattice $(S,\prec)$, the structure $(S,\mathrel{\vdash},\prec)$, where $\mathrel{\vdash}$ is defined by (4.1), is a strong continuous entailment relation. Moreover the relation $\ll_{\mathrel{\vdash}}$ determined by $(S,\mathrel{\vdash},\prec)$ is characterised by (5.7).

Proof.

Straightforward. ∎

By Lemma 5.14 and Lemma 5.15, we have the following.

Theorem 5.16**.**

The functor $F\colon\mathsf{ContEnt}\to\mathsf{ProxLat}$ restricts to $\mathsf{SContEnt_{Prox}}$ and $\mathsf{SProxLat_{Prox}}$, which establishes equivalence of the latter two categories. ∎

The following corresponds to the notion of join-preserving proximity relation.

Definition 5.17**.**

Let $(S,\mathrel{\vdash},\prec)$ and $(S^{\prime},\mathrel{\vdash}^{\prime},\prec^{\prime})$ be strong continuous entailment relations. A proximity map $r\colon(S,\mathrel{\vdash},\prec)\to(S^{\prime},\mathrel{\vdash}^{\prime},\prec^{\prime})$ is join-preserving if

1. (JP)

$A\mathrel{r}B\;\rightarrow\>\exists\,\mathcal{U}\in\mathsf{Fin}(\mathsf{Fin}(S))\left(\left\{A\right\}\mathrel{\widetilde{\mathrel{\vdash}}}\mathcal{U}\>\&\>\forall A^{\prime}\in\mathcal{U}\exists b\in B\left(A^{\prime}\mathrel{r}\left\{b\right\}\right)\right)$.

Since join-preserving proximity maps are closed under composition (see the remark below Proposition 5.20), strong continuous entailment relations and join-preserving proximity maps form a subcategory $\mathsf{SContEnt}$ of $\mathsf{SContEnt_{Prox}}$.

Let $\mathbf{1}=(\emptyset,\between,=)$ be a terminal object in $\mathsf{SContEnt}$. The notion of join-preserving proximity map is consistent with the theory $T(S,\mathrel{\vdash},\prec)$ in (5.6).

Proposition 5.18**.**

For any strong continuous entailment relation $(S,\mathrel{\vdash},\prec)$, there exists a bijective correspondence between the models of $T(S,\mathrel{\vdash},\prec)$ and the join-preserving proximity maps from $\mathbf{1}$ to $S$.

Proof.

A model $\alpha$ of $T(S,\mathrel{\vdash},\prec)$ corresponds to a join-preserving proximity map $r_{\alpha}\colon\mathbf{1}\to S$ defined by

[TABLE]

Conversely, a join-preserving proximity map $r\colon\mathbf{1}\to S$ corresponds to a model $\alpha_{r}$ of ${T(S,\mathrel{\vdash},\prec)}$ defined by

[TABLE]

It is straightforward to check that the above correspondence is bijective. ∎

We now restrict Theorem 5.16 to $\mathsf{SContEnt}$ and $\mathsf{SProxLat}$. The following should be compared with Vickers [24, Theorem 42].

Lemma 5.19**.**

The condition (JP) is equivalent to the following:

1. (JP[math])

$A\mathrel{r}\emptyset\;\rightarrow\>A\mathrel{\vdash}\emptyset$, 2. (JP$\vee$)

$A\mathrel{r}B\cup C\;\rightarrow\>\exists\,\mathcal{U},\mathcal{V}\in\mathsf{Fin}(\mathsf{Fin}(S))\left(\left\{A\right\}\mathrel{\widetilde{\mathrel{\vdash}}}\mathcal{U}\cup\mathcal{V}\>\&\>\mathcal{U}\mathrel{\widetilde{r}}\left\{B\right\}^{*}\>\&\>\mathcal{V}\mathrel{\widetilde{r}}\left\{C\right\}^{*}\right)$.

Proof.

Assume (JP). For (JP[math]), if $A\mathrel{r}\emptyset$, then we must have $\left\{A\right\}\mathrel{\widetilde{\mathrel{\vdash}}}\emptyset$ so $A\mathrel{\vdash}\emptyset$. For (JP$\vee$), suppose that $A\mathrel{r}B\cup C$. By (JP), there exist $\mathcal{U},\mathcal{V}\in\mathsf{Fin}(\mathsf{Fin}(S))$ such that $\left\{A\right\}\mathrel{\widetilde{\mathrel{\vdash}}}\mathcal{U}\cup\mathcal{V}$, and $\forall B^{\prime}\in\mathcal{U}\exists b\in B\left(B^{\prime}\mathrel{r}\left\{b\right\}\right)$ and $\forall C^{\prime}\in\mathcal{V}\exists c\in C\left(C^{\prime}\mathrel{r}\left\{c\right\}\right)$. Then, $\forall B^{\prime}\in\mathcal{U}\left(B^{\prime}\mathrel{r}B\right)$ and $\forall C^{\prime}\in\mathcal{V}\left(C^{\prime}\mathrel{r}C\right)$.

Conversely, assume (JP[math]) and (JP$\vee$). We show (JP) by induction on the size of $B$. The base case $B=\emptyset$ follows from (JP[math]). For the inductive case, suppose that $A\mathrel{r}B\cup\left\{b\right\}$. By (JP$\vee$), there exist $\mathcal{U},\mathcal{V}\in\mathsf{Fin}(\mathsf{Fin}(S))$ such that $A\mathrel{\widetilde{\mathrel{\vdash}}}\mathcal{U}\cup\mathcal{V}$, $\mathcal{U}\mathrel{\widetilde{r}}\left\{B\right\}^{*}$, and $\mathcal{V}\mathrel{\widetilde{r}}\left\{\left\{b\right\}\right\}^{*}$. By induction hypothesis, for each $C\in\mathcal{U}$ there exists $\mathcal{U}_{C}\in\mathsf{Fin}(\mathsf{Fin}(S))$ such that $C\mathrel{\widetilde{\mathrel{\vdash}}}\mathcal{U}_{C}$ and $\forall B^{\prime}\in\mathcal{U}_{C}\exists b^{\prime}\in B\left(B^{\prime}\mathrel{r}\left\{b^{\prime}\right\}\right)$. Then $\bigcup_{C\in\mathcal{U}}\mathcal{U}_{C}\cup\mathcal{V}$ witnesses (JP) for $B\cup\left\{b\right\}$. ∎

Proposition 5.20**.**

A proximity map $r\colon(S,\mathrel{\vdash},\prec)\to(S^{\prime},\mathrel{\vdash}^{\prime},\prec^{\prime})$ is join-preserving if and only if $\mathrel{\widetilde{r}}\colon(\mathrm{DL}(S,\mathrel{\vdash}),\mathrel{\widetilde{\ll_{\mathrel{\vdash}}}})\to(\mathrm{DL}(S^{\prime},\mathrel{\vdash}^{\prime}),\mathrel{\widetilde{\ll_{\mathrel{\vdash}^{\prime}}}})$ is join-preserving.

Proof.

Suppose that $r$ is join-preserving.

(Prox[math]) Suppose $\mathcal{U}\mathrel{\mathrel{\widetilde{r}}}\emptyset$. By (JP[math]), we have $A\mathrel{\vdash}\emptyset$ for all $A\in\mathcal{U}$. Thus $\mathcal{U}\mathrel{\widetilde{\mathrel{\vdash}}}\emptyset$.

(Prox$\vee$) Suppose $\mathcal{U}\mathrel{\widetilde{r}}\mathcal{V}\vee\mathcal{W}$. Since $(\mathcal{V}\vee\mathcal{W})^{*}=_{\mathrel{\vdash}^{\prime}}\mathcal{V}^{*}\wedge\mathcal{W}^{*}$ in $\mathrm{DL}(S^{\prime},\mathrel{\vdash}^{\prime})$, for each $A\in\mathcal{U}$, $B\in\mathcal{V}^{*}$, and $C\in\mathcal{W}^{*}$, we have $A\mathrel{r}B\cup C$. By (JP$\vee$), there exist $\mathcal{V}_{A,B,C},\mathcal{W}_{A,B,C}\in\mathsf{Fin}(\mathsf{Fin}(S))$ such that $A\mathrel{\widetilde{\mathrel{\vdash}}}\mathcal{V}_{A,B,C}\cup\mathcal{W}_{A,B,C}$, $\mathcal{V}_{A,B,C}\mathrel{\widetilde{r}}\left\{B\right\}^{*}$, and $\mathcal{W}_{A,B,C}\mathrel{\widetilde{r}}\left\{C\right\}^{*}$. Put

[TABLE]

Then, $\mathcal{V}^{\prime}\mathrel{\mathrel{\widetilde{r}}}\mathcal{V}$ and $\mathcal{W}^{\prime}\mathrel{\mathrel{\widetilde{r}}}\mathcal{W}$. Since

[TABLE]

for each $A\in\mathcal{U}$, we have $\mathcal{U}\mathrel{\widetilde{\mathrel{\vdash}}}\mathcal{V}^{\prime}\cup\mathcal{W}^{\prime}$.

Conversely, suppose that $\mathrel{\widetilde{r}}$ is join-preserving. We show (JP[math]) and (JP$\vee$).

(JP[math]) Suppose $A\mathrel{r}\emptyset$. Then $\left\{A\right\}\mathrel{\mathrel{\widetilde{r}}}\emptyset$. Thus $\left\{A\right\}\mathrel{\widetilde{\mathrel{\vdash}}}\emptyset$ by (Prox[math]), and so $A\mathrel{\vdash}\emptyset$.

(JP$\vee$) Suppose $A\mathrel{r}B\cup C$. Then $\left\{A\right\}\mathrel{\mathrel{\widetilde{r}}}\left\{B\right\}^{*}\vee\left\{C\right\}^{*}$. By (Prox$\vee$), there exist $\mathcal{U},\mathcal{V}\in\mathsf{Fin}(\mathsf{Fin}(S))$ such that $\left\{A\right\}\mathrel{\widetilde{\mathrel{\vdash}}}\mathcal{U}\cup\mathcal{V}$, $\mathcal{U}\mathrel{\mathrel{\widetilde{r}}}\left\{B\right\}^{*}$, and $\mathcal{V}\mathrel{\mathrel{\widetilde{r}}}\left\{C\right\}^{*}$. ∎

In particular, since join-preserving proximity relations are closed under composition, so do join-preserving proximity maps.

Theorem 5.21**.**

The categories $\mathsf{SContEnt}$ and $\mathsf{SProxLat}$ are equivalent.

Proof.

By Theorem 5.16 and Proposition 5.20, the functor $F\colon\mathsf{ContEnt}\to\mathsf{ProxLat}$ restricts to a full and faithful functor from $\mathsf{SContEnt}$ to $\mathsf{SProxLat}$. Since every isomorphic proximity relation between $\vee$-strong proximity lattices is join-preserving, $F$ establishes an equivalence of $\mathsf{SContEnt}$ and $\mathsf{SProxLat}$. ∎

By an abuse of notation, we write $F\colon\mathsf{SContEnt}\to\mathsf{SProxLat}$ and $G\colon\mathsf{SProxLat}\to\mathsf{SContEnt}$ for the restrictions of the functor $F\colon\mathsf{ContEnt}\to\mathsf{ProxLat}$ and its quasi-inverse $G\colon\mathsf{ProxLat}\to\mathsf{ContEnt}$.

Remark 5.22*.*

Many of the examples in Section 7 start from a strong proximity lattice $(S,\prec)$ and specify a strong continuous entailment relation which represents the desired construction on $\mathrm{Spec}(S)$. The functor $F\colon\mathsf{SContEnt}\to\mathsf{SProxLat}$ then allows us to calculate the corresponding construction on $(S,\prec)$.

The presentations of stably compact locales are invariant under the equivalence of $\mathsf{SContEnt}$ and $\mathsf{SProxLat}$ in the following sense.

Proposition 5.23**.**

For any strong proximity lattice $(S,\prec)$, the locale $\mathrm{Spec}(S)$ is presented by $G(S,\prec)$. 2. 2.

For any continuous entailment relation $(S,\mathrel{\vdash},\prec)$, the locale ${\mathrm{Spec}(F(S,\mathrel{\vdash},\prec))}$ is presented by $(S,\mathrel{\vdash},\prec)$.

Proof.

1. This is clear from the definition of $G(S,\prec)$ and Corollary 5.7.

2. First, we define a bijection between interpretations of $(S,\mathrel{\vdash},\prec)$ in a locale $X$ and interpretations of $GF(S,\mathrel{\vdash},\prec)$ in $X$ via a mapping $a\mapsto\left\{\left\{a\right\}\right\}\colon S\to\mathsf{Fin}(\mathsf{Fin}(S))$. Let $f\colon S\to{\mathrm{\Omega}(X})$ be an interpretation of $(S,\mathrel{\vdash},\prec)$ in $X$. Define $\overline{f}\colon\mathsf{Fin}(\mathsf{Fin}(S))\to{\mathrm{\Omega}(X})$ by

[TABLE]

which clearly satisfies $\overline{f}(\left\{\left\{a\right\}\right\})=f(a)$ for all $a\in S$. We show that $\overline{f}$ preserves the order on $\mathrm{DL}(S,\mathrel{\vdash})$, which implies that $\overline{f}$ respects the equality on $\mathrm{DL}(S,\mathrel{\vdash})$. Suppose $\mathcal{U}\mathrel{\widetilde{\mathrel{\vdash}}}\mathcal{V}$. Since $f$ is an interpretation of $(S,\mathrel{\vdash},\prec)$, we have

[TABLE]

where $\leq_{X}$ is the order on $X$. Thus, $\overline{f}$ is a function on $\mathrm{DL}(S,\mathrel{\vdash})$. Similarly, we have $\mathcal{U}\mathrel{\widetilde{\ll_{\mathrel{\vdash}}}}\mathcal{V}\;\rightarrow\>\overline{f}(\mathcal{U})\leq_{X}\overline{f}(\mathcal{V})$. It is also easy to check that $\overline{f}$ preserves finite meets and finite joins. Furthermore, for any $A\in\mathsf{Fin}(S)$, we have

[TABLE]

which implies $\overline{f}(\mathcal{U})\leq_{X}\!\bigvee_{\mathcal{V}\mathrel{\widetilde{\ll_{\mathrel{\vdash}}}}\mathcal{U}}\overline{f}(\mathcal{V})$. Thus, $\overline{f}$ is an interpretation of $GF(S,\mathrel{\vdash},\prec)$ in $X$. Since $\mathcal{U}=_{\mathrel{\vdash}}\operatorname*{{\textstyle{\bigvee}}}_{A\in\mathcal{U}}\operatorname*{{\textstyle{\bigwedge}}}_{a\in A}\left\{\left\{a\right\}\right\}$ for each $\mathcal{U}\in\mathsf{Fin}(\mathsf{Fin}(S))$, $\overline{f}$ is a unique interpretation of $GF(S,\mathrel{\vdash},\prec)$ in $X$ such that $\overline{f}(\left\{\left\{a\right\}\right\})=f(a)$ for all $a\in S$.

Define $j_{S}\colon S\to\mathrm{RIdl}(F(S,\mathrel{\vdash},\prec))$ by $j_{S}(a)=\mathord{\downarrow}_{\mathrel{\widetilde{\ll_{\mathrel{\vdash}}}}}\left\{\left\{a\right\}\right\}$. Then, it is straightforward to show that $j_{S}$ is a universal interpretation of $(S,\mathrel{\vdash},\prec)$. ∎

5.3 Generated strong continuous entailment

relations

To construct a new entailment relation, one often specifies a set of initial entailments from which the entire relation is generated.

Definition 5.24**.**

An axiom on a set $S$ is a pair $(A,B)\in\mathsf{Fin}(S)\times\mathsf{Fin}(S)$. Given a set $\mathrel{\vdash}_{0}$ of axioms on $S$, an entailment relation $(S,\mathrel{\vdash})$ is said to be generated by $\mathrel{\vdash}_{0}$ if $\mathrel{\vdash}$ is the smallest entailment relation on $S$ that contains $\mathrel{\vdash}_{0}$.

We usually write $A\mathrel{\vdash}_{0}B$ for $(A,B)\mathop{\in}\mathrel{\vdash}_{0}$.

Lemma 5.25**.**

If $\mathrel{\vdash}_{0}$ is a set of axioms on a set $S$, then the entailment relation $\mathrel{\vdash}$ generated by $\mathrel{\vdash}_{0}$ is inductively defined by the following rules:

[TABLE]

Proof.

First, we show that the relation $\mathrel{\vdash}$ generated by $(\mathrm{R^{\prime}})$ and $(\mathrm{AxL})$ is an entailment relation. The proof is by induction on the height of derivations of the premises of each condition in Definition 4.3. For example, to see that $\mathrel{\vdash}$ satisfies ($\mathrm{T}$), we show that $\mathrel{\vdash}$ satisfies more general condition:

[TABLE]

Suppose $A\mathrel{\vdash}B,a$ and $a,A^{\prime}\mathrel{\vdash}B^{\prime}$. Then $A\mathrel{\vdash}B,a$ is derived by either ($\mathrm{R^{\prime}}$) or ($\mathrm{AxL}$). The former case is easy. In the latter case, $A\mathrel{\vdash}B,a$ is of the form $C^{\prime},C\mathrel{\vdash}B,a$ for some $C\mathrel{\vdash}_{0}D$ such that $\forall d\in D\left(C^{\prime},d\mathrel{\vdash}B,a\right)$. By induction hypothesis, we have $A^{\prime},C^{\prime},d\mathrel{\vdash}B,B^{\prime}$ for all $d\in D$. Hence $A^{\prime},C,C^{\prime}\mathrel{\vdash}B,B^{\prime}$ by ($\mathrm{AxL}$). Next, if $\mathrel{\vdash}^{\prime}$ is another entailment relation on $S$ containing $\mathrel{\vdash}_{0}$, then $\mathrel{\vdash}^{\prime}$ satisfies ($\mathrm{R^{\prime}}$) and ($\mathrm{AxL}$), so $\mathrel{\vdash}^{\prime}$ must contain $\mathrel{\vdash}$. ∎

Dually, we have the following.

Lemma 5.26**.**

If $\mathrel{\vdash}_{0}$ is a set of axioms on a set $S$, the entailment relation $\mathrel{\vdash}$ generated by $\mathrel{\vdash}_{0}$ is inductively defined by the following rules:

[TABLE]

∎

The following is useful when defining a new strong continuous entailment relation using axioms.

Lemma 5.27**.**

Let $\mathrel{\vdash}$ be an entailment relation on a set $S$ generated by a set $\mathrel{\vdash}_{0}$ of axioms. If $\prec$ is an idempotent relation on $S$ such that

$C\prec_{U}A\mathrel{\vdash}_{0}B\;\rightarrow\>\exists B^{\prime}\in\mathsf{Fin}(S)\left(C\mathrel{\vdash}B^{\prime}\prec_{L}B\right)$, 2. 2.

$A\mathrel{\vdash}_{0}B\prec_{L}C\;\rightarrow\>\exists A^{\prime}\in\mathsf{Fin}(S)\left(A\prec_{U}A^{\prime}\mathrel{\vdash}C\right)$,

then $(S,\mathrel{\vdash},\prec)$ is a strong continuous entailment relation.

Proof.

Let $\prec$ be an idempotent relation on $S$ satisfying 1 and 2. We show only one direction of (5.5),

[TABLE]

by induction on the derivation of $A\mathrel{\vdash}B$. If $A\mathrel{\vdash}B$ is derived by ($\mathrm{R^{\prime}}$), then the conclusion is trivial. Suppose that $A,A^{\prime}\mathrel{\vdash}B$ is derived by ($\mathrm{AxL}$). Then, there exists $C\in\mathsf{Fin}(S)$ such that $A\mathrel{\vdash}_{0}C$ and $\forall c\in C\left(A^{\prime},c\mathrel{\vdash}B\right)$. Let $D\prec_{U}A\cup A^{\prime}$. Since $D\prec_{U}A$, there exists $C^{\prime}\prec_{L}C$ such that $D\mathrel{\vdash}C^{\prime}$ by 1. By induction hypothesis, for each $c^{\prime}\in C^{\prime}$, there exists $B_{c^{\prime}}\prec_{L}B$ such that $D,c^{\prime}\mathrel{\vdash}B_{c^{\prime}}$. Put $B^{\prime}=\bigcup_{c^{\prime}\in C^{\prime}}B_{c^{\prime}}$. Then, by successive applications of ($\mathrm{T}$), we obtain $D\mathrel{\vdash}B^{\prime}$.

The other direction of (5.5) follows from 2 and Lemma 5.26. ∎

As an application of generated strong continuous entailment relations, we show that $\mathsf{SProxLat_{Prox}}$ and $\mathsf{JSProxLat_{Prox}}$ are equivalent. Recall that the functor $F\colon\mathsf{ContEnt}\to\mathsf{ProxLat}$ restricts to an equivalence of $\mathsf{SContEnt_{Prox}}$ and $\mathsf{SProxLat_{Prox}}$ (Theorem 5.16). Composing $F$ with the inclusion $\mathsf{SProxLat_{Prox}}\hookrightarrow\mathsf{JSProxLat_{Prox}}$, we get a full and faithful functor $F^{\prime}\colon\mathsf{SContEnt_{Prox}}\to\mathsf{JSProxLat_{Prox}}$.

Lemma 5.28**.**

The functor $F^{\prime}$ is essentially surjective.

Proof.

Given a $\vee$-strong proximity lattice $(S,\prec)$, define an entailment relation $\mathrel{\vdash}^{\wedge}$ on $S$ by specifying its axioms as follows:

[TABLE]

Using Lemma 5.27, one can show that $(S,\mathrel{\vdash}^{\wedge},\prec)$ is a strong continuous entailment relation. On the other hand, let $G(S,\prec)=(S,\mathrel{\vdash},\ll)$ be the continuous entailment relation determined by the quasi-inverse $G$ of $F$ (see (4.1) and (5.7)). It suffices to show that $(S,\mathrel{\vdash}^{\wedge},\prec)$ and $(S,\mathrel{\vdash},\ll)$ are isomorphic as continuous entailment relations. By induction on $\mathrel{\vdash}^{\wedge}$, we see that

[TABLE]

Then, it is straightforward to show that $\ll\cdot\ll_{\mathrel{\vdash}^{\wedge}}{=}\ll_{\mathrel{\vdash}^{\wedge}}{=}\ll_{\mathrel{\vdash}^{\wedge}}\cdot\ll_{\mathrel{\vdash}^{\wedge}}$ and $\ll_{\mathrel{\vdash}^{\wedge}}\cdot\ll{=}\ll{=}\ll\cdot\ll$. Thus $\ll$ and $\ll_{\mathrel{\vdash}^{\wedge}}$ are proximity maps $\ll\colon{(S,\mathrel{\vdash},\ll)}\to(S,\mathrel{\vdash}^{\wedge},\ll_{\mathrel{\vdash}^{\wedge}})$ and $\ll_{\mathrel{\vdash}^{\wedge}}\colon(S,\mathrel{\vdash}^{\wedge},\ll_{\mathrel{\vdash}^{\wedge}})\to(S,\mathrel{\vdash},\ll)$ and inverse to each other. ∎

Theorem 5.29**.**

The categories $\mathsf{SContEnt_{Prox}}$, $\mathsf{ContEnt}$, $\mathsf{ProxLat}$, $\mathsf{JSProxLat_{Prox}}$, and $\mathsf{SProxLat_{Prox}}$ are equivalent.

Proof.

By Lemma 5.28, Theorem 5.16, and Theorem 5.8. ∎

Since every isomorphic proximity relation between $\vee$-strong proximity lattices are join-preserving, we also have the following by Theorem 5.21.

Theorem 5.30**.**

The categories $\mathsf{SContEnt}$, $\mathsf{JSProxLat}$, and $\mathsf{SProxLat}$ are equivalent. ∎

6 De Groot duality

In point-set topology, the de Groot dual of a stably compact space has the same set of points equipped with the cocompact topology: the topology generated by the complements of compact saturated subsets of the original space. By Hofmann–Mislove theorem, compact saturated subsets correspond to Scott open filters, which are amenable to point-free treatment. Thus, the de Groot dual of a stably compact locale $X$ is defined to be the locale whose frame is the Scott open filters on ${\mathrm{\Omega}(X})$; see Escardó [5]. We relate the de Groot duality to the structural dualities of proximity lattices and continuous entailment relations.

6.1 Duality of proximity lattices

Definition 6.1**.**

The dual ${{S}^{\mathsf{\circ}}}$ of a distributive lattice $S=(S,0,\vee,1,\wedge)$ is the distributive lattice $(S,1,\wedge,0,\vee)$ with the opposite order. The dual ${{S}^{\mathsf{d}}}$ of a proximity lattice $S=(S,\prec)$ is the proximity lattice $({{S}^{\mathsf{\circ}}},\succ)$.

Our aim is to give a localic account of [16, Section 4], which shows that $\mathrm{RIdl}({{S}^{\mathsf{d}}})$ is isomorphic to the frame of Scott open filters on $\mathrm{RIdl}(S)$.

Definition 6.2**.**

Let $(S,\prec)$ be a proximity lattice. Write $\Sigma(\mathrm{Spec}(S))$ for the locale whose models are rounded ideals of $S$, i.e., $\Sigma(\mathrm{Spec}(S))$ is presented by a geometric theory $T_{\Sigma}$ over $S$ with the following axioms:

[TABLE]

Let $\mathrm{Upper}(S)$ be the collection of rounded upper subsets of $(S,\prec)$, i.e., those subset $U\subseteq S$ such that $a\in U\leftrightarrow\exists b\prec a\left(b\in U\right)$. Clearly, $\mathrm{Upper}(S)$ is closed under all joins, which are just unions. Moreover, (ProxI) ensures that $\mathrm{Upper}(S)$ has finite meets defined by

[TABLE]

where $\mathord{\uparrow}_{\prec}a\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\left\{b\in S\mid b\succ a\right\}$. These finite meets clearly distribute over all joins. Hence $\mathrm{Upper}(S)$ is a frame.

Lemma 6.3**.**

The frames ${\mathrm{\Omega}(\Sigma(\mathrm{Spec}(S))})$ and $\mathrm{Upper}(S)$ are isomorphic.

Proof.

It is straightforward to show that a function $i_{\Sigma}\colon S\to\mathrm{Upper}(S)$ defined by $i_{\Sigma}(a)\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\mathord{\uparrow}_{\prec}a$ is a universal interpretation of $T_{\Sigma}$. ∎

Proposition 6.4**.**

The frame ${\mathrm{\Omega}(\Sigma(\mathrm{Spec}(S))})$ is the Scott topology on $\mathrm{RIdl}(S)$.

Proof.

It is known that $\mathrm{Upper}(S)$ is the Scott topology on $\mathrm{RIdl}(S)$; see Vickers [21, Lemma 2.11] or Jung and Sünderhauf [16, Lemma 14]. Then, the claim follows from Lemma 6.3. ∎

Scott open filters on a locale $X$ are models of the upper powerlocale of $X$, which is characterised by the following universal property; see Vickers [22].

Definition 6.5**.**

The upper powerlocale of a locale $X$ is a locale $\mathrm{P_{U}}(X)$ together with a preframe homomorphism $i_{U}\colon{\mathrm{\Omega}(X})\to{\mathrm{\Omega}(\mathrm{P_{U}}(X)})$ such that for any preframe homomorphism $f\colon{\mathrm{\Omega}(X})\to{\mathrm{\Omega}(Y})$ to a locale $Y$, there exists a unique frame homomorphism $\overline{f}\colon{\mathrm{\Omega}(\mathrm{P_{U}}(X)})\to{\mathrm{\Omega}(Y})$ such that $\overline{f}\circ i_{U}=f$.

Proposition 6.6**.**

For any proximity lattice $S$, $\Sigma(\mathrm{Spec}({{S}^{\mathsf{d}}}))$ is the upper powerlocale of $\mathrm{Spec}(S)$.

Proof.

By Definition 6.2, the locale $\Sigma(\mathrm{Spec}({{S}^{\mathsf{d}}}))$ is presented by a geometric theory $T$ over $S$ with the following axioms:

[TABLE]

By the preframe version of Proposition 5.5 (see also Remark 5.6), the universal interpretation $i_{T}\colon S\to{\mathrm{\Omega}(\Sigma(\mathrm{Spec}({{S}^{\mathsf{d}}}))})$ of $T$ in $\Sigma(\mathrm{Spec}({{S}^{\mathsf{d}}}))$ uniquely extends to a preframe homomorphism $i_{U}\colon\mathrm{RIdl}(S)\to{\mathrm{\Omega}(\Sigma(\mathrm{Spec}({{S}^{\mathsf{d}}}))})$ via the function $i_{S}\colon S\to\mathrm{RIdl}(S)$ defined by (5.2). Then, it is straightforward to show that $i_{U}$ satisfies the universal property of the upper powerlocale of $\mathrm{Spec}(S)$. ∎

Theorem 6.7**.**

For any proximity lattice $S$, the frame $\mathrm{RIdl}({{S}^{\mathsf{d}}})$ is isomorphic to the frame of Scott open filters on $\mathrm{RIdl}(S)$. Thus, $\mathrm{Spec}({{S}^{\mathsf{d}}})$ is the de Groot dual of $\mathrm{Spec}(S)$.

Proof.

Since $\mathrm{RIdl}({{S}^{\mathsf{d}}})$ is the collection of models of $\Sigma(\mathrm{Spec}({{S}^{\mathsf{d}}}))$, it is isomorphic to the frame of Scott open filters on $\mathrm{RIdl}(S)$ by Proposition 6.6 ∎

We extend the duality to morphisms. The following are obvious.

Lemma 6.8**.**

If $r\colon S\to S^{\prime}$ is a proximity relation between proximity lattices, then the relational opposite $r^{-}\!$ is a proximity relation $r^{-}\colon{{S^{\prime}}^{\mathsf{d}}}\to{{S}^{\mathsf{d}}}$. ∎

Proposition 6.9**.**

The assignment $r\mapsto r^{-}$ determines a dual isomorphism ${(\cdot)^{-}\colon\mathsf{ProxLat}\xrightarrow{\cong}{{\mathsf{ProxLat}}^{\mathsf{op}}}}$. ∎

All of the categories we have introduced so far ($\mathsf{ProxLat}$, $\mathsf{ContEnt}$ etc.) are order-enriched categories, where homsets are ordered by the set-theoretic inclusion. Thus, the following notion applies.

Definition 6.10**.**

Let $\mathbb{C}$ be an order-enriched category. For morphisms $f\colon A\to B$ and $g\colon B\to A$, we say that $f$ is a left adjoint to $g$ and $g$ is a right adjoint to $f$ if $f\circ g\leq_{B}\mathrm{id}_{B}$ and $\mathrm{id}_{A}\leq_{A}g\circ f$, where $\leq_{A}$ and $\leq_{B}$ are the orders on $\mathsf{Hom}(A,A)_{\mathbb{C}}$ and $\mathsf{Hom}(B,B)_{\mathbb{C}}$ respectively. In this case, $(f,g)$ is called an adjoint pair of morphisms from $A$ to $B$.

Let $\mathsf{ProxLat_{Perf}}$ be the subcategory of $\mathsf{ProxLat}$ where morphisms from $S$ to $S^{\prime}$ are adjoint pairs of proximity relations from $S^{\prime}$ to $S$. The identity on $(S,\prec)$ is $(\prec,\prec)$, and the composition of adjoint pairs $(s,r)$ and $(s^{\prime},r^{\prime})$ is $(s\circ s^{\prime},r^{\prime}\circ r)$.

Theorem 6.11**.**

The assignment $(s,r)\colon S\to S^{\prime}\mapsto(r^{-},s^{-})\colon{{S}^{\mathsf{d}}}\to{{S^{\prime}}^{\mathsf{d}}}$ determines an isomorphism ${{(\cdot)}^{\mathsf{d}}}\colon\mathsf{ProxLat_{Perf}}\xrightarrow{\cong}\mathsf{ProxLat_{Perf}}$.

Proof.

Since the functor $(\cdot)^{-}\colon\mathsf{ProxLat}\to{{\mathsf{ProxLat}}^{\mathsf{op}}}$ preserves the order on morphisms, for any morphism $(s,r)\colon S\to S^{\prime}$ in $\mathsf{ProxLat_{Perf}}$ (i.e. an adjoint pair of proximity relations from $S^{\prime}$ to $S$), the pair $(r^{-},s^{-})$ is an adjoint pair from ${{S^{\prime}}^{\mathsf{d}}}$ to ${{S}^{\mathsf{d}}}$, i.e., a morphism $(r^{-},s^{-})\colon{{S}^{\mathsf{d}}}\to{{S^{\prime}}^{\mathsf{d}}}$ in $\mathsf{ProxLat_{Perf}}$. ∎

A locale map $f\colon X\to Y$ is perfect if the corresponding frame homomorphism ${\mathrm{\Omega}(f})\colon{\mathrm{\Omega}(Y})\to{\mathrm{\Omega}(X})$ has a Scott continuous right adjoint $g\colon{\mathrm{\Omega}(X})\to{\mathrm{\Omega}(Y})$. In this case, $g$ is necessarily a preframe homomorphism. An adjoint pair $(s,r)\colon S\to S^{\prime}$ of proximity relations in $\mathsf{ProxLat_{Perf}}$ corresponds to a perfect map from $\mathrm{Spec}(S)$ to $\mathrm{Spec}(S^{\prime})$. Hence, Theorem 6.11 is a manifestation of the de Groot duality of stably compact locales in the setting of proximity lattice.

6.2 Duality of continuous entailment relations

We describe an analogous duality on the category $\mathsf{ContEnt}$, and relate it to the duality on $\mathsf{ProxLat}$ via the equivalence of the two categories.

Definition 6.12**.**

The dual ${{\mathrel{\vdash}}^{\mathsf{\circ}}}$ of an entailment relation $\mathrel{\vdash}$ on $S$ is the relational opposite: $A\mathrel{{{\mathrel{\vdash}}^{\mathsf{\circ}}}}B\stackrel{{\scriptstyle\textup{def}}}{{\iff}}B\mathrel{\vdash}A$. The dual ${{S}^{\mathsf{d}}}$ of a continuous entailment relation $S=(S,\mathrel{\vdash},\ll)$ is the continuous entailment relation $(S,{{\mathrel{\vdash}}^{\mathsf{\circ}}},\gg)$.

If $r\colon S\to S^{\prime}$ is a proximity map between continuous entailment relations, then $r^{-}$ is a proximity map $r^{-}\colon{{S^{\prime}}^{\mathsf{d}}}\to{{S}^{\mathsf{d}}}$. Then, the following is obvious.

Proposition 6.13**.**

The assignment $r\colon S\to S^{\prime}\mapsto r^{-}\colon{{S^{\prime}}^{\mathsf{d}}}\to{{S}^{\mathsf{d}}}$ determines a dual isomorphism $(\cdot)^{-}\colon\mathsf{ContEnt}\xrightarrow{\cong}{{\mathsf{ContEnt}}^{\mathsf{op}}}$. ∎

Theorem 6.14**.**

The equivalence $F\colon\mathsf{ContEnt}\to\mathsf{ProxLat}$ commutes with the dual isomorphisms $(\cdot)^{-}\!$ on $\mathsf{ContEnt}$ and $\mathsf{ProxLat}$ up to natural isomorphism.

Proof.

For each continuous entailment relation $(S,\mathrel{\vdash},\ll)$, define a relation $r_{S}\subseteq{{D(S,\mathrel{\vdash})}^{\mathsf{\circ}}}\times D(S,{{\mathrel{\vdash}}^{\mathsf{\circ}}})$ by

[TABLE]

Since $\mathcal{U}\mathrel{\widetilde{\ll}}\mathcal{V}\leftrightarrow\mathcal{V}^{*}\mathrel{\widetilde{\gg}}\mathcal{U}^{*}$, one can easily show that $r_{S}$ is a proximity relation from ${{F(S,\mathrel{\vdash},\ll)}^{\mathsf{d}}}$ to $F({{(S,\mathrel{\vdash},\ll)}^{\mathsf{d}}})$ with an inverse $t_{S}$ defined by

[TABLE]

To see that $r_{S}$ is natural in $S$, for any proximity map $r\colon(S,\mathrel{\vdash},\ll)\to(S^{\prime},\mathrel{\vdash}^{\prime},\ll^{\prime})$ and for any $\mathcal{U}\in\mathsf{Fin}(\mathsf{Fin}(S^{\prime}))$ and $\mathcal{V}\in\mathsf{Fin}(\mathsf{Fin}(S))$, we have

[TABLE]

Let $\mathsf{ContEnt_{Perf}}$ be the category of continuous entailment relations and adjoint pairs of proximity maps which is defined similarly as $\mathsf{ProxLat_{Perf}}$. The following is analogous to Theorem 6.11.

Proposition 6.15**.**

The assignment $(s,r)\colon S\to S^{\prime}\mapsto(r^{-},s^{-})\colon{{S}^{\mathsf{d}}}\to{{S^{\prime}}^{\mathsf{d}}}$ determines an isomorphism ${{(\cdot)}^{\mathsf{d}}}\colon\mathsf{ContEnt_{Perf}}\xrightarrow{\cong}\mathsf{ContEnt_{Perf}}$. ∎

Theorem 6.16**.**

The category $\mathsf{ContEnt_{Perf}}$ is equivalent to $\mathsf{ProxLat_{Perf}}$. The equivalence commutes with the isomorphisms ${{(\cdot)}^{\mathsf{d}}}\!$ on $\mathsf{ContEnt_{Perf}}$ and $\mathsf{ProxLat_{Perf}}$ up to natural isomorphism.

Proof.

Since the functor $F\colon\mathsf{ContEnt}\to\mathsf{ProxLat}$ preserves the order on morphisms, it can be restricted to an equivalence between $\mathsf{ContEnt_{Perf}}$ and $\mathsf{ProxLat_{Perf}}$. The second statement follows from Theorem 6.14. ∎

We introduce the notion of dual for strong continuous entailment relations.

Definition 6.17**.**

The dual of a strong continuous entailment relation $(S,\mathrel{\vdash},\prec)$ is a strong continuous entailment relation $(S,{{\mathrel{\vdash}}^{\mathsf{\circ}}},\succ)$.

Note that the inclusion $\mathsf{SContEnt_{Prox}}\hookrightarrow\mathsf{ContEnt}$ commutes with the dualities on both categories. Since strong proximity lattices are closed under the duality in the sense of Definition 6.1, Theorem 6.16 restricts to the full subcategories $\mathsf{SContEnt_{Perf}}$ and $\mathsf{SProxLat_{Perf}}$ of $\mathsf{ContEnt_{Perf}}$ and $\mathsf{ProxLat_{Perf}}$, respectively, which consist of strong continuous entailment relations and strong proximity lattices.

7 Applications of entailment relations

We present a number of constructions on stably compact locales in the setting of strong proximity lattices and strong continuous entailment relations and analyse their de Groot duals. For the sake of simplicity, we prefer to work with strong proximity lattices rather proximity lattices because the geometric theories of the locales represented by the former are simpler and easier to work with.

Our main tool is the following observation, together with Lemma 5.27.

Lemma 7.1**.**

If $(S,\mathrel{\vdash})$ is an entailment relation generated by a set $\mathrel{\vdash}_{0}$ of axioms, then the dual ${{\mathrel{\vdash}}^{\mathsf{\circ}}}$ is generated by ${{\mathrel{\vdash}_{0}}^{\mathsf{\circ}}}\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\left\{(B,A)\mid A\mathrel{\vdash}_{0}B\right\}$.

Proof.

Immediate from the structural symmetry of entailment relations. ∎

7.1 Powerlocales

We deal with the lower, upper, and Vietoris powerlocales and consider their interactions with the construction $\Sigma(\mathrm{Spec}(S))$, the locale whose frame is the Scott topology on $\mathrm{RIdl}(S)$. For the localic account of powerlocales, the reader is referred to Vickers [22, 23].

7.1.1 Lower and upper powerlocales

Lemma 7.2**.**

Let $(S,\prec)$ be a strong proximity lattice.

The locale $\Sigma(\mathrm{Spec}(S))$ is presented by a strong continuous entailment relation $\Sigma(S)=(S,\mathrel{\vdash}_{\Sigma},\succ)$ where $\mathrel{\vdash}_{\Sigma}$ is generated by the following axioms:

[TABLE] 2. 2.

The upper powerlocale of $\mathrm{Spec}(S)$ is presented by a strong continuous entailment relation $\mathrm{P_{U}}(S)=(S,\mathrel{\vdash}_{U},\prec)$ where $\mathrel{\vdash}_{U}$ is generated by the following axioms:

[TABLE]

In particular, (the locale whose frame is) the Scott topology and the upper powerlocale of a stably compact locale are stably compact.

Proof.

It is straightforward to check that $\Sigma(S)$ and $\mathrm{P_{U}}(S)$ satisfy the condition in Lemma 5.27. Then, item 1 is immediate from Definition 6.2, while item 2 follows from Proposition 6.6. ∎

Note that $A\mathrel{\vdash}_{\Sigma}B\leftrightarrow\exists b\in B\left(b\leq\operatorname*{{\textstyle{\bigvee}}}A\right)$ and $A\mathrel{\vdash}_{U}B\leftrightarrow\exists b\in B\left(\operatorname*{{\textstyle{\bigwedge}}}A\leq b\right)$. The constructions $\Sigma(S)$ and $\mathrm{P_{U}}(S)$ extend to functors $\Sigma\colon{{\mathsf{SProxLat}}^{\mathsf{op}}}\to\mathsf{SContEnt}$ and $\mathrm{P_{U}}\colon\mathsf{SProxLat}\to\mathsf{SContEnt}$, which send each join-preserving proximity relation $r\colon(S,\prec)\to(S^{\prime},\prec^{\prime})$ to join-preserving proximity maps $\Sigma(r)\colon\Sigma(S^{\prime})\to\Sigma(S)$ and $\mathrm{P_{U}}(r)\colon\mathrm{P_{U}}(S)\to\mathrm{P_{U}}(S^{\prime})$ defined by

[TABLE]

The notion of lower powerlocale is the dual of that of upper powerlocale.

Definition 7.3**.**

The lower powerlocale of a locale $X$ is a locale $\mathrm{P_{L}}(X)$ together with a suplattice homomorphism $i_{L}\colon{\mathrm{\Omega}(X})\to{\mathrm{\Omega}(\mathrm{P_{L}}(X)})$ such that for any suplattice homomorphism $f\colon{\mathrm{\Omega}(X})\to{\mathrm{\Omega}(Y})$ to a locale $Y$, there exists a unique frame homomorphism $\overline{f}\colon{\mathrm{\Omega}(\mathrm{P_{L}}(X)})\to{\mathrm{\Omega}(Y})$ such that $\overline{f}\circ i_{L}=f$.

Lemma 7.4**.**

For any strong proximity lattice $(S,\prec)$, the lower powerlocale of $\mathrm{Spec}(S)$ is presented by a strong continuous entailment relation $\mathrm{P_{L}}(S)={(S,\mathrel{\vdash}_{L},\prec)}$ where $\mathrel{\vdash}_{L}$ is generated by the following axioms:

[TABLE]

In particular, the lower powerlocale of a stably compact locale is stably compact.

Proof.

Immediate from the suplattice version of Proposition 5.5. ∎

Note that $A\mathrel{\vdash}_{L}B\leftrightarrow\exists a\in A\left(a\leq\operatorname*{{\textstyle{\bigvee}}}B\right).$ The construction $\mathrm{P_{L}}(S)$ extends to a functor $\mathrm{P_{L}}\colon\mathsf{SProxLat}\to\mathsf{SContEnt}$, which sends each join-preserving proximity relation $r\colon(S,\prec)\to(S^{\prime},\prec^{\prime})$ to a join-preserving proximity map $\mathrm{P_{L}}(r)\colon\mathrm{P_{L}}(S)\to\mathrm{P_{L}}(S^{\prime})$ defined by

[TABLE]

Theorem 7.5**.**

For any strong proximity lattice $S$, we have

${{\mathrm{P_{U}}(S)}^{\mathsf{d}}}\cong\mathrm{P_{L}}({{S}^{\mathsf{d}}})$* and ${{\mathrm{P_{L}}(S)}^{\mathsf{d}}}\cong\mathrm{P_{U}}({{S}^{\mathsf{d}}})$,* 2. 2.

$\Sigma({{S}^{\mathsf{d}}})\cong\mathrm{P_{U}}(S)$* and ${{\Sigma(S)}^{\mathsf{d}}}\cong\mathrm{P_{L}}(S)$.*

Proof.

Immediate from Lemma 7.1, Lemma 7.2, and Lemma 7.4. ∎

Item 1 of Theorem 7.5 is known: Vickers gave a localic proof using entailment systems [24, Theorem 54], and Goubault-Larrecq proved the corresponding result for stably compact spaces [8, Theorem 3.1]. It is notable, however, that our proof is a simple analysis of axioms of entailment relations.

In the following, compositions such as $\mathrm{P_{U}}(\Sigma(S))$ should be read as $\mathrm{P_{U}}(F(\Sigma(S)))$, where $F\colon\mathsf{SContEnt}\to\mathsf{SProxLat}$ is the functor establishing the equivalence of the two categories (see Remark 5.22).

Proposition 7.6**.**

For any strong proximity lattice $S$, we have

$\mathrm{P_{U}}(\Sigma(S))\cong\Sigma(\mathrm{P_{L}}(S))$, 2. 2.

$\mathrm{P_{U}}(\mathrm{P_{L}}(S))\cong\Sigma(\Sigma(S))$.

Proof.

By Theorem 6.14 and item 2 of Theorem 7.5, we have

[TABLE]

The proof of item 2 is similar. ∎

7.1.2 Double powerlocale

Definition 7.7**.**

The double powerlocale of a locale $X$ is a locale $\mathrm{P_{D}}(X)$ together with a Scott continuous function $i_{D}\colon{\mathrm{\Omega}(X})\to{\mathrm{\Omega}(\mathrm{P_{D}}(X)})$ such that for any Scott continuous function $f\colon{\mathrm{\Omega}(X})\to{\mathrm{\Omega}(Y})$ to a locale $Y$, there exists a unique frame homomorphism $\overline{f}\colon{\mathrm{\Omega}(\mathrm{P_{D}}(X)})\to{\mathrm{\Omega}(Y})$ such that $\overline{f}\circ i_{D}=f$.

Lemma 7.8**.**

For any strong proximity lattice $(S,\prec)$, the double power locale of $\mathrm{Spec}(S)$ can be presented by a strong continuous entailment relation $\mathrm{P_{D}}(S)=(S,\mathrel{\vdash}_{D},\prec)$, where $\mathrel{\vdash}_{D}$ is generated by the following axioms:

[TABLE]

Proof.

By the dcpo version of Proposition 5.5. ∎

Note that $A\mathrel{\vdash}_{D}B\leftrightarrow\exists a\in A\exists b\in B\left(a\leq b\right).$ The construction $(S,\prec)\mapsto\left(S,\mathrel{\vdash}_{D},\prec\right)$ extends to a functor $\mathrm{P_{D}}\colon\mathsf{SProxLat}\to\mathsf{SContEnt}$, which sends each join-preserving proximity relation $r\colon(S,\prec)\to(S^{\prime},\prec^{\prime})$ to a join-preserving proximity map $\mathrm{P_{D}}(r)\colon(S,\mathrel{\vdash}_{D},\prec)\to(S,\mathrel{\vdash}_{D}^{\prime},\prec^{\prime})$ defined by

[TABLE]

Proposition 7.9**.**

For any strong proximity lattice $S$, we have

[TABLE]

Proof.

Immediate from Lemma 7.1 and Lemma 7.8. ∎

We prove some well-known characterisations of the double powerlocale (see Proposition 7.13 and Proposition 7.15). To this end, we begin with the construction of the lower powerlocale of a strong continuous entailment relation.

Given a strong continuous entailment relation $(S,\mathrel{\vdash},\prec)$ define an entailment relation $\mathrel{\vdash}^{L}$ on $\mathsf{Fin}(S)$ by the following axioms:

[TABLE]

Define an idempotent relation $\prec^{L}$ on $\mathsf{Fin}(S)$ by

[TABLE]

Then $(\mathsf{Fin}(S),\mathrel{\vdash}^{L},\prec^{L})$ is a strong continuous entailment relation by Lemma 5.27.

Lemma 7.10**.**

For any $\mathcal{U},\mathcal{V}\in\mathsf{Fin}(\mathsf{Fin}(S))$, we have

[TABLE]

Proof.

By induction on $\mathrel{\vdash}^{L}$, one can show that

[TABLE]

Then, the direction $\Rightarrow$ is obvious from (7.1). Conversely, suppose that there exists $A\in\mathcal{U}$ such that $\forall B\in\mathcal{V}^{*}\left(A\ll_{\mathrel{\vdash}}B\right)$. Then, for each $B\in\mathcal{V}^{*}$, there exists $C_{B}$ such that $A\prec_{U}C_{B}\mathrel{\vdash}B$. Put $C=\bigcup_{B\in\mathcal{U}^{*}}C_{B}$. Then $A\prec_{U}C$ and $C\mathrel{\vdash}B$ for all $B\in\mathcal{V}^{*}$. Hence $\mathcal{U}\mathrel{(\prec^{L})_{U}}\left\{C\right\}\mathrel{\vdash}^{L}\mathcal{V}$ and so $\mathcal{U}\ll_{\mathrel{\vdash}^{L}}\mathcal{V}$. ∎

Lemma 7.11**.**

The strong continuous entailment relation $(\mathsf{Fin}(S),\mathrel{\vdash}^{L},\prec^{L})$ presents the lower powerlocale of $\mathrm{Spec}(F(S,\mathrel{\vdash},\prec))$.

Proof.

From the characterisation of $\ll_{\mathrel{\vdash}^{L}}$ in Lemma 7.10, the entailment system $(\mathsf{Fin}(S),\ll_{\mathrel{\vdash}^{L}})$ coincides with the construction of the lower powerlocale of the entailment system ${(S,\ll_{\mathrel{\vdash}})}$ in Vickers [24, Theorem 53]. ∎

Corollary 7.12**.**

The upper powerlocale of $\mathrm{Spec}(F(S,\mathrel{\vdash},\prec))$ can be presented by a strong continuous entailment relation $(\mathsf{Fin}(S),\mathrel{\vdash}^{U},\prec^{U})$ defined by

[TABLE]

Proof.

We have ${{\mathrm{P_{L}}({{S}^{\mathsf{d}}})}^{\mathsf{d}}}\cong\mathrm{P_{U}}(S)$ by item 2 of Theorem 7.5. The corollary follows by unfolding the definition of ${{\mathrm{P_{L}}({{S}^{\mathsf{d}}})}^{\mathsf{d}}}$ using Lemma 7.10. ∎

For any strong proximity lattice $(S,\prec)$, define a preorder $\leq^{\vee}$ on $\mathsf{Fin}(S)$ by

[TABLE]

Let $S^{\vee}$ be the set $\mathsf{Fin}(S)$ equipped with the equality determined by $\leq^{\vee}$. Define a lattice structure $S^{\vee}\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}(S^{\vee},0^{\vee},\vee^{\vee},1^{\vee},\wedge^{\vee})$ as in (5.4) and an idempotent relation $\prec^{\vee}$ on $S^{\vee}$ by

[TABLE]

Then, $(S^{\vee},\prec^{\vee})$ is a strong proximity lattice, which is isomorphic to $(S,\prec)$ via proximity relations $r\colon(S,\prec)\to(S^{\vee},\prec^{\vee})$ and $s\colon(S^{\vee},\prec^{\vee})\to(S,\prec)$ defined by

[TABLE]

The following is a special case of Vickers [23], which holds for more general context of locally compact locale.111111In [23], $\Sigma(S)$ is expressed as the exponential over the Sierpinski locale.

Proposition 7.13**.**

For any strong proximity lattice $(S,\prec)$, we have

[TABLE]

Proof.

By item 2 of Proposition 7.6, it suffices to show that $\mathrm{P_{D}}(S)\cong\mathrm{P_{U}}(\mathrm{P_{L}}(S))$. By Lemma 7.4 and Corollary 7.12, the locale $\mathrm{P_{U}}(\mathrm{P_{L}}(S))$ is presented by a strong continuous entailment relation $(\mathsf{Fin}(S),\mathrel{\vdash}^{\mathit{UL}},\prec^{\mathit{UL}})$ on $\mathsf{Fin}(S)$ defined by

[TABLE]

As for the strong proximity lattice $(S^{\vee},\prec^{\vee})$ defined above, its double powerlocale $\mathrm{P_{D}}(S^{\vee})=(S^{\vee},\mathrel{\vdash}^{\vee},\prec^{\vee})$ characterised in Lemma 7.8 satisfies

[TABLE]

Clearly, the entailment systems $(S^{\vee},\ll_{\mathrel{\vdash}^{\vee}})$ and $(\mathsf{Fin}(S),\ll_{\mathrel{\vdash}^{\mathit{UL}}})$ are isomorphic. Since $\mathrm{P_{D}}$ is functorial and the embedding $\mathsf{SContEnt_{Prox}}\hookrightarrow\mathsf{Entsys}$ is faithful, we have $\mathrm{P_{D}}(S)\cong\mathrm{P_{D}}(S^{\vee})\cong\mathrm{P_{U}}(\mathrm{P_{L}}(S))$. ∎

Corollary 7.14**.**

For any strong proximity lattice $S$, we have

[TABLE]

Proof.

By Proposition 7.9 and Proposition 7.13. ∎

Proposition 7.15**.**

For any strong proximity lattice $S$, we have

$\mathrm{P_{L}}(\Sigma(S))\cong\Sigma(\mathrm{P_{U}}(S))$, 2. 2.

$\mathrm{P_{L}}(\mathrm{P_{U}}(S))\cong\mathrm{P_{D}}(S)$.

Proof.

1. By Corollary 7.14, and item 2 of Theorem 7.5.

2. Apply item 1 to ${{S}^{\mathsf{d}}}$ and use Theorem 7.5 and Proposition 7.13. ∎

Item 2 of Proposition 7.6 and Proposition 7.15 are known for locally compact locales; see Vickers [23]. Item 1 of Proposition 7.6 and Proposition 7.15 say that the locales of the form $\Sigma(S)$ for a stably compact $S$ is closed under the lower and upper powerlocales. Moreover, the lower and upper powerlocales of $\Sigma(S)$ are obtained by the upper and the lower powerlocales of $S$, respectively.

7.1.3 Vietoris powerlocale

Definition 7.16**.**

Let $(S,\prec)$ be a strong proximity lattice. The Vietoris powerlocale of $\mathrm{Spec}(S)$ is presented by a strong continuous entailment relation $\mathrm{P_{V}}(S)=(S_{V},\mathrel{\vdash}_{V},\prec_{V})$ on the set $S_{V}\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\left\{\Diamond a\mid a\in S\right\}\cup\left\{\Box a\mid a\in S\right\},$ where $\mathrel{\vdash}_{V}$ is generated by the following axioms:

[TABLE]

The idempotent relation $\prec_{V}$ is defined by

[TABLE]

One can easily verify that $\mathrm{P_{V}}(S)$ satisfies the condition in Lemma 5.27. Moreover, it is straightforward to show that the locale presented by $\mathrm{P_{V}}(S)$ is isomorphic to the Vietoris powerlocale of $\mathrm{Spec}(S)$; see Johnstone [11] for the construction of Vietoris powerlocales. Thus, the Vietoris powerlocale of a stably compact locale is stably compact.

The construction $\mathrm{P_{V}}(S)$ extends to a functor $\mathrm{P_{V}}\colon\mathsf{SProxLat}\to\mathsf{SContEnt}$, which sends each join-preserving proximity relation $r\colon(S,\prec)\to(S^{\prime},\prec^{\prime})$ to a join-preserving proximity map $\mathrm{P_{V}}(r)\colon\mathrm{P_{V}}(S)\to\mathrm{P_{V}}(S^{\prime})$ defined by

[TABLE]

where $\Diamond A\Box B\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\left\{\Diamond a\mid a\in A\right\}\cup\left\{\Box b\mid b\in B\right\}$ for each $A,B\in\mathsf{Fin}(S)$.

Theorem 7.17**.**

For any strong proximity lattice $S$, we have

[TABLE]

Proof.

${{\mathrm{P_{V}}(S)}^{\mathsf{d}}}$ and $\mathrm{P_{V}}({{S}^{\mathsf{d}}})$ are identical except that $\Diamond$ and $\Box$ are swapped. ∎

Goubault-Larrecq proved the result corresponding to Theorem 7.17 for stably compact spaces using $\mathbf{A}$-valuations [8, Corollary 5.24].

7.2 Patch topologies

Coquand and Zhang [4] gave a construction of patch topologies for entailment relations with the interpolation property. The same construction carries over to the setting of strong continuous entailment relation.

Definition 7.18** **(Coquand and Zhang [4, Section

4]).

Given a strong continuous entailment relation $(S,\mathrel{\vdash},\prec)$, the patch topology of $S$ is a strong continuous entailment relation $\mathrm{Patch}(S)=(S_{P},\mathrel{\vdash}_{P},\prec_{P})$ on the set $S_{P}\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}S\cup\left\{{a}^{\circ}\mid a\in S\right\},$ where $\mathrel{\vdash}_{P}$ is generated by the following axioms:

[TABLE]

The idempotent relation $\prec_{P}$ is defined by

[TABLE]

Let $\mathrm{Patch^{\prime}}(S)=(S_{P},\mathrel{\vdash}_{P}^{\prime},\prec_{P})$ be the strong continuous entailment relation which is obtained from $\mathrm{Patch}(S)$ by adjoining the following axioms:

[TABLE]

where ${A}^{\circ}\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\left\{{a}^{\circ}\mid a\in A\right\}$ for each $A\in\mathsf{Fin}(S)$.

Proposition 7.19**.**

For any strong continuous entailment relation $(S,\mathrel{\vdash},\prec)$, we have

[TABLE]

Proof.

We show that the entailment systems associated with $\mathrm{Patch^{\prime}}(S)$ and $\mathrm{Patch}(S)$ coincide, i.e., $\ll_{\mathrel{\vdash}_{P}}{=}\ll_{\mathrel{\vdash}_{P}^{\prime}}$. Since $\mathrel{\vdash}_{P}^{\prime}$ is generated by the extra axioms, we have $\ll_{\mathrel{\vdash}_{P}}\mathop{\subseteq}\ll_{\mathrel{\vdash}_{P}^{\prime}}$. To prove the converse inclusion, it suffices to show that

[TABLE]

This is proved by induction on the derivation of $X\mathrel{\vdash}_{P}^{\prime}Y$ (see Lemma 5.25). The case $(\mathrm{R^{\prime}})$ is obvious, so it suffices to check the case $(\mathrm{AxL})$ for each axiom of $\mathrm{Patch}(S^{\prime})$. We only deal with (7.5). Suppose that ${{B}^{\mathsf{\circ}}},X\mathrel{\vdash}_{P}^{\prime}Y$ is derived from ${{B}^{\mathsf{\circ}}}\mathrel{\vdash}_{P}^{\prime}{{A}^{\mathsf{\circ}}}$ and $\forall a\in A\left(X,{{a}^{\mathsf{\circ}}}\mathrel{\vdash}_{P}^{\prime}Y\right)$ where $A\mathrel{\vdash}B$. Let $Z\left(\prec_{P}\right)_{U}{{B}^{\mathsf{\circ}}},X$. Then, there exists $C\in\mathsf{Fin}(S)$ such that ${{C}^{\mathsf{\circ}}}\subseteq Z$ and $B\prec_{L}C$, and so there exists $C^{\prime}$ such that $B\prec_{L}C^{\prime}\prec_{L}C$. Thus, there exists $D$ such that $A\prec_{U}D\mathrel{\vdash}C^{\prime}$ by (5.5). For each $d\in D$, there exist $a\in A$ and $d^{\prime}$ such that $a\prec d^{\prime}\prec d$. Then, $Z,{{d^{\prime}}^{\mathsf{\circ}}}\left(\prec_{P}\right)_{U}X,{{a}^{\mathsf{\circ}}}$ so $Z,{{d^{\prime}}^{\mathsf{\circ}}}\ll_{\mathrel{\vdash}_{P}}Y$ by induction hypothesis. Thus, for each $d\in D$, there exist $d^{\prime}\prec d$ and $W_{d}\in\mathsf{Fin}(S)$ such that $Z,{{d^{\prime}}^{\mathsf{\circ}}}\mathrel{\vdash}_{P}W_{d}\left(\prec_{P}\right)_{L}Y$ so that $Z\mathrel{\vdash}_{P}W_{d},d$ by (7.4). Since $D\mathrel{\vdash}C^{\prime}\prec_{L}C$, we get $Z,{{C}^{\mathsf{\circ}}}\mathrel{\vdash}_{P}\bigcup_{d\in D}W_{d}$ by (7.2) and successive applications of $(\mathrm{T})$ and (7.3). Hence, $Z=Z\cup{{C}^{\mathsf{\circ}}}\ll_{\mathrel{\vdash}_{P}}Y$. ∎

In terms of $\mathsf{SContEnt}$, we have proximity maps $r\colon\mathrm{Patch}(S)\to\mathrm{Patch^{\prime}}(S)$ and $s\colon\mathrm{Patch^{\prime}}(S)\to\mathrm{Patch}(S)$ defined by

[TABLE]

which are inverse to each other.

Theorem 7.20**.**

For any strong continuous entailment relation $S$, we have

[TABLE]

Proof.

By Proposition 7.19, we may identify $\mathrm{Patch}(S)$ with $\mathrm{Patch^{\prime}}(S)$. Then, we have $\mathrm{Patch^{\prime}}(S)\cong\mathrm{Patch^{\prime}}({{S}^{\mathsf{d}}})$ by exchanging the roles of $a$ and ${a}^{\circ}$. ∎

Remark 7.21*.*

Combining $\mathrm{Patch}$ and the equivalence between $\mathsf{SProxLat_{Perf}}$ and $\mathsf{SContEnt_{Perf}}$, we get a functor $\mathrm{Patch}\colon\mathsf{SProxLat_{Perf}}\to\mathsf{SContEnt_{Perf}}$, which sends an adjoint pair $(s,r)$ of proximity relations $r\colon(S,\prec)\to(S^{\prime},\prec^{\prime})$ and $s\colon{(S^{\prime},\prec^{\prime})}\to{(S,\prec)}$ to an adjoint pair $(\mathfrak{P}(s),\mathfrak{P}(r))$ of proximity maps $\mathfrak{P}(r)\colon{\mathrm{Patch}(G(S))}\to\mathrm{Patch}(G(S^{\prime}))$ and $\mathfrak{P}(s)\colon\mathrm{Patch}(G(S^{\prime}))\to\mathrm{Patch}(G(S))$ defined by

[TABLE]

7.3 Space of valuations

The space of valuations is a localic analogue of the probabilistic power domain by Jones and Plotkin [13, 14]. We first recall several notions of real numbers which are needed for its definition.

A lower real is a rounded downward closed subset of rationals $\mathbb{Q}$. 2. 2.

An upper real is a rounded upward closed subset of $\mathbb{Q}$. 3. 3.

A Dedekind real is a disjoint pair $(L,U)$ of an inhabited lower real $L$ and an inhabited upper real $U$ which is located: $p<q$ implies $p\in L$ or $q\in U$.

Let $\overrightarrow{[0,\infty]}$ and $\overleftarrow{[0,\infty]}$ denote the lower and the upper reals greater than [math] respectively (including infinity). We follow Vickers [25, Section 4 and Section 6] for the definition of spaces of valuations and covaluations.

Definition 7.22**.**

A valuation on a locale $X$ is a Scott continuous function $\mu\colon{\mathrm{\Omega}(X})\to\overrightarrow{[0,\infty]}$ satisfying

[TABLE]

where the second condition is called the modular law. A covaluation is a Scott continuous function $\nu\colon{\mathrm{\Omega}(X})\to\overleftarrow{[0,\infty]}$ satisfying $\nu(1)=0$ and the modular law. The space of valuations $\mathfrak{V}(X)$ on a locale $X$ is the locale whose models are valuations on $X$. The space of covaluations $\mathfrak{C}(X)$ is defined similarly.

For a strong proximity lattice $(S,\prec)$, the locale $\mathfrak{V}(\mathrm{Spec}(S))$ is presented by a geometric theory $T_{\mathfrak{V}}$ over the set

[TABLE]

with the following axioms:

[TABLE]

A model $\alpha$ of $T_{\mathfrak{V}}$ determines a valuation $\mu_{\alpha}\colon\mathrm{RIdl}(S)\to\overrightarrow{[0,\infty]}$ by

[TABLE]

Conversely, a valuation $\mu\colon\mathrm{RIdl}(S)\to\overrightarrow{[0,\infty]}$ determines a model $\alpha_{\mu}$ of $T_{\mathfrak{V}}$ by

[TABLE]

The locale $\mathfrak{C}(\mathrm{Spec}(S))$ is presented by a geometric theory $T_{\mathfrak{C}}$ obtained from $T_{\mathfrak{V}}$ by replacing the first three and the last two axioms with the following:

[TABLE]

It is straightforward to show that $\mathfrak{V}(\mathrm{Spec}(S))$ and $\mathfrak{C}(\mathrm{Spec}(S))$ are isomorphic to the spaces of valuations and covaluations in Vickers [25, Section 4 and Section 6].

The following lemma allows us to present the space of valuations on $\mathrm{Spec}(S)$ by a strong continuous entailment relation.

Lemma 7.23**.**

Under the other axioms of $T_{\mathfrak{V}}$ (or $T_{\mathfrak{C}}$), the axioms

[TABLE]

are equivalent to the following axioms:

[TABLE]

Here, the equivalence of two axioms means that one axiom holds in the locale presented by the other axiom and the rest of the axioms of $T_{\mathfrak{V}}$ (or $T_{\mathfrak{C}}$).

Proof.

The proof is inspired by Coquand and Spitters [3, Lemma 2], which we elaborate below. We identify generators $S_{\mathfrak{V}}$ with the corresponding elements of $\mathrm{Sp}(T_{\mathfrak{V}})$ (or the locale presented by (7.8) and (7.9) in place of (7.6) and (7.7)). We write $\leq_{\mathfrak{V}}$ for the orders in these locales.

First, assume (7.6). Let $p,q,r,s\in\mathbb{Q}$ such that $p+q=r+s$. Take any $p^{\prime},q^{\prime}\in\mathbb{Q}$ such that $p^{\prime}+q^{\prime}=p+q$. If $p^{\prime}\geq r$, then $\langle p^{\prime},a\wedge b\rangle\leq_{\mathfrak{V}}\langle r,a\wedge b\rangle$. If $p^{\prime}<r$, then $q^{\prime}=s+(r-p^{\prime})$, and thus $\langle q^{\prime},a\vee b\rangle\leq_{\mathfrak{V}}\langle s,a\vee b\rangle$. Hence

[TABLE]

for all $p^{\prime},q^{\prime}\in\mathbb{Q}$ such that $p^{\prime}+q^{\prime}=p+q$. Applying (7.6), we obtain (7.8). Similarly, we obtain (7.9) from (7.7).

Conversely, assume (7.8). By the last two axioms of $T_{\mathfrak{V}}$, we have

[TABLE]

Let $q^{\prime},r^{\prime}\in\mathbb{Q}$ such that $q^{\prime}+r^{\prime}>q+r$. Let $\theta\in\mathbb{Q}$ such that $q^{\prime}+r^{\prime}=q+r+\theta$, and choose $N\in\mathbb{N}$ so large that $q+r+\theta-N\theta<0$. By (7.8), we have

[TABLE]

for all $n\in\mathbb{N}$. For each $n\in\mathbb{N}$, define

[TABLE]

Then, we have

[TABLE]

where $\mathsf{Ch}(N+1)$ is the set of choice functions $f\colon\left\{0,\dots,N+1\right\}\to\{0,1\}$. For each $f\in\mathsf{Ch}(N+1)$, one of the following cases occurs:

Case 1: $\forall n\leq N+1\,f_{n}=0$. Since $-\theta<0$, we have

[TABLE]

Case 2: $\forall n\leq N+1\,f_{n}=1$. Since $q+r+\theta-N\theta<0$, we have

[TABLE]

Case 3: $\exists n\leq N\,f_{n}=0\>\&\>f_{n+1}=1$.

[TABLE]

Case 4: $\exists n\leq N\,f_{n}=1\>\&\>f_{n+1}=0$.

[TABLE]

Thus, in any case

[TABLE]

Hence, by (7.11) and (7.10), we have (7.6). Similarly, (7.9) implies (7.7). ∎

Proposition 7.24**.**

For any strong proximity lattice $(S,\prec)$, the locale $\mathfrak{V}(\mathrm{Spec}(S))$ can be presented by a strong continuous entailment relation $\mathfrak{V}(S)={(S_{\mathfrak{V}},\mathrel{\vdash}_{\mathfrak{V}},\prec_{\mathfrak{V}})}$ where $\mathrel{\vdash}_{\mathfrak{V}}$ is generated by the following axioms:

[TABLE]

The idempotent relation $\prec_{\mathfrak{V}}$ is defined by

[TABLE]

The locale $\mathfrak{C}(\mathrm{Spec}(S))$ can be presented by a strong continuous entailment relation $\mathfrak{C}(S)=(S_{\mathfrak{V}},\mathrel{\vdash}_{\mathfrak{C}},\prec_{\mathfrak{C}})$ where $\mathrel{\vdash}_{\mathfrak{C}}$ is generated by the following axioms:

[TABLE]

The idempotent relation $\prec_{\mathfrak{C}}$ is defined by

[TABLE]

In particular, the spaces of valuations and covaluations on a stably compact locale are stably compact.

Proof.

One can check that $\mathfrak{V}(S)$ and $\mathfrak{C}(S)$ satisfy the condition in Lemma 5.27. Then, the claim of the proposition follows from Lemma 7.23. ∎

The constructions $\mathfrak{V}(S)$ and $\mathfrak{C}(S)$ extend to functors $\mathfrak{V}\colon\mathsf{SProxLat}\to\mathsf{SContEnt}$ and $\mathfrak{C}\colon\mathsf{SProxLat}\to\mathsf{SContEnt}$, which send each join-preserving proximity relation $r\colon(S,\prec)\to(S^{\prime},\prec^{\prime})$ to join-preserving proximity maps $\mathfrak{V}(r)\colon\mathfrak{V}(S)\to\mathfrak{V}(S^{\prime})$ and $\mathfrak{C}(r)\colon\mathfrak{C}(S)\to\mathfrak{C}(S^{\prime})$ defined by

[TABLE]

Theorem 7.25**.**

For any strong proximity lattice $S$, we have

[TABLE]

Proof.

Immediate from Proposition 7.24 and Lemma 7.1. ∎

We now focus on probabilistic valuations and covaluations, i.e., those valuations $\mu$ and covaluations $\nu$ satisfying $\mu(1)=1$ and $\nu(0)=1$.

For a strong proximity lattice $(S,\prec)$, the space $\mathfrak{V_{P}}(\mathrm{Spec}(S))$ of probabilistic valuations is presented by a geometric theory $T_{\mathfrak{V_{P}}}$ which extends the theory $T_{\mathfrak{V}}$ with the following extra axioms:

[TABLE]

The space $\mathfrak{C_{P}}(\mathrm{Spec}(S))$ of probabilistic covaluations is presented by a geometric theory $T_{\mathfrak{C_{P}}}$ which extends the theory $T_{\mathfrak{C}}$ with the following extra axioms:

[TABLE]

Proposition 7.24 restricts to probabilistic valuations and covaluations.

Proposition 7.26**.**

For any strong proximity lattice $(S,\prec)$, the locale $\mathfrak{V_{P}}(\mathrm{Spec}(S))$ can be presented by a strong continuous entailment relation $\mathfrak{V_{P}}(S)={(S_{\mathfrak{V}},\mathrel{\vdash}_{\mathfrak{V_{P}}},\prec_{\mathfrak{V}})}$ where $\mathrel{\vdash}_{\mathfrak{V_{P}}}$ is generated by the axioms of $\mathrel{\vdash}_{\mathfrak{V}}$ and the following extra axioms:

[TABLE]

The locale $\mathfrak{C_{P}}(\mathrm{Spec}(S))$ can be presented by a strong continuous entailment relation $\mathfrak{C_{P}}(S)=(S_{\mathfrak{V}},\mathrel{\vdash}_{\mathfrak{C_{P}}},\prec_{\mathfrak{C}})$ where $\mathrel{\vdash}_{\mathfrak{C_{P}}}$ is generated by the axioms of $\mathrel{\vdash}_{\mathfrak{C}}$ and the following extra axioms:

[TABLE]

In particular, the spaces of probabilistic valuations and probabilistic covaluations on a stably compact locale are stably compact. ∎

As a corollary we obtain the probabilistic version of Theorem 7.25.

Theorem 7.27**.**

For any strong proximity lattice $S$, we have

[TABLE]

∎

For probabilistic valuations and covaluations, we have the following duality.

Lemma 7.28**.**

For any strong proximity lattice $S$, we have

[TABLE]

for all $A,B\in\mathsf{Fin}(S_{\mathfrak{V}})$, where ${{A}^{\mathsf{\bullet}}}\stackrel{{\scriptstyle\textup{def}}}{{\ =\ }}\left\{\langle 1-p,a\rangle\mid\langle p,a\rangle\in A\right\}.$

Proof.

The direction $\Rightarrow$ is proved by induction on the derivation of $A\mathrel{\vdash}_{\mathfrak{V_{P}}}B$. Note that each axiom $A\mathrel{\vdash}_{\mathfrak{V_{P}}}B$ of $\mathfrak{V_{P}}(S)$ corresponds to an axiom ${{A}^{\mathsf{\bullet}}}\mathrel{\vdash}_{\mathfrak{C_{P}}}{{B}^{\mathsf{\bullet}}}$ of $\mathfrak{C_{P}}(S)$. The direction $\Leftarrow$ is similarly proved by induction on ${{A}^{\mathsf{\bullet}}}\mathrel{\vdash}_{\mathfrak{C_{P}}}{{B}^{\mathsf{\bullet}}}$. ∎

Since “$1$” in the lower and upper reals form a Dedekind real, the following proposition is analogous to Vickers [25, Proposition 6.3], which holds for an arbitrary locale. We give a proof for the special case of stably compact locales.

Proposition 7.29**.**

For any strong proximity lattice $S$, we have

[TABLE]

Proof.

Define proximity maps $r\colon\mathfrak{V_{P}}(S)\to\mathfrak{C_{P}}(S)$ and $s\colon\mathfrak{C_{P}}(S)\to\mathfrak{V_{P}}(S)$ by

[TABLE]

Using Lemma 7.28, it is straightforward to show that $r$ and $s$ are indeed proximity maps which are inverse to each other. ∎

Theorem 7.30**.**

For any strong proximity lattice $S$, we have

[TABLE]

Proof.

By Theorem 7.27 and Proposition 7.29. ∎

Goubault-Larrecq [8, Theorem 6.11] proved the corresponding result for stably compact spaces. Although his proof is classical and the space of covaluations is implicit in his proof, the essential idea seems to be similar.

Acknowledgements

I thank the referees for numerous suggestions which help me improve the paper in an essential way. In particular, their suggestion to use entailment systems allows me to simplify and constructivise many parts of the paper. I also thank Steve Vickers and Daniel Wessel for helpful discussions. This work was carried out while I was in the Hausdorff Research Institute for Mathematics (HIM), University of Bonn, for their trimester program “Types, Sets and Constructions” (May–August 2018). I thank the institute for their support and the organisers of the program for creating a stimulating environment for research.