Pervin spaces and Frith frames: bitopological aspects and completion

TL;DR

This paper explores the bitopological and categorical structures of Pervin spaces and Frith frames, establishing dualities and characterizations that extend classical topological dualities into a pointfree and quasi-uniform context.

Contribution

It provides a categorical equivalence between zero-dimensional complete Pervin spaces and complete Frith frames, extending Stone-type dualities and characterizations to this setting.

Findings

Categorical equivalences involving zero-dimensional structures

Duality between $T_0$ complete Pervin spaces and complete Frith frames

Analogues of Banaschewski and Pultr's characterizations in this context

Abstract

A Pervin space is a set equipped with a bounded sublattice of its powerset, while its pointfree version, called Frith frame, consists of a frame equipped with a generating bounded sublattice. It is known that the dual adjunction between topological spaces and frames extends to a dual adjunction between Pervin spaces and Frith frames, and that the latter may be seen as representatives of certain quasi-uniform structures. As such, they have an underlying bitopological structure and inherit a natural notion of completion. In this paper we start by exploring the bitopological nature of Pervin spaces and of Frith frames, proving some categorical equivalences involving zero-dimensional structures. We then provide a conceptual proof of a duality between the categories of $T_0$ complete Pervin spaces and of complete Frith frames. This enables us to interpret several Stone-type dualities as a restriction of the dual adjunction between Pervin spaces and Frith frames along full subcategory embeddings. Finally, we provide analogues of Banaschewski and Pultr's characterizations of sober and $T_D$ topological spaces in the setting of Pervin spaces and of Frith frames, highlighting the parallelism between the two notions.

Equations

$$a\wedge \underset{i\in I}{\bigvee }{b}_i=\underset{i\in I}{\bigvee }(a\wedge b_i).$$

$$a\to b=\bigvee \{x\in L\mid x\wedge a\le b\},$$

$$h(a\to b)\le h(a)\to h(b),$$

$$a\to h_{\ast }(x)=h_{\ast }(h(a)\to x)$$

$${\nabla }_a:=\{(x,y)\in L\times L\mid a\vee x=a\vee y\}\text{and}{\Delta }_a:=\{(x,y)\in L\times L\mid a\wedge x=a\wedge y\}.$$

$$c_{(L,S)}:(\mathrm{Idl}(S),S)\to (L,S),J\mapsto \bigvee J.$$

$${\Phi }_D:D\to \mathcal{P}(\mathrm{pf}(D)),a\mapsto \tilde{a}:=\{F\in \mathrm{pf}(D)\mid a\in F\}.$$

$${\mathcal{N}}_{(X,\mathcal{S})}:(X,\mathcal{S})\to (\mathrm{pf}(\mathcal{S}),\tilde{\mathcal{S}}),x\mapsto \{S\in \mathcal{S}\mid x\in S\}.$$

$${\mathbf{Sk}}_{\mathrm{Pervin}}\circ {\mathbf{Clop}}_{+}(\mathcal{X})=(X,{\Omega }_{{\mathrm{Clop}}_{+}(\mathcal{X})}(X),{\Omega }_{{\mathrm{Clop}}_{-}(\mathcal{X})}(X)).$$

$${\eta }_{\mathcal{X}}:(X,{\tau }_{+},{\tau }_{-})\to (X,{\Omega }_{{\mathrm{Clop}}_{+}(\mathcal{X})}(X),{\Omega }_{{\mathrm{Clop}}_{-}(\mathcal{X})}(X))$$

$${\epsilon }_{(X,\mathcal{S})}:(X,[\mathcal{S}{]}_{op})\to (X,\mathcal{S})$$

$${\mathbf{Sk}}_{\mathrm{Pervin}}\circ {\mathbf{Clop}}_{+}\circ {\mathbf{Sk}}_{\mathrm{Pervin}}(X,\mathcal{S})$$

$$={\mathbf{Sk}}_{\mathrm{Pervin}}(X,\mathcal{S}),$$

$$\overline{h}[\nabla L]=\nabla h[L]\text{and}\overline{h}[\Delta S]=\Delta h[S].$$

$${\eta }_{(L,S)}:(L,S)\to {\mathbf{B}}_{+}\circ {\mathbf{Sk}}_{\mathrm{Frith}}(L,S).$$

$${\eta }_{(L,S)}:(L,S)\to (\nabla L,\{{\nabla }_a\mid a\in [S{]}_{se}\}),a\mapsto {\nabla }_a.$$

$${\beta }_{(L,S)}:{\mathbf{Sk}}_{\mathrm{Pervin}}\circ \mathbf{pt}(L,S)\to {\mathbf{pt}}_b\circ {\mathbf{Sk}}_{\mathrm{Frith}}(L,S),p\mapsto \tilde{p}$$

$$p\in {\beta }_{(L,S)}^{-1}(\widehat{{\nabla }_a})⟺\tilde{p}({\nabla }_a)=1⟺p(a)=1⟺p\in \hat{a}.$$

$$\tilde{p}\circ {\mathbf{Sk}}_{\mathrm{Frith}}(h)({\nabla }_x)=\tilde{p}({\nabla }_{h(x)})=p\circ h(x)=\widetilde{p\circ h}({\nabla }_x).\text{qed}$$

$${\mathbf{U}}_{\mathrm{Pervin}}^{\prime }(X,\mathcal{S})=(X,{\Omega }_{\mathcal{S}}(X))\text{ and }{\mathbf{U}}_{\mathrm{Frith}}^{\prime }(L,S)=L.$$

$$\mathbf{\Omega }(X,\mathcal{S})=\mathbf{\Omega }\circ \mathbf{pt}(\mathrm{Idl}(\mathcal{S}),\mathcal{S})\cong (\mathrm{Idl}(\mathcal{S}),\mathcal{S}),$$

$$x\leq_{{\mathcal{S}}}y\mbox{ if and only if $x\in S$ implies $y\in S$ for all $S\in{\mathcal{S}}$,}$$

$$\mathbf{Priest}\stackrel{\mathbf{CUp}}{\to }\mathbf{CPervin}\stackrel{{\mathbf{U}}_{\mathrm{Pervin}}}{\to }\mathbf{Spec}\text{ and }\mathbf{Spec}\stackrel{\mathbf{P}}{\to }\mathbf{CPervin}\stackrel{\mathbf{KO}}{\to }\mathbf{Priest}$$

$$X=(\bigcap _{i\in I}{S}_i{)}^c\cup (\bigcap _{i\in I}{S}_i)=\bigcup _{i\in I}{S}_i^c\cup \bigcup _{j\in J}{S}_j^{\prime }$$

$$\forall T_1,T_2\in \mathcal{T},f^{-1}(T_1)\subseteq f^{-1}(T_2)⟹T_1\subseteq T_2,$$

$$\forall T_1,T_2\in \mathcal{T},f^{-1}(T_1\cap T_2^c)=\varnothing ⟹T_1\cap T_2^c=\varnothing .$$

$$a=\bigwedge \{b\to s\mid b\in L,s\in S,\text{ and }a\le b\to s\}.$$

$$h_{\ast }\circ h(a)$$

$$\le h_{\ast }(h(b)\to h(s))\text{(by eqrefeq:1 and because h∗ is order-preserving)}$$

$$=b\to h_{\ast }\circ h(s)\text{(by eqrefeq:2)}$$

$$=b\to s\text{(by Lemma refl:13)}.$$

Full text

Mathematics Subject Classification (2020): 06D22, 54E55, 06D50

Keywords: Pervin space, Frith frame, bitopogical space, biframe, completion

1 Introduction

The category of Pervin spaces is introduced in [10, 18] as an isomorph of the category of transitive and totally bounded quasi-uniform spaces. Its pointfree analogue, whose objects are named Frith frames, was later defined in [7]. In this setting, we have a full embedding of the category of Frith frames in that of transitive and totally bounded quasi-uniform frames, which is a coreflection but not an equivalence. It is also shown in [7] that the classical dual adjunction between topological spaces and frames naturally extends to a dual adjunction between Pervin spaces and Frith frames. In fact, this is what justifies calling Frith frames the pointfree version of Pervin spaces.

Since both Pervin spaces and Frith frames may be seen as quasi-uniform structures, they come equipped with an underlying bitopological structure as well [9, Chapter 3]. The study of such bitopological structure is the main content of Section 3. In Section 3.1, we start by assigning a bitopological space to each Pervin space, and show that this is a functorial assignment with a left adjoint. When studying the categorical equivalence induced by such adjunction, strong exactness (for Pervin spaces) and zero-dimensionality (for bitopological spaces) appear as crucial concepts. More precisely, we show that the categories of the so-called strongly exact Pervin spaces and of zero-dimensional bitopological spaces are equivalent. We then consider the pointfree version of these results and show that strongly exact Frith frames are a full coreflective subcategory of the category of zero-dimensional biframes, leaving as an open problem to describe the underlying categorical equivalence. Noting that topological spaces and frames may be seen as bitopological spaces and biframes, respectively, in Section 3.2, we specialize the results of the previous section in the monotopological setting. In particular, we show that the categories of zero-dimensional topological spaces and of strongly exact symmetric Pervin spaces are equivalent, and so are those of zero-dimensional frames and of strongly exact symmetric Frith frames.

As representatives of quasi-uniform structures, Pervin spaces and Frith frames also inherit natural notions of completeness. It is observed in [18] that $T_{0}$ and complete Pervin spaces can be identified with spectral spaces, while in [7] it is shown that complete Frith frames can be identified with bounded distributive lattices. In particular, thanks to Stone duality for bounded distributive lattices, it follows that the categories of $T_{0}$ and complete Pervin spaces and of complete Frith frames are dual to each other. In Section 4, we provide a direct and conceptual proof of this duality, which is based on a characterization of complete Pervin spaces and of complete Frith frames, and does not invoke Stone duality. On the other hand, since the categories of $T_{0}$ complete Pervin spaces and of complete Frith frames are full subcategories of the categories of Pervin spaces and of Frith frames, respectively, we may then see Stone duality as a restriction of the Pervin-Frith dual adjunction along full subcategory embeddings (unlike what happens when seeing it as a restriction of the dual adjunction between topological spaces and frames). In Section 5, we exhibit several Stone-type dualities as suitable restrictions of the dual adjunction along full subcategory embeddings. Section 5.1 is devoted to the already mentioned Stone duality, Section 5.2 to Priestley duality, and Section 5.3 to bitopological duality. In Section 5.4, we provide the global picture of the results thus obtained. It is our concern in Sections 4 and 5 to point out where the assumption of the Prime Ideal Theorem is needed.

Finally, in Section 6, starting from Banaschewski and Pultr’s characterizations of sober and $T_{D}$ topological spaces [5, Proposition 4.3], which highlights the parallelism between the two notions, we state and prove analogous results for Pervin spaces, where sober is replaced by complete and $T_{D}$ by Pervin-$T_{D}$ (the latter notion having been introduced in [7, Section 4.5]). When looking for a pointfree version of such results, we are naturally led to consider the notion of locale-based Frith frame, which will replace Pervin-$T_{D}$ in our statement.

We readily warn the reader that, although we implicitly have in mind the quasi-uniform interpretation of Pervin spaces and of Frith frames (namely, when considering their bitopological nature and the property of being complete), we will avoid mentioning quasi-uniformities throughout the paper. This reduces the amount of background required from the reader, leaving the details of existing connections for those already familiar with quasi-uniformities. For a detailed study of Pervin spaces, Frith frames, and corresponding quasi-uniform structures, we refer to [7, 10, 18].

2 Preliminaries

The material in this section is presented mostly to set up the notation. We assume the reader to be familiar with frame and locale theory.

2.1 Basic notation

The content of this section may be found in [12, 17].

A frame is a complete lattice $L$ such that for every $a\in L$ and $\{b_{i}\}_{i\in I}\subseteq L$ the following distributivity law holds:

[TABLE]

A frame $L$ is always a complete Heyting algebra, with the Heyting implication given by

[TABLE]

for every $a,b\in L$. The element $a\to 0$, called the pseudocomplement of $a$, will be denoted by $a^{*}$. When $a\vee a^{*}=1$, we say that $a$ is complemented and $a^{*}$ is the complement of $a$. A frame homomorphism is a map $h:L\to M$ that preserves finite meets and arbitrary joins. We will denote by ${\bf Frm}$ the category of frames and frame homomorphisms. A frame homomorphism $h:L\to M$ is dense provided $h(a)=0$ implies $a=0$. In general, a frame homomorphism need not preserve the Heyting implication. We have however the following:

[TABLE]

for every $a,b\in L$. Moreover, since every frame homomorphism $h$ preserves arbitrary joins, it has a right adjoint $h_{*}$, and the equality

[TABLE]

holds, for every $a\in L$ and $x\in M$. This is usually called the Frobenius identity.

We say that an element $a\in L$ is compact if whenever $a\leq\bigvee_{i\in I}a_{i}$ there exists a finite subset $I^{\prime}\subseteq I$ such that $a\leq\bigvee_{i\in I^{\prime}}a_{i}$. A frame $L$ is compact if its top element is compact. If the set of compact elements of $L$ is closed under finite meets and join-generates $L$, then we say that $L$ is coherent. A frame $L$ is zero-dimensional if it is join-generated by its sublattice of complemented elements.

The opposite category of ${\bf Frm}$, is usually denoted by $\bf Loc$. Its objects are called locales, and morphisms $h:L\to M$ are the right adjoints of the corresponding frame maps. Locales will only be mentioned in Section 6. For our purposes, the notion of sublocale will be enough. A sublocale of $L$ is a subset $K\subseteq L$ that is closed under arbitrary joins and contains every element of the form $a\to x$, with a $a\in L$ and $x\in K$. A sublocale $K$ is itself a frame, but not a subframe of $L$, as joins may be computed differently. Every sublocale is uniquely determined by a frame quotient $q:L\twoheadrightarrow K$ whose right adjoint is the localic embedding $K\hookrightarrow L$. In particular, $q(x)=x$, whenever $x\in K$.

Since sublocales correspond to frame quotients, these may also be defined via frame congruences, which will be widely used throughout the paper. The set ${\mathcal{C}}L$ of all frame congruences on $L$ is itself a frame when ordered by inclusion. For every element $a\in L$, we may define two congruences:

[TABLE]

Congruences of the form $\nabla_{a}$ are called closed, while those of the form $\Delta_{a}$ are open. Open and closed congruences suffice to generate ${\mathcal{C}}L$, as a frame. The functions $\nabla:a\mapsto\nabla_{a}$ and $\Delta:a\mapsto\Delta_{a}$ from $L$ to ${\mathcal{C}}L$ are, respectively, a frame embedding and an injection that turns finite meets into finite joins and arbitrary joins to arbitrary meets. Given a subset $S\subseteq L$, we denote by $\nabla S$ and by $\Delta S$ the subframes of ${\mathcal{C}}L$ generated by $\{\nabla_{s}\mid s\in S\}$ and by $\{\Delta_{s}\mid s\in S\}$, respectively. The subframe of ${\mathcal{C}}L$ generated by $\nabla L\cup\Delta S$ will be denoted by ${\mathcal{C}}_{S}L$. The following generalizes the well-known universal property of the congruence frame.

Proposition 2.1** ([23, Theorem 16.2]).**

For every frame $L$ and subset $S\subseteq L$, the frame ${\mathcal{C}}_{S}L$ has the following universal property: whenever $h:L\rightarrow M$ is a frame map such that $h(s)$ is complemented for all $s\in S$, there is a unique frame homomorphism $\widetilde{h}:{\mathcal{C}}_{S}L\rightarrow M$ making the following diagram commute.

L$${\mathcal{C}}_{S}L$$M$$\nabla$$\widetilde{h}$$h

Finally, we have an idempotent adjunction $\bf\Omega:{\bf Top}\leftrightarrows{\bf Frm}^{op}:{\bf pt}$ between the category ${\bf Top}$ of topological spaces and continuous functions and the category opposite to ${\bf Frm}$. Given a topological space $(X,\tau)$ (or simply $X$ if no confusion arises), ${\bf\Omega}(X)$ is the frame $\Omega(X)$ consisting of the open subsets of $X$ (ordered by $\subseteq$) and, for a continuous function $f:X\to Y$, ${\bf\Omega}(f)=f^{-1}$ is the preimage frame homomorphism. In the other direction, given a frame $L$, ${\bf pt}(L)$ is the set ${\rm pt}(L)$ of points of $L$ (here seen as frame homomorphisms $p:L\to{\bf 2}$) equipped with the topology $\widehat{L}:=\{\widehat{a}\mid a\in L\}$, where $\widehat{a}:=\{p\in{\rm pt}(L)\mid p(a)=1\}$, and given a frame homomorphism $h:L\to M$, ${\bf pt}(h)$ maps $p\in{\rm pt}(M)$ to $p\circ h\in{\rm pt}(L)$. The fixpoints of ${\bf\Omega}\dashv{\bf pt}$ are the so-called sober spaces and spatial frames, respectively.

2.2 Bitopological spaces and biframes

We refer to [20] and to [4, 21] for further reading on bitopological spaces and on biframes, respectively.

A bitopological space, or bispace, is a triple ${\mathcal{X}}=(X,\tau_{+},\tau_{-})$, where $X$ is a set and $\tau_{+}$ and $\tau_{-}$ two topologies on that set. Morphisms between bitopological spaces are functions between their underlying sets that are continuous with respect to both topologies. We denote by ${\bf BiTop}$ the category thus obtained. The topology $\tau_{+}\vee\tau_{-}$ on $X$ generated by $\tau_{+}\cup\tau_{-}$ is called the patch topology. We call $\tau_{+}$ the positive topology, and $\tau_{-}$ the negative one. Accordingly, elements of $\tau_{+}$ are called positive opens, and a positive open whose complement is a negative one is called a positive clopen. The collection of positive clopen subsets of $X$ will be denoted by ${\rm Clop}_{+}({\mathcal{X}})$. Negative (cl)opens and ${\rm Clop}_{-}({\mathcal{X}})$ are defined similarly, in the obvious way.

We say that a bispace is $T_{0}$ (respectively, compact) if its patch topology is $T_{0}$ (respectively, compact). We say that a bispace $(X,\tau_{+},\tau_{-})$ is zero-dimensional if every element in $\tau_{+}$ is a union of positive clopens, and every element in $\tau_{-}$ is a union of negative clopens.444These notions are not consistent over all the literature. For instance, in [6] our notions of $T_{0}$ and compact are named join $T_{0}$ and join compact, respectively, while compact is named pairwise compact in [20]. Moreover, in [19, 6] our notion of zero-dimensional is named pairwise zero-dimensional.

A biframe is a triple ${\mathcal{L}}=(L,\,L_{+},\,L_{-})$ such that all three components are frames, together with subframe inclusions $L_{+}\subseteq L$ and $L_{-}\subseteq L$, and such that every element of $L$ is a join of finite meets of elements of $L_{+}\cup L_{-}$. The frame $L$ is called the main component of the biframe, while $L_{+}$ and $L_{-}$ are, respectively, the positive and negative components. Accordingly, elements of $L_{+}$ are positive and those of $L_{-}$ are negative. We say that an element $a\in L_{+}$ is positive bicomplemented when it is complemented in $L$ with complement in $L_{-}$. Negative bicomplemented elements are defined similarly. We denote by ${\rm B}_{+}({\mathcal{L}})$ and by ${\rm B}_{-}({\mathcal{L}})$ the lattices of positive and negative bicomplemented elements of ${\mathcal{L}}$, respectively. A morphism $h:(L,\,L_{+},\,L_{-})\rightarrow(M,\,M_{+},\,M_{-})$ between biframes is a frame homomorphism $h:L\rightarrow M$ such that $h[L_{+}]\subseteq M_{+}$ and $h[L_{-}]\subseteq M_{-}$. The category of biframes and biframe homomorphisms will be denoted by ${\bf BiFrm}$. We say that $h$ is dense if its underlying frame homomorphism is dense.

We say that a biframe ${\mathcal{L}}=(L,L_{+},L_{-})$ is compact if its main component $L$ is compact, and that it is zero-dimensional if both $L_{+}$ and $L_{-}$ are join-generated by their bicomplemented elements.

Finally, we also have an adjunction ${\bf\Omega}_{b}:{\bf BiTop}\leftrightarrows{\bf BiFrm}^{op}:{\bf pt}_{b}$ between bitopological spaces and biframes, which extends the classical adjunction between topological spaces and frames (here, we identify a topological space $(X,\tau)$ with the bispace $(X,\tau,\tau)$, and a frame $L$ with the biframe $(L,L,L)$). Given a bitopological space ${\mathcal{X}}=(X,\tau_{+},\tau_{-})$, ${\bf\Omega}_{b}({\mathcal{X}})$ is the biframe $(\tau_{+}\vee\tau_{-},\tau_{+},\tau_{-})$, while for a biframe ${\mathcal{L}}=(L,L_{+},L_{-})$, ${\bf pt}_{b}({\mathcal{L}})=({\rm pt}(L),\widehat{L_{+}},\widehat{L_{-}})$, where for $P\in\{L_{+},L_{-}\}$, we denote $\widehat{P}:=\{\widehat{a}\mid a\in P\}$. On morphisms, ${\bf\Omega}_{b}$ and ${\bf pt}_{b}$ are defined as expected.

2.3 The Prime Ideal Theorem

One of the main features of pointfree topology is that it often avoids the use of the Axiom of Choice, thereby leading to constructive results. Sometimes, a strictly weaker version known as the Prime Ideal Theorem is however needed. It may be stated as follows:

Let $D$ be a bounded distributive lattice. Then, every proper ideal of $D$ may be extended to a prime ideal.

In Sections 4 and 5, some results are valid only under the assumption of the Prime Ideal Theorem. The following equivalent statements will be useful in there.

Theorem 2.2**.**

The following statements are equivalent:

1. $(a)$

The Prime Ideal Theorem holds. 2. $(b)$

For every set $X$, every proper filter of ${\mathcal{P}}(X)$ can be extended to an ultrafilter. 3. $(c)$

Every frame of the form ${\rm Idl}(D)$, where $D$ is a bounded distributive lattice, is spatial.

Relevant references for the equivalence between these statements are [2, 8, 11, 12].

2.4 Pervin spaces and Frith frames

A Pervin space is a pair $(X,{\mathcal{S}})$ where $X$ is a set and ${\mathcal{S}}$ a sublattice of its powerset. A morphism $f:(X,{\mathcal{S}})\to(Y,{\mathcal{T}})$ of Pervin spaces is a set function $f:X\to Y$ such that $f^{-1}({\mathcal{T}})\subseteq{\mathcal{S}}$. Since a topology on a set $X$ is, in particular, a bounded sublattice of its powerset, the category ${\bf Top}$ of topological spaces fully embeds in the category ${\bf Pervin}$ of Pervin spaces.

Proposition 2.3** ([7, Section 3]).**

Let $f:(X,{\mathcal{S}})\to(Y,{\mathcal{T}})$ be a map of Pervin spaces. Then,

1. $(a)$

$f$* is an epimorphism if and only if its underlying set map is surjective;* 2. $(b)$

$f$* is an extremal monomorphism if and only if its underlying set map is injective and every element of ${\mathcal{S}}$ is of the form $f^{-1}(T)$ for some $T\in{\mathcal{T}}$.*

In particular, $f$ is an isomorphism if and only if its underlying set map is a bijection and $f[{\mathcal{S}}]={\mathcal{T}}$.

A Frith frame is a pair $(L,S)$, where $L$ is a frame and $S$ is a join-dense bounded sublattice of $L$. A morphism of Frith frames $h:(L,S)\to(M,T)$ is a frame homomorphism between the underlying frames that satisfies $h[S]\subseteq T$. The category of Frith frames and their morphisms is denoted ${\bf Frith}$, and we have a full embedding ${\bf Frm}\hookrightarrow{\bf Frith}$ obtained by identifying a frame $L$ with the Frith frame $(L,L)$.

Proposition 2.4** ([7, Section 4.4]).**

Let $h:(L,S)\to(M,T)$ be a homomorphism of Frith frames. Then,

1. $(a)$

$h$* is a monomorphism if and only if so is its underlying frame homomorphism;* 2. $(b)$

$h$* is an extremal epimorphism if and only if it satisfies $h[S]=T$.*

In particular, $h$ is an isomorphism if and only if it is injective and satisfies $h[S]=T$.

The classical dual adjunction between topological spaces and frames may then be extended to a dual adjunction ${\bf\Omega}:{\bf Pervin}\leftrightarrows{\bf Frith}:{\bf pt}$ between Pervin spaces and Frith frames as follows. For a Pervin space $(X,{\mathcal{S}})$, ${\bf\Omega}(X,{\mathcal{S}})$ is the Pervin space $(\Omega_{{\mathcal{S}}}(X),{\mathcal{S}})$, where $\Omega_{{\mathcal{S}}}(X)$ denotes the topology on $X$ generated by ${\mathcal{S}}$. For a morphism $f:(X,{\mathcal{S}})\rightarrow(Y,{\mathcal{T}})$, ${\bf\Omega}(f)$ is the preimage map $f^{-1}:(\Omega_{\mathcal{T}}(Y),{\mathcal{T}})\to(\Omega_{\mathcal{S}}(X),{\mathcal{S}})$. In the other direction, for a Frith frame $(L,S)$, ${\bf pt}(L,S)$ is the Pervin space $({\rm pt}(L),\widehat{S})$, where $\widehat{S}:=\{\widehat{s}\mid s\in S\}$. Finally, given a morphism of Frith frames $h:(L,S)\to(M,T)$, ${\bf pt}(h)$ maps $p\in{\rm pt}(M)$ to $p\circ h\in{\rm pt}(L)$.

Theorem 2.5** ([7, Proposition 4.3]).**

There is an adjunction ${\bf\Omega}:{\bf Pervin}\leftrightarrows{\bf Frith}^{op}:{\bf pt}$ with ${\bf\Omega}\dashv{\bf pt}$, whose fixpoints are, respectively, the Pervin spaces $(X,{\mathcal{S}})$ such that $(X,\,\Omega_{\mathcal{S}}(X))$ is sober and the Frith frames $(L,S)$ such that $L$ is spatial. These will be called, respectively, sober Pervin spaces and spatial Frith frames.

2.5 Symmetrization

Symmetrization is for Pervin spaces and Frith frames, what uniformization is for quasi-uniform spaces and quasi-uniform frames, respectively. This has been considered in [18] for Pervin spaces and in [7] for Frith frames. In particular, it has been shown that the categories of symmetric Pervin spaces and of symmetric Frith frames are equivalent to the categories of transitive and totally bounded uniform spaces and frames, respectively.

Recall that a Pervin space $(X,{\mathcal{B}})$ is symmetric if ${\mathcal{B}}$ is a Boolean algebra, and the full subcategory of ${\bf Pervin}$ determined by the symmetric Pervin spaces will be denoted by ${\bf Pervin}_{\rm sym}$. A Frith frame $(L,B)$ is symmetric if $B$ is a Boolean algebra, and the full subcategory of ${\bf Frith}$ determined by the symmetric Frith frames will be denoted by ${\bf Frith}_{\rm sym}$.

We define a functor ${\bf Sym}_{\rm Perv}:{\bf Pervin}\rightarrow{\bf Pervin}_{\rm sym}$ as follows. For an object $(X,{\mathcal{S}})$, we let ${\bf Sym}_{\rm Perv}(X,{\mathcal{S}})$ be the Pervin space $(X,\overline{{\mathcal{S}}})$, where $\overline{\mathcal{S}}$ is the Boolean subalgebra of the powerset $\mathcal{P}(X)$ generated by the elements of $\mathcal{S}$. On morphisms, we simply map a function to itself.

Proposition 2.6** ([7, Proposition 3.4]).**

The functor ${\bf Sym}_{\rm Perv}$ is right adjoint to the embedding ${\bf Pervin}_{\rm sym}\hookrightarrow{\bf Pervin}$.

The pointfree version of ${\bf Sym}_{\rm Perv}$ is defined as follows. For a Frith frame $(L,S)$ we set ${\bf Sym}_{\rm Frith}(L,S):=({\mathcal{C}}_{S}L,\overline{S})$, where $\overline{S}$ denotes the sublattice of ${\mathcal{C}}_{S}L$ generated by the elements of the form $\nabla_{s}$ together with their complements. For a morphism of Frith frames $h:(L,S)\rightarrow(M,T)$ we set ${\bf Sym}_{\rm Frith}(h):=\overline{h}$, where $\overline{h}$ is the unique extension of $h$ to a frame homomorphism $\overline{h}:{\mathcal{C}}_{S}L\to{\mathcal{C}}_{T}M$ (recall Proposition 2.1).

Proposition 2.7** ([7, Proposition 6.5]).**

The functor ${\bf Sym}_{\rm Frith}$ is left adjoint to the embedding ${\bf Frith}_{\rm sym}\hookrightarrow{\bf Frith}$.

2.6 Forgetful functors

Both Pervin spaces and Frith frames encode two kinds of structures - topological and lattice-theoretical. It is then natural to consider several forgetful functors on the categories ${\bf Pervin}$ and ${\bf Frith}$.

Every Pervin space $(X,{\mathcal{S}})$ defines a topology $\Omega_{\mathcal{S}}(X)$ on $X$. This assignment can be extended to a functor ${\bf U}_{\rm Pervin}:{\bf Pervin}\rightarrow{\bf Top}$ which leaves functions unaltered.555Under the identification of Pervin spaces with transitive and totally bounded quasi-uniform spaces, this functor forgets the quasi-uniform structure. The pointfree version of this functor is the functor ${\bf U}_{\rm Frith}:{\bf Frith}\rightarrow{\bf Frm}$, which acts as $(L,S)\mapsto L$ on objects, and which leaves frame maps unaltered. The relationship between ${\bf U}_{\rm Pervin}$ and ${\bf U}_{\rm Frith}$ is depicted in the following commutative diagrams:

{\bf Pervin}$${\bf Top}$${\bf Frith}^{op}$${\bf Frm}^{op}$${\bf U}_{\rm Pervin}$$\bf\Omega$$\bf\Omega$${\bf U}_{\rm Frith}$${\bf Pervin}$${\bf Top}$${\bf Frith}^{op}$${\bf Frm}^{op}$${\bf U}_{\rm Pervin}$${\bf pt}$${\bf pt}$${\bf U}_{\rm Frith}

Proposition 2.8** ([7]).**

The functor ${\bf U}_{\rm Pervin}$ is right adjoint to the embedding ${\bf Top}\hookrightarrow{\bf Pervin}$, and the functor ${\bf U}_{\rm Frith}$ is left adjoint to the embedding ${\bf Frm}\hookrightarrow{\bf Frith}$.

Given a topological property, we will often say that a Pervin space has that property provided so does its underlying topological space. For instance, a Pervin space $(X,{\mathcal{S}})$ is $T_{0}$ if $(X,\Omega_{\mathcal{S}}(X))$ is $T_{0}$. The same applies to the notion of dense morphism. We say that a morphism $f:(X,{\mathcal{S}})\to(Y,{\mathcal{T}})$ is dense if the image of ${\bf U}_{\rm Pervin}(f):(X,\Omega_{\mathcal{S}}(X))\to(Y,\Omega_{\mathcal{T}}(Y))$ is dense in $(X,\Omega_{{\mathcal{T}}}(Y))$, that is, if $f[X]$ intersects every nonempty open subset of $(Y,\Omega_{\mathcal{T}}(Y))$. The following characterization of density for Pervin morphisms is easy to prove. We will use it without further mention.

Lemma 2.9**.**

For a map $f:(X,{\mathcal{S}})\rightarrow(Y,{\mathcal{T}})$ of Pervin spaces, the following are equivalent.

1. $(a)$

The map $f$ is dense; 2. $(b)$

$f[X]$* intersects every nonempty element of ${\mathcal{T}}$;* 3. $(c)$

We have $f^{-1}(T)=\emptyset$ implies $T=\emptyset$ for all $T\in{\mathcal{T}}$.

We may also forget the topological structures, thereby obtaining functors ${\bf L}_{\rm Pervin}:{\bf Pervin}\to{\bf DLat}^{op}$ and ${\bf L}_{\rm Frith}:{\bf Frith}\to{\bf DLat}$ defined in the expected way.

In [7, Proposition 4.6], we have proved that ${\bf L}_{\rm Frith}$ is right adjoint to the functor ${\bf Idl}:{\bf DLat}\rightarrow{\bf Frith}$ acting on objects as $S\mapsto({\rm Idl}(S),S)$ and assigning to each morphism $f:S\rightarrow T$ its unique extension to a frame morphism ${\rm Idl}(S)\rightarrow{\rm Idl}(T)$. The component of the counit of this adjunction at a Frith frame $(L,S)$ is the morphism

[TABLE]

We now discuss the point-set version of this result. To define the right adjoint of ${\bf L}_{\rm Pervin}$, we introduce some notation. Given a lattice $D$, we denote by ${\rm pf}(D)$ the set of all prime filters of $D$, and we consider the map

[TABLE]

We denote as $\widetilde{D}:=\{\widetilde{a}\mid a\in D\}$. It is well-known that $\Phi_{D}$ is a lattice homomorphism and it is an embedding if and only if $D$ is isomorphic to a sublattice of the powerset ${\mathcal{P}}(X)$ for some set $X$ (see e.g. [8, Chapter 10]). If we further assume that the Prime Ideal Theorem holds, then $\Phi_{D}$ is always an embedding.

We define the functor ${\bf pf}:{\bf DLat}^{op}\rightarrow{\bf Pervin}$ as the one mapping each lattice $D$ to the Pervin space $({\rm pf}(D),\widetilde{D})$, and each lattice homomorphism $f:D_{1}\rightarrow D_{2}$ to the preimage map ${\bf pf}(f):=f^{-1}:({\rm pf}(D_{2}),\widetilde{D_{2}})\rightarrow({\rm pf}(D_{1}),\widetilde{D_{1}})$. This is well-defined as preimages of prime filters are prime filters, and ${\bf pf}(f)^{-1}(\widetilde{a})=\widetilde{f(a)}$ for every $a\in D_{1}$.

Lemma 2.10**.**

We have an idempotent adjunction ${\bf L}_{\rm Pervin}:{\bf Pervin}\leftrightarrows{\bf DLat}^{op}:{\bf pf}$ with ${\bf L}_{\rm Pervin}\dashv{\bf pf}$.

Proof.

With a routine computation one can show that, given a lattice $D$, the co-restriction of $\Phi_{D}$ to a map $D\to\widetilde{D}$ is a universal morphism from ${\bf L}_{\rm Pervin}$ to $D$ and thus, the counit of the adjunction at $D$. To conclude that the adjunction is idempotent, we only have to note that $\Phi_{D}$ is an isomorphism whenever $D$ is a sublattice of some powerset and that is the case for every lattice component of a Pervin space $(X,{\mathcal{S}})$. ∎

We further remark that the component of the unit of the adjunction ${\bf L}_{\rm Pervin}\dashv{\bf pf}$ at a Pervin space $(X,{\mathcal{S}})$ is the neighborhood morphism of Pervin spaces defined by

[TABLE]

We finish this section by providing an alternative representation of the Pervin space ${\bf pf}(D)$, based on the well-known correspondence between prime filters of $D$ and points of ${\rm Idl}(D)$.

Lemma 2.11**.**

There is a one-to-one correspondence between prime filters of $D$ and points of ${\rm Idl}(D)$ and, under this identification, $\widetilde{a}$ corresponds to $\widehat{a}$, for every $a\in D$. In particular, ${\bf pf}(D)$ is isomorphic to ${\bf pt}({\rm Idl}(D),D)$.

2.7 Open intersections and strongly exact meets

For a Pervin space $(X,{\mathcal{S}})$ we say that an intersection of elements in ${\mathcal{S}}$ is open if it is so in the topological space $(X,\Omega_{\mathcal{S}}(X))$. We will denote by $[\,{\mathcal{S}}\,]_{op}$ the collection of all elements of $\Omega_{\mathcal{S}}(X)$ that are open intersections of elements of ${\mathcal{S}}$. It is easy to see that this collection is closed under open intersections and so, $[\,{\mathcal{S}}\,]_{op}$ may be seen as the closure of ${\mathcal{S}}$ under open intersections.

Let now $L$ be a frame and $P\subseteq L$. The meet $\bigwedge P$ is strongly exact if the corresponding intersection of open sublocales (=open pointfree subspaces) is open, or equivalently, if the congruence $\bigvee_{s\in P}\Delta_{s}$ is open (cf. [1, Section 4.5]). Note that, if $\Delta_{a}=\bigvee_{s\in P}\Delta_{s}$ for some $P\subseteq L$, then the meet $\bigwedge P$ is, by definition, strongly exact, and we necessarily have $a=\bigwedge P$. Given a Frith frame $(L,S)$, we denote by $[\,S\,]_{se}$ the set of elements of $L$ that may be written as a strongly exact meet of elements of $S$. Again, $[\,S\,]_{se}$ can be thought of as the closure of $S$ under strongly exact meets.

Finally, we say that a Pervin space $(X,{\mathcal{S}})$ (respectively, Frith frame $(L,S)$) is strongly exact if the lattice ${\mathcal{S}}$ (respectively, $S$) is closed under open intersections of ${\mathcal{S}}$ (respectively, strongly exact meets of $S$). We denote by $\mathbf{Pervin}_{se}$ and by $\mathbf{Frith}_{se}$ the full subcategories of ${\bf Pervin}$ and of ${\bf Frith}$ determined by the strongly exact objects.

The next result implies that the contravariant functor ${\bf\Omega}:{\bf Pervin}\to{\bf Frith}$ restricts and co-restricts to a functor $\mathbf{Pervin}_{se}\to\mathbf{Frith}_{se}$.

Proposition 2.12** ([1, Proposition 5.3]).**

Let $(X,\tau)$ be a topological space and ${\mathcal{U}}\subseteq\Omega(X)$ be a family of open subsets. If $\bigwedge{\mathcal{U}}$ is a strongly exact meet in the frame $\Omega(X)$, then $\bigcap{\mathcal{U}}$ is an open subset of $X$.

We do not know whether the functor ${\bf pt}:{\bf Frith}\to{\bf Pervin}$ restricts and co-restricts to a functor $\mathbf{Frith}_{se}\to\mathbf{Pervin}_{se}$.

3 The bitopological point of view

3.1 Strong exactness and zero-dimensionality

A Pervin space $(X,\mathcal{S})$ defines the bitopological space $(X,\,\Omega_{{\mathcal{S}}}(X),\,\Omega_{{\mathcal{S}}^{c}}(X))$, where ${\mathcal{S}}^{c}$ denotes the lattice $\{S^{c}\mid S\in{\mathcal{S}}\}$ formed by the complements in $X$ of the elements of ${\mathcal{S}}$.666For the interested reader, this the underlying bitopological space of the quasi-uniform space represented by $(X,{\mathcal{S}})$. The Skula functor ${\bf Sk}_{\rm Pervin}:{\bf Pervin}\rightarrow{\bf BiTop}{}$ is then defined by assigning $(X,\,\Omega_{{\mathcal{S}}}(X),\,\Omega_{{\mathcal{S}}^{c}}(X))$ to the Pervin space $(X,\mathcal{S})$, and mapping each function to itself.

In the other direction, we may define a functor ${\bf Clop}_{+}:{\bf BiTop}\to{\bf Pervin}$ by assigning to each bitopological space ${\mathcal{X}}=(X,\tau_{+},\tau_{-})$ the Pervin space $(X,\,{\rm Clop}_{+}({\mathcal{X}}))$ and keeping morphisms unchanged.

It is easily seen that these are well-defined functors. Let us prove that ${\bf Clop}_{+}$ is left adjoint to ${\bf Sk}_{\rm Pervin}$.

Lemma 3.1**.**

The functor ${\bf Clop}_{+}$ is left adjoint to ${\bf Sk}_{\rm Pervin}:{\bf Pervin}\to{\bf BiTop}$.

Proof.

Let ${\mathcal{X}}=(X,\tau_{+},\tau_{-})$ be a bitopological space. We first observe that

[TABLE]

Since the inclusions ${\rm Clop}_{+}({\mathcal{X}})\subseteq\tau_{+}$ and ${\rm Clop}_{-}({\mathcal{X}})\subseteq\tau_{-}$ hold, the identity function on $X$ induces a morphism of bitopological spaces $\eta_{{\mathcal{X}}}:{\mathcal{X}}\to{\bf Sk}_{\rm Pervin}\circ{\bf Clop}_{+}({\mathcal{X}})$. Let us show that $({\bf Clop}_{+}({\mathcal{X}}),\,\eta_{{\mathcal{X}}})$ is a universal morphism from ${\mathcal{X}}$ to ${\bf Sk}_{\rm Pervin}$. Let $(Y,{\mathcal{T}})$ be a Pervin space and $f:{\mathcal{X}}\to{\bf Sk}_{\rm Pervin}(Y,{\mathcal{T}})$ be a morphism of bitopological spaces. Since $f^{-1}({\mathcal{T}})\subseteq\tau_{+}$ and $f^{-1}({\mathcal{T}}^{c})\subseteq\tau_{-}$, the underlying set function of $f$ defines a morphism $g:{\bf Clop}_{+}({\mathcal{X}})\to(Y,{\mathcal{T}})$. Clearly, $g$ is the unique morphism satisfying ${\bf Sk}_{\rm Pervin}(g)\circ\eta_{{\mathcal{X}}}=f$, and this proves our claim. ∎

We now describe the equivalence of categories determined by ${\bf Clop}_{+}\dashv{\bf Sk}_{\rm Pervin}$.

Proposition 3.2**.**

The fixpoints of the adjunction ${\bf Clop}_{+}:{\bf BiTop}\leftrightarrows{\bf Pervin}:{\bf Sk}_{\rm Pervin}$ are, respectively, the zero-dimensional bispaces and the strongly exact Pervin spaces.

Proof.

It follows from the proof of Lemma 3.1 that the unit of the adjunction ${\bf Clop}_{+}\dashv{\bf Sk}_{\rm Pervin}$ at a bispace ${\mathcal{X}}=(X,\,\tau_{+},\,\tau_{-})$ is the morphism

[TABLE]

defined by the identity map on $X$. Thus, ${\mathcal{X}}$ is a fixpoint of the adjunction if and only if $\tau_{+}=\Omega_{{\rm Clop}_{+}({\mathcal{X}})}(X)$ and $\tau_{-}=\Omega_{{\rm Clop}_{-}({\mathcal{X}})}(X)$, that is, if and only if ${\mathcal{X}}$ is zero-dimensional.

Let us now exhibit the counit of ${\bf Clop}_{+}\dashv{\bf Sk}_{\rm Pervin}$. It is easy to see that the positive clopens of ${\bf Sk}_{\rm Pervin}(X,{\mathcal{S}})=(X,\,\Omega_{\mathcal{S}}(X),\,\Omega_{{\mathcal{S}}^{c}}(X))$ are the open intersections of ${\mathcal{S}}$. Since ${\mathcal{S}}\subseteq[\,{\mathcal{S}}\,]_{op}$, the identity on $X$ defines a morphism

[TABLE]

of Pervin spaces, which can be shown to be the counit of the adjunction. In particular, we have that $(X,{\mathcal{S}})$ is a fixpoint if and only if ${\mathcal{S}}=[\,{\mathcal{S}}\,]_{op}$, that is, if and only if $(X,{\mathcal{S}})$ is a strongly exact Pervin space. ∎

Corollary 3.3**.**

The categories ${\bf BiTop}_{\rm Z}$ and ${\bf Pervin}_{se}$ of zero-dimensional bitopological spaces and of strongly exact Pervin spaces are equivalent.

We finally remark that, since, for every Pervin space $(X,{\mathcal{S}})$, we have

[TABLE]

the unit $\eta_{{\bf Sk}_{\rm Pervin}(X,{\mathcal{S}})}$ is always an isomorphism, and thus, the adjunction ${\bf Clop}_{+}\dashv{\bf Sk}_{\rm Pervin}$ is idempotent.

Let us now look at the pointfree version of the Skula functor and its left adjoint. For a Frith frame $(L,S)$ we set ${\bf Sk}_{\rm Frith}(L,S)=({\mathcal{C}}_{S}L,\nabla L,\Delta S)$.777As for spaces, this is the underlying biframe of the quasi-uniform frame defined by $(L,S)$. In order to define ${\bf Sk}_{\rm Frith}$ on morphisms, we first observe that, by Proposition 2.1, every morphism of Frith frames $h:(L,S)\rightarrow(M,T)$ uniquely extends to a frame homomorphism $\overline{h}:{\mathcal{C}}_{S}L\to{\mathcal{C}}_{T}M$ satisfying

[TABLE]

Therefore, $\overline{h}$ defines a biframe homomorphism $\overline{h}:{\bf Sk}_{\rm Frith}(L,S)\to{\bf Sk}_{\rm Frith}(M,T)$ and we may set ${\bf Sk}_{\rm Frith}(h)=\overline{h}$.

In the other direction, we define ${\bf B}_{+}:{\bf BiFrm}\to{\bf Frith}$ as follows. For a biframe ${\mathcal{L}}=(L,L_{+},L_{-})$, we set ${\bf B}_{+}({\mathcal{L}})=(\langle{\rm B}_{+}({\mathcal{L}})\rangle_{\bf Frm},\,{\rm B}_{+}({\mathcal{L}}))$, where $\langle{\rm B}_{+}({\mathcal{L}})\rangle_{\bf Frm}$ denotes the subframe of $L_{+}$ generated by the lattice ${\rm B}_{+}({\mathcal{L}})$ of positive bicomplemented elements of ${\mathcal{L}}$. In order to define ${\bf B}_{+}$ on morphisms, notice that, if $h:{\mathcal{L}}\to{\mathcal{K}}$ is a biframe homomorphism then, since positive bicomplemented elements of ${\mathcal{L}}$ are mapped to positive bicomplemented elements of ${\mathcal{K}}$, the suitable restriction and co-restriction of $h$ induces a morphism of Frith frames ${\bf B}_{+}h:{\bf B}_{+}({\mathcal{L}})\to{\bf B}_{+}({\mathcal{K}})$.

Next we will see that, as for Pervin spaces, the functors ${\bf Sk}_{\rm Frith}$ and ${\bf B}_{+}$ define an adjunction between the categories of Frith frames and of biframes. However, while the fixpoints of ${\bf Frith}$ are still easy to describe, the same does not happen with those of ${\bf BiFrm}$. We leave it as an open problem to describe the categorical equivalence underlying this adjunction.

Before proceeding, we prove the following technical result:

Lemma 3.4**.**

let $(L,S)$ be a Frith frame and $a\in L$. Then, $\nabla_{a}$ is a positive bicomplemented element of $({\mathcal{C}}_{S}L,\nabla L,\Delta S)$ if and only if $a$ is a strongly exact meet of elements of $S$.

Proof.

Since ${\mathcal{C}}_{S}L$ is a subframe of ${\mathcal{C}}L$, we have that $\nabla_{a}$ is bicomplemented if and only if $\Delta_{a}\in\Delta S$, that is, if and only if there is some $P\subseteq S$ such that $\Delta_{a}=\bigvee_{s\in P}\Delta_{s}$. But this is the same as saying that $\bigwedge P$ is a strongly exact meet and $a=\bigwedge P$. ∎

We are now able to prove that ${\bf Sk}_{\rm Frith}$ is indeed the left adjoint of ${\bf B}_{+}$.

Lemma 3.5**.**

The functor ${\bf Sk}_{\rm Frith}$ is left adjoint to ${\bf B}_{+}:{\bf BiFrm}\to{\bf Frith}$.

Proof.

It follows from Lemma 3.4 that ${\bf B}_{+}\circ{\bf Sk}_{\rm Frith}(L,S)=(\nabla L,\{\nabla_{a}\mid a\in[\,S\,]_{se}\})$ and thus, the isomorphism $\nabla:L\to\nabla L$ induces an embedding of Frith frames

[TABLE]

To conclude that ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$, it suffices to show that $\eta_{(L,S)}$ is universal from $(L,S)$ to ${\bf B}_{+}$, that is, that for every biframe ${\mathcal{K}}$ and every morphism $h:(L,S)\to{\bf B}_{+}({\mathcal{K}})$, there exists a unique $h^{\prime}:{\bf Sk}_{\rm Frith}(L,S)\to{\mathcal{K}}$ such that ${\bf B}_{+}(h^{\prime})\circ\eta_{(L,S)}=h$. But the underlying frame homomorphism of such an $h^{\prime}$ has to be an extension $h^{\prime}:{\mathcal{C}}_{S}L\to K$ of $h$. Since $h[S]$ consists of complemented elements of $K$, by Proposition 2.1, there exists exactly one such morphism, which is easily seen to define a biframe homomorphism $h^{\prime}:{\bf Sk}_{\rm Frith}(L,S)\to{\mathcal{K}}$. ∎

Corollary 3.6**.**

The fixpoints of ${\bf Frith}$ for the adjunction ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$ are the strongly exact Frith frames.

Proof.

It follows from the proof of Lemma 3.5 that the unit of the adjunction ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$ is

[TABLE]

Clearly, this is an isomorphism if and only if $(L,S)$ is strongly exact. ∎

Let ${\mathcal{L}}=(L,L_{+},L_{-})$ be a biframe and ${\bf B}_{+}({\mathcal{L}})=(M,T)$. Since the elements of $T$ are complemented in $L$, by Proposition 2.1, the frame embedding $M\hookrightarrow L$ may be uniquely extended to a frame homomorphism ${\mathcal{C}}_{T}M\to L$. It is easily seen that this map induces a biframe homomorphism $\varepsilon_{\mathcal{L}}:({\mathcal{C}}_{T}M,\nabla M,\Delta T)\to(L,L_{+},L_{-})$. We leave it for the reader to verify that $\varepsilon_{\mathcal{L}}$ is the component at ${\mathcal{L}}$ of the counit of the adjunction ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$. In particular, if $(L,S)$ is a Frith frame then, since $\{\Delta_{s}\mid s\in S\}$ and $\{\Delta_{a}\mid a\in[\,S\,]_{se}\}$ generate the same subframe of ${\mathcal{C}}L$, by Lemma 3.4, we have that ${\bf Sk}_{\rm Frith}\circ{\bf B}_{+}\circ{\bf Sk}_{\rm Frith}(L,S)={\bf Sk}_{\rm Frith}(L,S)$ and $\varepsilon_{{\bf Sk}_{\rm Frith}(L,S)}$ is the identity map. Therefore, the adjunction ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$ is idempotent and, as such, it induces an equivalence between the images of the two involved functors.

While it is clear that every biframe of the form ${\bf Sk}_{\rm Frith}(L,S)$ is zero-dimensional, it is not the case that every zero-dimensional biframe is of that form.

Example 3.7**.**

888This example was borrowed from [7, Example 5.13]. The interested reader may show that the fixpoints of the adjunction ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$ are precisely the underlying biframes of the quasi-uniform frames representable by a Frith frame in the sense of [7, Proposition 5.6].

Let $X$ be a topological space such that the congruence frame of its frame of opens is not spatial (see [15, Theorem 3.4] for a characterization of the frames whose congruence frame is not spatial). We let ${\mathcal{L}}=(L,L_{+},L_{-})$ be the Skula biframe of $X$, that is: $L_{+}$ is the frame of opens of $X$, $L_{-}$ is the subframe of ${\mathcal{P}}(X)$ generated by the complements of the elements of $L_{+}$, and $L$ is the subframe of ${\mathcal{P}}(X)$ generated by $L_{+}\cup L_{-}$. To show that ${\mathcal{L}}$ is not a fixpoint of the adjunction ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$, we first recall that the underlying frame homomorphism of the counit of ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$ at a biframe ${\mathcal{L}}=(L,L_{+},L_{-})$ is the unique frame extension $\varepsilon_{{\mathcal{L}}}:{\mathcal{C}}_{T}M\to L$ of the embedding $M\hookrightarrow L$, where $(M,T)={\bf B}_{+}({\mathcal{L}})$. Since, in this case, we have ${\bf B}_{+}({\mathcal{L}})=(L_{+},L_{+})$, ${\mathcal{L}}$ is a fixpoint if and only if the unique frame homomorphism ${\mathcal{C}}L_{+}\to L$ extending $L_{+}\hookrightarrow L$ is an isomorphism. But that is not the case because $L$ is spatial and ${\mathcal{C}}L_{+}$ is not. A concrete example is given by taking for $X$ the real line $\mathbb{R}$ equipped with the Euclidean topology $\Omega(\mathbb{R})$. Since the Booleanization of $\Omega(\mathbb{R})$ is a pointless nontrivial sublocale, by the characterization of [15], its congruence frame is not spatial.

Also, the fixpoints of ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$ need not be compact as ${\bf Sk}_{\rm Frith}(L,S)$ is not compact if neither is $L$. We may however show that every compact and zero-dimensional biframe is a fixpoint.

Proposition 3.8**.**

Let ${\mathcal{L}}=(L,L_{+},L_{-})$ be a biframe and $\varepsilon_{\mathcal{L}}:({\mathcal{C}}_{T}M,\nabla M,\Delta T)\to(L,L_{+},L_{-})$ be the component at ${\mathcal{L}}$ of the counit of the adjunction ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$, where $(M,T)={\bf B}_{+}({\mathcal{L}})$. Then,

1. $(a)$

$\varepsilon_{\mathcal{L}}$* is dense,* 2. $(b)$

if ${\mathcal{L}}$ is zero-dimensional, then $\varepsilon_{\mathcal{L}}[\nabla M]=L_{+}$ and $\varepsilon_{\mathcal{L}}[\Delta T]=L_{-}$.

In particular, if ${\mathcal{L}}$ is compact and zero-dimensional, then $\varepsilon_{\mathcal{L}}$ is an isomorphism and thus, ${\mathcal{L}}$ is a fixpoint of the adjunction ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$.

Proof.

Let $a\in M$ and $t\in T$ be such that $\varepsilon_{\mathcal{L}}(\nabla_{a}\wedge\Delta_{t})=0$. By definition of $\varepsilon_{\mathcal{L}}$, this is the same as having that the equality $a\wedge t^{*}=0$ holds in $L$. Since $t$ is complemented in $L$, this is equivalent to $a\leq t$ which, in turn, implies $\nabla_{a}\wedge\Delta_{t}=0$. This proves that $\varepsilon_{\mathcal{L}}$ is dense.

Now, again by definition of $\varepsilon_{\mathcal{L}}$, we have that $\varepsilon_{\mathcal{L}}[\nabla M]\supseteq T$ and $\varepsilon_{\mathcal{L}}[\Delta T]\supseteq T^{*}$. Since $T$ is the lattice of bicomplemented elements of $L_{+}$, if ${\mathcal{L}}$ is zero-dimensional, this implies that $\varepsilon_{\mathcal{L}}[\nabla M]=L_{+}$ and $\varepsilon_{\mathcal{L}}[\Delta T]=L_{-}$. Thus, $(b)$ holds.

Finally, recall that $\varepsilon_{\mathcal{L}}$ is an isomorphism of biframes provided its underlying frame homomorphism is injective and satisfies $\varepsilon_{\mathcal{L}}[\nabla M]=L_{+}$ and $\varepsilon_{\mathcal{L}}[\Delta T]=L_{-}$. Thus, it suffices to show that if ${\mathcal{L}}$ is compact and zero-dimensional then $\varepsilon_{\mathcal{L}}$ is injective. But it is well-known that dense frame homomorphisms with zero-dimensional domain (which is the case of ${\mathcal{C}}_{T}M$) and compact codomain are injective (see e.g. [17, Chapter VII, Proposition 2.2.2]).999The result cited is stated for a regular domain, but every zero-dimensional frame is regular. ∎

The following is as close as we will get to a pointfree version of the result stated in Corollary 3.3.

Corollary 3.9**.**

Strongly exact Frith frames are a full coreflective subcategory of the category of zero-dimensional biframes.

We finish this section by relating the point-set and pointfree versions of the functors we have considered.

Proposition 3.10**.**

The following squares commute up to natural isomorphism.

{\bf BiTop}$${\bf Pervin}$${\bf BiFrm}$${\bf Frith}$${\bf Clop}_{+}$$\bf\Omega$${\bf\Omega}_{b}$${\bf B}_{+}$${\bf Pervin}$${\bf BiTop}$${\bf Frith}$${\bf BiFrm}$${\bf Sk}_{\rm Pervin}$${\bf pt}_{b}$${\bf pt}$${\bf Sk}_{\rm Frith}

Proof.

Commutativity of the left-hand side diagram follows easily from computing the functors ${\bf B}_{+}\circ{\bf\Omega}_{b}$ and ${\bf\Omega}\circ{\bf Clop}_{+}$. To show that the right-hand side diagram commutes up to natural isomorphism, we define a natural isomorphism $\beta:{\bf Sk}_{\rm Pervin}\circ{\bf pt}\implies{\bf pt}_{b}\circ{\bf Sk}_{\rm Frith}$ as follows. For a Frith frame $(L,S)$, we define

[TABLE]

where $\widetilde{p}$ is the unique morphism making the following diagram commute (cf. Proposition 2.1).

L$${\mathcal{C}}_{S}L$${\bf 2}$$\nabla$$\widetilde{p}$$p

By uniqueness of each $\widetilde{p}$, this correspondence establishes a bijection between the points of $L$ and the points of ${\mathcal{C}}_{S}L$. Let us show that this is a homeomorphism with respect to the first topology of ${\bf Sk}_{\rm Pervin}\circ{\bf pt}(L,S)$. We first note that the positive open subsets of ${\bf Sk}_{\rm Pervin}\circ{\bf pt}(L,S)$ are the subsets of the form $\widehat{a}$, while those of ${\bf pt}_{b}\circ{\bf Sk}_{\rm Frith}(L,S)$ are the subsets of the form $\widehat{\nabla_{a}}$, where $a\in L$. Now, given $a\in L$ and $p\in{\rm pt}(L)$, using commutativity of the triangle above, we have

[TABLE]

Since $\beta_{(L,S)}$ is a bijection, this implies that $\beta_{(L,S)}$ is both continuous and open with respect to the first topologies, thus a homeomorphism. Showing that $\beta_{(L,S)}$ is also a homeomorphism with respect to the second topology is analogous, and we leave it for the reader.

Now, $\beta$ is a natural transformation provided the following square commutes for every morphism $h:(M,T)\to(L,S)$ of Frith frames.

{\bf Sk}_{\rm Pervin}\circ{\bf pt}(L,S)$${\bf pt}_{b}\circ{\bf Sk}_{\rm Frith}(L,S)$${\bf Sk}_{\rm Pervin}\circ{\bf pt}(M,T)$${\bf pt}_{b}\circ{\bf Sk}_{\rm Frith}(M,T)$$\beta_{(L,S)}$$(-)\circ{\bf Sk}_{\rm Frith}(h)$$(-)\circ h$$\beta_{(M,T)}

That is indeed the case because, for every $p\in{\rm pt}(L)$ and $x\in M$, we have the following equalities:

[TABLE]

Proposition 3.10 makes it natural to ask whether the corresponding diagrams for the spectrum and open-set functors also commute. The answer is negative, as shown by the next example.

Example 3.11**.**

For the first diagram, consider the biframe ${\mathcal{L}}=({\bf 3},{\bf 3},{\bf 2})$, where ${\bf 3}$ denotes the $3$-element chain. Then, ${\bf pt}\circ{\bf B}_{+}({\mathcal{L}})$ is a space with one point, while ${\bf Clop}_{+}\circ{\bf pt}_{b}({\mathcal{L}})$ has two, so these cannot be isomorphic. For the second diagram, we let $X$ be a topological space as in Example 3.7 and observe that ${\bf\Omega}_{b}\circ{\bf Sk}_{\rm Pervin}(X,\Omega(X))$ is the Skula biframe ${\mathcal{L}}$ of $X$. As already argued, ${\mathcal{L}}$ is not in the image of ${\bf Sk}_{\rm Frith}$, thus, ${\bf\Omega}_{b}\circ{\bf Sk}_{\rm Pervin}(X,\Omega(X))$ is not isomorphic to ${\bf Sk}_{\rm Frith}\circ{\bf\Omega}(X,\Omega(X))$.

3.2 The monotopological case

In this section, we will investigate the monotopological version of the results of Section 3.1. Under the identifications ${\bf Top}\hookrightarrow{\bf BiTop}$ and ${\bf Frm}\hookrightarrow{\bf BiFrm}$, these will follow as a consequence of the latter.

Let us consider the restrictions ${\bf Clop}:{\bf Top}\to{\bf Pervin}$ and ${\bf B}:{\bf Frm}\to{\bf Frith}$ of the functors ${\bf Clop}_{+}$ and ${\bf B}_{+}$ defined in Section 3.1. Explicitly, ${\bf Clop}$ maps a topological space $(X,\tau)$ to the Pervin space ${\bf Clop}_{+}(X,\tau,\tau)=(X,\,{\rm Clop}(X,\tau))$, where ${\rm Clop}(X,\tau)$ denotes the Boolean algebra of clopen subsets of $X$ for the topology $\tau$, and a morphism to itself. On the other hand, given a frame $L$, ${\bf B}(L)$ is the pair $(\langle{\rm B}(L)\rangle_{\bf Frm},\,{\rm B}(L))$, where $\langle{\rm B}(L)\rangle_{\bf Frm}$ denotes the subframe of $L$ generated by the lattice of complemented elements ${\rm B}(L)$ of $L$, and a frame homomorphism $h:L\to K$ is sent to the morphism of Frith frames ${\bf B}h:{\bf B}(L)\to{\bf B}(K)$ induced by the suitable restriction and co-restriction of $h$. Then, the adjunctions ${\bf Clop}_{+}:{\bf BiTop}\leftrightarrows{\bf Pervin}:{\bf Sk}_{\rm Pervin}$ and ${\bf Sk}_{\rm Frith}:{\bf Frith}\leftrightarrows{\bf BiFrm}:{\bf B}_{+}$ studied in Section 3.1 restrict, respectively, to adjunctions ${\bf Clop}:{\bf Top}\leftrightarrows{\bf Pervin}^{\prime}:{\bf U}_{\rm Pervin}^{\prime}$ and ${\bf U}_{\rm Frith}^{\prime}:{\bf Frith}^{\prime}\leftrightarrows{\bf Frm}:{\bf B}$, where

• •

${\bf Pervin}^{\prime}$ denotes the full subcategory of ${\bf Pervin}$ determined by the Pervin spaces $(X,{\mathcal{S}})$ such that ${\bf Sk}_{\rm Pervin}(X,{\mathcal{S}})$ belongs to the image of ${\bf Top}\hookrightarrow{\bf BiTop}$,

• •

${\bf Frith}^{\prime}$ denotes the full subcategory of ${\bf Frith}$ determined by the Frith frames $(L,S)$ such that ${\bf Sk}_{\rm Frith}(L,S)$ belongs to the image of ${\bf Frm}\hookrightarrow{\bf BiFrm}$,

• •

${\bf U}_{\rm Pervin}^{\prime}$ is the suitable restriction and co-restriction of ${\bf Sk}_{\rm Pervin}$, and

• •

${\bf U}_{\rm Frith}^{\prime}$ is the suitable restriction and co-restriction of ${\bf Sk}_{\rm Frith}$.

The following result, whose proof is trivial, explains our choice of notation for the functors ${\bf U}_{\rm Pervin}^{\prime}$ and ${\bf U}_{\rm Frith}^{\prime}$: these are nothing but the suitable restrictions of the functors ${\bf U}_{\rm Pervin}$ and ${\bf U}_{\rm Frith}$ defined in Section 2.6.

Lemma 3.12**.**

The following statements hold:

1. $(a)$

a Pervin space $(X,{\mathcal{S}})$ belongs to ${\bf Pervin}^{\prime}$ if and only if $\Omega_{\mathcal{S}}(X)=\Omega_{{\mathcal{S}}^{c}}(X)$, 2. $(b)$

a Frith frame $(L,S)$ belongs to ${\bf Frith}^{\prime}$ if and only if $\nabla L=\Delta S$.

In particular, given $(X,{\mathcal{S}})\in{\bf Pervin}^{\prime}$ and $(L,S)\in{\bf Frith}^{\prime}$, the following equalities hold:

[TABLE]

We will now characterize the categorical equivalences induced by the adjunctions ${\bf Clop}\dashv{\bf U}_{\rm Pervin}^{\prime}$ and ${\bf U}_{\rm Frith}^{\prime}\dashv{\bf B}$. Recall that we have seen in Section 3.1 that both ${\bf Clop}_{+}\dashv{\bf Sk}_{\rm Pervin}$ and ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$ are idempotent and, therefore, so are their restrictions.

Proposition 3.13**.**

The categories of zero-dimensional topological spaces and that of strongly exact symmetric Pervin spaces are equivalent.

Proof.

Since ${\bf Clop}\dashv{\bf U}_{\rm Pervin}^{\prime}$ is a restriction of ${\bf Clop}_{+}\dashv{\bf Sk}_{\rm Pervin}$, by Proposition 3.2, it induces an equivalence between the categories of topological spaces that are zero-dimensional when seen as bitopological spaces, and the category determined by the Pervin spaces $(X,{\mathcal{S}})\in{\bf Pervin}^{\prime}$ that are strongly exact. The former are easily seen to be the zero-dimensional topological spaces. We argue that $(X,{\mathcal{S}})\in{\bf Pervin}^{\prime}$ is strongly exact if and only if it is a strongly exact symmetric Pervin space. Clearly, ${\bf Pervin}^{\prime}$ contains all symmetric Pervin spaces, thus the backwards implication is trivial. Conversely, if $(X,{\mathcal{S}})\in{\bf Pervin}^{\prime}$ is strongly exact then, being a fixpoint of the idempotent adjunction ${\bf Clop}\dashv{\bf U}_{\rm Pervin}^{\prime}$, it belongs to the image of ${\bf Clop}$. Hence, it is symmetric, as required. ∎

Proposition 3.14**.**

The categories of zero-dimensional frames and that of strongly exact symmetric Frith frames are equivalent.

Proof.

Since the adjunction ${\bf U}_{\rm Frith}^{\prime}\dashv{\bf B}$ is idempotent, its fixpoints in ${\bf Frm}$ are the frames of the form ${\bf U}_{\rm Frith}^{\prime}(L,S)=L$, for $(L,S)\in{\bf Frith}^{\prime}$. Noticing that the inclusion $\nabla L\supseteq\Delta S$ holds if and only if $S$ consists of complemented elements, these are easily seen to be the zero-dimensional ones. On the other hand, an argument similar to that used in the proof of Proposition 3.13 shows that the fixpoints of ${\bf U}_{\rm Frith}^{\prime}\dashv{\bf B}$ in ${\bf Frith}^{\prime}$ are strongly exact symmetric Frith frames. ∎

4 Complete Pervin spaces and complete Frith

frames

In this section we will show that the dual adjunction ${\bf\Omega}:{\bf Pervin}\leftrightarrows{\bf Frith}:{\bf pt}$ induces a duality between $T_{0}$ complete Pervin spaces on the one hand and complete Frith frames on the other. We use the following definition from [10, 18].

Definition 4.1** ([10, 18]).**

Let $(X,{\mathcal{S}})$ be a Pervin space. A filter $F\subseteq{\mathcal{P}}(X)$ is a Cauchy filter if it is proper and, for every $S\in\mathcal{S}$, either $S$ or its complement is in $F$. We say that a Cauchy filter $F$ converges to the point $x\in X$ if every open neighborhood $U\in\Omega_{\overline{{\mathcal{S}}}}(X)$ of $x$ belongs to $F$. Finally, a Pervin space $(X,\mathcal{S})$ is said to be Cauchy complete if every Cauchy filter converges, and a Cauchy completion of $(X,{\mathcal{S}})$ is a dense extremal monomorphism $c:(X,{\mathcal{S}})\hookrightarrow(Y,{\mathcal{T}})$ into a Cauchy complete Pervin space $(Y,{\mathcal{T}})$.101010In [10] Cauchy complete and Cauchy completion are simply named complete and completion, respectively.

The following is an easy observation that we state for later reference.

Lemma 4.2**.**

Let $(X,{\mathcal{S}})$ be a Pervin space, and $F\subseteq{\mathcal{P}}(X)$ be a Cauchy filter. Then, $F$ converges to $x$ if and only if $x$ belongs to $\bigcap(F\cap\overline{{\mathcal{S}}})$.

Note that a filter is Cauchy with respect to $(X,{\mathcal{S}})$ if and only if it is Cauchy with respect to $(X,\overline{{\mathcal{S}}})$. Therefore, a Pervin space is Cauchy complete if and only if so is its symmetrization. As observed in [10, 18], one may show that this notion of Cauchy complete Pervin space correctly captures the notion of a complete quasi-uniform space. It is known that complete quasi-uniform spaces may be equivalently characterized via dense extremal monomorphisms. In the case of Pervin spaces, the suitable definitions are the following.

Definition 4.3**.**

A symmetric Pervin space $(X,{\mathcal{B}})$ is complete if every dense extremal monomorphism $(X,{\mathcal{B}})\hookrightarrow(Y,{\mathcal{C}})$, with $(Y,{\mathcal{C}})$ a $T_{0}$ symmetric Pervin space is an isomorphism. More generally, we say that a Pervin space $(X,{\mathcal{S}})$ is complete if so is its symmetrization.

Our next goal is to show that Definitions 4.1 and 4.3 are equivalent. Before we move on, we need to prove a couple of technical lemmas.

Lemma 4.4**.**

Let $m:(X,{\mathcal{S}})\hookrightarrow(Y,{\mathcal{T}})$ be a dense extremal monomorphism. If $F\subseteq{\mathcal{P}}(Y)$ is a Cauchy filter, then so is $m^{-1}(F)$.

Proof.

Let $F\subseteq{\mathcal{P}}(Y)$ be a Cauchy filter. Since $m$ is dense and $F$ is proper, $m^{-1}(F)$ is, by Lemma 2.9, a proper filter too. Now, given $S\in{\mathcal{S}}$, since $m$ is an extremal monomorphism, we have $S=m^{-1}(T)$ for some $T\in{\mathcal{T}}$. Since $F$ is Cauchy, it contains either $T$ or $T^{c}$ and thus, $m^{-1}(F)$ contains either $S=m^{-1}(T)$ or $S^{c}=m^{-1}(T^{c})$. This shows that $m^{-1}(F)$ is Cauchy as well. ∎

Recall the neighborhood map $\mathcal{N}_{(X,{\mathcal{S}})}:(X,{\mathcal{S}})\to({\rm pf}({\mathcal{S}}),\,\widetilde{\mathcal{S}})$ from (5), that is, the unit of the adjunction ${\bf L}_{\rm Pervin}\dashv{\bf pf}$.

Lemma 4.5**.**

For a $T_{0}$ Pervin space $(X,{\mathcal{S}})$, the map $\mathcal{N}_{(X,{\mathcal{S}})}$ is an extremal monomorphism of Pervin spaces whose symmetrization is dense.

Proof.

If $(X,{\mathcal{S}})$ is $T_{0}$, then different points have different neighborhood filters in ${\mathcal{S}}$, and so $\mathcal{N}_{(X,{\mathcal{S}})}$ is injective. Since, for every $S\in{\mathcal{S}}$, we have $\mathcal{N}_{(X,{\mathcal{S}})}^{-1}(\widetilde{S})=S$, the map $\mathcal{N}_{(X,{\mathcal{S}})}$ is an extremal monomorphism. To show that ${\bf Sym}_{\rm Perv}(\mathcal{N}_{(X,{\mathcal{S}})})$ is dense, suppose that $\mathcal{N}_{(X,{\mathcal{S}})}^{-1}(\widetilde{S_{1}}\cap\widetilde{S_{2}}^{c})=S_{1}\cap S_{2}^{c}=\emptyset$, that is, $S_{1}\subseteq S_{2}$. Then, there is no prime filter containing $S_{1}$ and omitting $S_{2}$, which means that $\widetilde{S_{1}}\cap\widetilde{S_{2}}^{c}$ must be empty. ∎

We remark that, for every $T_{0}$ Pervin space $(X,{\mathcal{S}})$, the map $\mathcal{N}_{(X,{\mathcal{S}})}:(X,{\mathcal{S}})\hookrightarrow({\rm pf}({\mathcal{S}}),\widetilde{\mathcal{S}})$ is the completion of $(X,{\mathcal{S}})$ (cf. [10, 18]).

We may now prove the following characterization of $T_{0}$ complete Pervin spaces.

Theorem 4.6**.**

Let $(X,{\mathcal{S}})$ be a $T_{0}$ Pervin space. Then, the following are equivalent:

1. $(a)$

$(X,{\mathcal{S}})$* is Cauchy complete;* 2. $(b)$

$(X,{\mathcal{S}})$* is complete;* 3. $(c)$

Every extremal monomorphism $(X,{\mathcal{S}})\hookrightarrow(Y,{\mathcal{T}})$ into a $T_{0}$ Pervin space whose symmetrization is dense is an isomorphism; 4. $(d)$

$(X,{\mathcal{S}})$* is isomorphic to ${\bf pf}({\mathcal{S}})$;* 5. $(e)$

$(X,{\mathcal{S}})$* is isomorphic to ${\bf pt}({\rm Idl}({\mathcal{S}}),{\mathcal{S}})$;* 6. $(f)$

$(X,{\mathcal{S}})$* is isomorphic to a Pervin space of the form ${\bf pt}({\rm Idl}(D),D)$, for some lattice $D$;* 7. $(g)$

$(X,{\mathcal{S}})$* is isomorphic to a Pervin space of the form ${\bf pf}(D)$, for some lattice $D$.*

Proof.

Noting that extremal monomorphisms are preserved under symmetrization, the equivalence between $(b)$ and $(c)$ follows. That $(c)$ implies $(d)$ is a consequence of Lemma 4.5. The equivalences between $(d)$ and $(e)$ and between $(f)$ and $(g)$ follow from Lemma 2.11, while that $(e)$ implies $(f)$ is trivial. It remains to show that $(a)$ implies $(b)$ and that $(g)$ implies $(a)$.

Suppose that $(a)$ holds, and let $m:(X,\overline{{\mathcal{S}}})\hookrightarrow(Y,{\mathcal{C}})$ be a dense extremal monomorphism into a symmetric $T_{0}$ Pervin space $(Y,{\mathcal{C}})$. We need to show that $m$ is an isomorphism, that is, that $m$ is surjective. Given $y\in Y$, consider the filter $F_{y}:={\uparrow}\{C\in{\mathcal{C}}\mid y\in C\}$. Since ${\mathcal{C}}$ is a Boolean algebra, $F_{y}$ is a Cauchy filter. By Lemma 4.4, the filter $m^{-1}(F_{y})$ is Cauchy as well. Since $(X,{\mathcal{S}})$ is Cauchy complete, $m^{-1}(F_{y})$ converges to some point $x\in X$. We claim that $y=m(x)$. Since $(Y,{\mathcal{C}})$ is $T_{0}$ and ${\mathcal{C}}$ is a Boolean algebra, we have that $y=m(x)$ provided $y\in C$ implies $m(x)\in C$, for every $C\in{\mathcal{C}}$. We let $C\in{\mathcal{C}}$ be such that $y\in C$. Then, $m^{-1}(C)$ belongs to $m^{-1}(F_{y})\cap\overline{{\mathcal{S}}}$ and, since $m^{-1}(F_{y})$ converges to $x$, by Lemma 4.2, it follows that $x\in m^{-1}(C)$, that is, $m(x)\in C$, as required.

Finally, let us assume that we have a Pervin space of the form ${\bf pf}(D)=({\rm pf}(D),\widetilde{D})$, with $D$ a distributive lattice. Suppose that $F\subseteq{\mathcal{P}}({\rm pf}(D))$ is a Cauchy filter and set $P:=\{a\in D\mid\widetilde{a}\in F\}$. Clearly, $P$ is a filter of $D$. Let us show that $P$ is prime. Let $a,b\in D$ be such that $a\vee b\in P$, and suppose that $a\notin P$. Equivalently, $a,b$ are such that $\widetilde{a\vee b}=\widetilde{a}\cup\widetilde{b}\in F$ and $\widetilde{a}\notin F$. Since $F$ is Cauchy, it follows that $(\widetilde{a})^{c}$ belongs to $F$ and thus, so does $\widetilde{b}\supseteq(\widetilde{a})^{c}\cap\widetilde{b}=(\widetilde{a})^{c}\cap(\widetilde{a}\cup\widetilde{b})$. This shows that $b\in P$ as required. We now claim that $F$ converges to $P$. By Lemma 4.2, it suffices to show that $P\in\widetilde{a}\cap(\widetilde{b})^{c}$ whenever $a,b\in D$ are such that $\widetilde{a}\cap(\widetilde{b})^{c}\in F$. Since $F$ is proper, having $\widetilde{a}\cap(\widetilde{b})^{c}\in F$ implies that $\widetilde{a}\in F$ and $\widetilde{b}\notin F$. But by definition of $P$, this means that $P\in\widetilde{a}\cap(\widetilde{b})^{c}$, as required. ∎

From now on, we will drop the use of Cauchy complete and call complete Pervin space every Pervin space satisfying the equivalent conditions of Theorem 4.6.

In turn, completeness of Frith frames is discussed in [7], where a characterization of complete Frith frames using both dense extremal epimorphisms and Cauchy maps is given. Here, it will suffice to consider the following definitions:

Definition 4.7** ([7]).**

We say that a symmetric Frith frame $(L,B)$ is complete if every dense extremal epimorphism $(M,C)\twoheadrightarrow(L,B)$ with $(M,C)$ symmetric is an isomorphism. More generally, a Frith frame $(L,S)$ is complete provided its symmetric reflection ${\bf Sym}_{\rm Frith}(L,S)$ is complete. A completion of $(L,S)$ is a complete Frith frame $(M,T)$ together with a dense extremal epimorphism $(M,T)\twoheadrightarrow(L,S)$.

The fact that completeness of a Frith frame $(L,S)$ is equivalent to completeness of the associated quasi-uniform frame is shown in [7, Proposition 7.2]. Moreover, every Frith frame $(L,S)$ has a unique, up to isomorphism, completion, which is given by the counit (3) of the adjunction ${\bf Idl}\dashv{\bf L}_{\rm Frith}$. Also in [7], we have shown the following:

Theorem 4.8** **([7, Proposition 4.6 and

Theorem 7.7]).

Let $(L,S)$ be a Frith frame. Then, the following are equivalent:

1. $(a)$

$(L,S)$* is complete;* 2. $(b)$

$(L,S)$* is coherent;* 3. $(c)$

$L$* is isomorphic to the ideal completion ${\rm Idl}(S)$ of $S$.*

Part $(c)$ of this characterization, together with Theorem 4.6$(f)$, yield the following:

Corollary 4.9**.**

A Pervin space is $T_{0}$ and complete if and only if it is of the form ${\bf pt}(L,S)$, for some complete Frith frame $(L,S)$.

In particular, the functor ${\bf pt}:{\bf Frith}\to{\bf Pervin}$ restricts and co-restricts to a functor $\mathbf{CFrith}\to\mathbf{CPervin}$. In order to show that $\bf\Omega$, too, restricts correctly, we will need to use the Prime Ideal Theorem.

Proposition 4.10**.**

The following are equivalent.

1. $(a)$

The Prime Ideal Theorem holds; 2. $(b)$

If $(X,{\mathcal{S}})$ is a $T_{0}$ complete Pervin space, then the Frith frame ${\bf\Omega}(X,{\mathcal{S}})$ is complete. 3. $(c)$

If $(X,{\mathcal{B}})$ is a $T_{0}$ complete symmetric Pervin space, then the Frith frame ${\bf\Omega}(X,{\mathcal{B}})$ is complete.

Proof.

We first show that $(a)$ implies $(b)$. Let $(X,{\mathcal{S}})$ be a $T_{0}$ complete Pervin space. By Theorem 4.6, we may assume, without loss of generality, that $(X,{\mathcal{S}})={\bf pt}({\rm Idl}({\mathcal{S}}),{\mathcal{S}})$. Since we are assuming that the Prime Ideal Theorem holds, by Theorem 2.2, ${\rm Idl}({\mathcal{S}})$ is a spatial frame, and thus so is $({\rm Idl}({\mathcal{S}}),{\mathcal{S}})$ (cf. Theorem 2.5). Therefore, we have

[TABLE]

which, by Theorem 4.8, is a complete Frith frame.

Clearly, $(b)$ implies $(c)$. Finally, suppose that $(c)$ holds, and let $X$ be a set. By Theorem 2.2, it suffices to show that every proper filter $F$ on $X$ is contained in a prime filter. For the sake of readability, we set $B:={\mathcal{P}}(X)$. Note that showing that $F$ is contained in some prime filter is equivalent to showing that the intersection $\bigcap_{S\in F}\widetilde{S}$ is nonempty. For that, we consider the $T_{0}$ symmetric Pervin space $({\rm pf}(B),\widetilde{B})$. By Theorem 4.6, this is complete, and by hypothesis, so is the Frith frame ${\bf\Omega}({\rm pf}(B),\,\widetilde{B})=(\Omega_{\widetilde{B}}({\rm pf}(B)),\widetilde{B})$. In particular, the topological space $({\rm pf}(B),\Omega_{\widetilde{B}}({\rm pf}(B)))$ is compact, and thus, it suffices to show that $\{\widetilde{S}\mid S\in F\}$ has the finite intersection property. In turn, since $F$ is closed under finite meets, this is the same as showing that $\widetilde{S}\neq\emptyset$ for every $S\in F$. But since $F$ is proper, every $S\in F$ is nonempty, and given $x\in S$, we have ${\uparrow}\{x\}\in\widetilde{S}$ and $\widetilde{S}$ is nonempty as well. This finishes the proof. ∎

Corollary 4.11**.**

The following are equivalent.

1. $(a)$

The Prime Ideal Theorem holds; 2. $(b)$

If $(X,{\mathcal{S}})$ is a $T_{0}$ complete Pervin space, then the compact open subsets of $(X,\,\Omega_{\mathcal{S}}(X))$ are precisely the elements of ${\mathcal{S}}$.

Proof.

By the equivalence between $(a)$ and $(b)$ of Proposition 4.10, it suffices to show that ${\bf\Omega}(X,{\mathcal{S}})$ is a complete Frith frame if and only if the compact open subsets of $(X,\,\Omega_{\mathcal{S}}(X))$ are precisely the elements of ${\mathcal{S}}$. Observe that, by Theorem 4.8, ${\bf\Omega}(X,{\mathcal{S}})=(\Omega_{\mathcal{S}}(X),\,{\mathcal{S}})$ is complete if and only if it is coherent. Thus, ${\mathcal{S}}$ is the set of compact elements of the frame $\Omega_{\mathcal{S}}(X)$, hence of compact open subsets of the topological space $(X,\,\Omega_{\mathcal{S}}(X))$. ∎

We have just proved the following:

Corollary 4.12**.**

If the Prime Ideal Theorem holds, then the adjunction ${\bf\Omega}:{\bf Pervin}\leftrightarrows{\bf Frith}:{\bf pt}$ restricts and co-restricts to an adjunction between $T_{0}$ complete Pervin spaces and complete Frith frames.

We may now show the main result of this section.

Theorem 4.13**.**

If the Prime Ideal Theorem holds, then the adjunction ${\bf\Omega}:{\bf Pervin}\leftrightarrows{\bf Frith}:{\bf pt}$ restricts and co-restricts to a duality between the categories $\mathbf{CFrith}$ of complete Frith frames and $\mathbf{CPervin}$ of $T_{0}$ complete Pervin spaces.

Proof.

Recall from Theorem 2.5 that the adjunction ${\bf\Omega}\dashv{\bf pt}$ induces a duality between sober Pervin spaces and spatial Frith frames. Thus, because of Corollary 4.12, it remains to show that $T_{0}$ complete Pervin spaces are sober and complete Frith frames are spatial. By Theorem 4.6, a $T_{0}$ Pervin space is complete if and only if it is isomorphic to the Pervin space ${\bf pt}({\rm Idl}(D),D)$, for some lattice $D$, and thus a complete Pervin space is sober. In turn, complete Frith frames are spatial because, by Theorem 4.8, they are of the form $({\rm Idl}(D),D)$ for some lattice $D$ and, by the Prime Ideal Theorem, these are spatial Frith frames (cf. Theorems 2.2 and 2.5). ∎

5 Stone-type dualities

In this section we will see how several Stone-type dualities relate to the duality between complete Frith frames and $T_{0}$ complete Pervin spaces shown in the previous section (cf. Theorem 4.13). Note that the fact that every $T_{0}$ complete Pervin space defines a spectral, a Priestley, and a pairwise Stone space is already observed in [18], but no proof is provided. Here, we will give the functorial details of this assignment, and use Theorem 4.13 to interpret Stone-type dualities as a restriction an co-restriction of the dual adjunction ${\bf\Omega}:{\bf Pervin}\leftrightarrows{\bf Frith}:{\bf pt}$ along full subcategory embeddings.

5.1 Stone duality

Stone duality establishes that the categories of bounded distributive lattices and of spectral spaces are dually equivalent. We recall that a topological space is spectral if it is sober, and its compact open subsets are closed under finite intersections and form a basis of the topology. The category of spectral spaces together with those continuous functions such that the preimages of compact open subsets are compact will be denoted by ${\bf Spec}$. By identifying each lattice with the coherent frame given by its ideal completion, Stone duality may be seen as a restriction and co-restriction of the dual adjunction ${\bf\Omega}:{\bf Top}\leftrightarrows{\bf Frm}:{\bf pt}$, but not along full inclusions, as not every continuous function is a morphism of spectral spaces, and morphisms of coherent frames are required to preserve compact elements. We will now see that this duality may also be seen as a restriction and co-restriction of the dual adjunction ${\bf\Omega}:{\bf Pervin}\leftrightarrows{\bf Frith}:{\bf pt}$, the advantage being that spectral spaces and bounded distributive lattices form full subcategories of ${\bf Pervin}$ and ${\bf Frith}$, respectively.

It follows straightforwardly from Theorem 4.8 (by identifying each lattice $S$ with the Frith frame $({\rm Idl}(S),S)$) that the categories of complete Frith frames and of bounded distributive lattices are equivalent, and by definition of morphism of Frith frames, this is indeed a full subcategory of ${\bf Frith}$ (see also [7, Proposition 4.6]). Given the Prime Ideal Theorem, we also have that every $T_{0}$ complete Pervin space defines a spectral space.

Lemma 5.1**.**

If the Prime Ideal Theorem holds, then the functor ${\bf U}_{\rm Pervin}:{\bf Pervin}\to{\bf Top}$ restricts and co-restricts to a functor $\mathbf{CPervin}\to{\bf Spec}$.

Proof.

Let $(X,{\mathcal{S}})$ be a $T_{0}$ complete Pervin space. By Theorem 4.13, $(X,{\mathcal{S}})$ is a fixpoint of the adjunction ${\bf\Omega}\dashv{\bf pt}$ and thus, it is sober, that is to say that the topological space $(X,\Omega_{\mathcal{S}}(X))$ is sober (recall Theorem 2.5). By Corollary 4.11, the lattice ${\mathcal{S}}$ is the set of compact open elements of $(X,\,\Omega_{\mathcal{S}}(X))$. Therefore, $(X,\Omega_{\mathcal{S}}(X))$ is spectral. Finally, note that this also implies that if $f:(X,{\mathcal{S}})\to(Y,{\mathcal{T}})$ is a morphism of $T_{0}$ complete Pervin spaces, then is induces a morphism $f:(X,\Omega_{\mathcal{S}}(X))\to(Y,\Omega_{\mathcal{T}}(Y))$ of spectral spaces. ∎

It remains then to show that the categories of $T_{0}$ complete Pervin spaces and of spectral spaces are, in fact, isomorphic. Consider the functor ${\bf KO}:\mathbf{Spec}\rightarrow\mathbf{CPervin}$ which sends a spectral space $(X,\tau)$ to the Pervin space $X$ equipped with the lattice of compact open subsets of $X$. It is easily seen that ${\bf KO}$ is well-defined. We may further prove the following:

Proposition 5.2**.**

If the Prime Ideal Theorem holds, then the functors ${\bf U}_{\rm Pervin}$ and ${\bf KO}$ establish an isomorphism of categories between ${\bf Spec}$ and $\mathbf{CPervin}$.

Proof.

Let $(X,{\mathcal{S}})$ be a $T_{0}$ complete Pervin space. By Corollary 4.11, ${\bf KO}\circ{\bf U}_{\rm Pervin}$ is the identity functor on $\mathbf{CPervin}$. For a spectral space $(X,\tau)$, we have that ${\bf U}_{\rm Pervin}\circ{\bf KO}(X,\tau)$ is the set $X$ equipped with the topology generated by the lattice of compact open subsets of $(X,\tau)$. But by definition of spectral space, this is $(X,\tau)$ itself. ∎

Corollary 5.3**.**

If the Prime Ideal Theorem holds, then Stone duality for bounded distributive lattices may be seen as a restriction along full subcategory embeddings of the dual adjunction ${\bf\Omega}:{\bf Pervin}\leftrightarrows{\bf Frith}:{\bf pt}$.

5.2 Priestley duality

Another duality for bounded distributive lattices, due to Priestley, uses the so-called Priestley spaces in place of spectral spaces. A Priestley space is a compact topological space equipped with a partial order relation on its points satisfying the Priestley separation axiom, which states that for points $x\nleq y$ there is a clopen upper set (“upset” hereon) containing $x$ and omitting $y$. A morphism of Priestley spaces is a continuous map which is monotone with respect to the order. We denote by $\bf Priest$ the category of Priestley spaces and corresponding morphisms. We have already seen that $T_{0}$ complete Pervin spaces form a category equivalent to spectral spaces, and it is well-known that the latter form a category equivalent to $\bf Priest$. It is the goal of this section to explicitly exhibit the correspondence between $T_{0}$ complete Pervin spaces and Priestley spaces, thereby providing yet another way of understanding Priestley duality.

As noticed in [18], every Pervin space $(X,{\mathcal{S}})$ comes naturally equipped with a preorder given by

[TABLE]

which is a partial order exactly when $(X,{\mathcal{S}})$ is $T_{0}$. In the case where $(X,{\mathcal{S}})$ is $T_{0}$ and complete, this is the underlying partial order of the corresponding Priestley space, and its topology is the patch topology of the bitopological space ${\bf Sk}_{\rm Pervin}(X,{\mathcal{S}})$.

Lemma 5.4**.**

If the Prime Ideal Theorem holds, then there is a well-defined functor ${\bf P}:\mathbf{CPervin}\to\bf Priest$ defined by ${\bf P}(X,{\mathcal{S}})=(X,\,\Omega_{\overline{{\mathcal{S}}}}(X),\,\leq_{\mathcal{S}})$ on objects, and mapping each morphism to the morphism defined by its underlying set function.

Proof.

If $(X,{\mathcal{S}})$ is $T_{0}$ complete, then so is its symmetrization $(X,\overline{{\mathcal{S}}})$ and, by Corollary 4.11, $X\in\overline{{\mathcal{S}}}$ is a compact element of $\Omega_{\overline{{\mathcal{S}}}}(X)$. Thus, $(X,\,\Omega_{\overline{{\mathcal{S}}}}(X))$ is compact. Since elements of ${\mathcal{S}}$ are clopen upsets of $(X,\,\Omega_{\overline{{\mathcal{S}}}}(X),\,\leq_{\mathcal{S}})$, the relation $\leq_{\mathcal{S}}$ satisfies the Priestley separation axiom. Therefore, ${\bf P}(X,{\mathcal{S}})$ is a Priestley space. It is not hard to see that ${\bf P}$ is well-defined on morphisms, too. ∎

In the other direction, we have the following:

Lemma 5.5**.**

There is well-defined functor ${\bf CUp}:\bf Priest\to\mathbf{CPervin}$ that assigns to each Priestley space $(X,\,\tau,\,\leq)$ the Pervin space $X$ equipped with the lattice of clopen upsets of $X$, and keeps morphisms unchanged.

Proof.

It is easy to verify that ${\bf CUp}$ is well-defined on morphisms. Let us argue that ${\bf CUp}$ is well-defined on objects. Fix a Priestley space $(X,\tau,\leq)$. By the Priestley separation axiom, we have that $(X,{\mathcal{S}}):={\bf CUp}(X,\tau,\leq)$ is $T_{0}$. To show that $(X,{\mathcal{S}})$ is complete, we show that every Cauchy filter converges. Indeed, if $F\subseteq{\mathcal{P}}(X)$ is a Cauchy filter then, since it is proper, it has the finite intersection property. Thus, $F\cap\overline{{\mathcal{S}}}$ is a family of closed subsets of $X$ with the finite intersection property. Since Priestley spaces are compact, it follows that $\bigcap(F\cap\overline{{\mathcal{S}}})$ is nonempty and, by Lemma 4.2, $F$ converges. ∎

We leave it for the reader to verify that the functors ${\bf P}$ and ${\bf CUp}$ are mutually inverse. The reader may also check that, by composing the functors

[TABLE]

one obtains the well-known isomorphism between the categories of spectral and of Priestley spaces.

Proposition 5.6**.**

If the Prime Ideal Theorem holds, then the functors ${\bf P}$ and ${\bf CUp}$ establish an isomorphism of categories between $\bf Priest$ and $\mathbf{CPervin}$.

Corollary 5.7**.**

If the Prime Ideal Theorem holds, then Priestley duality may be seen as a restriction along full subcategory embeddings of the dual adjunction ${\bf\Omega}:{\bf Pervin}\leftrightarrows{\bf Frith}:{\bf pt}$.

5.3 Bitopological duality

It has long been known [3] that the dual adjunction between bitopological spaces and biframes restricts and co-restricts to a duality between $T_{0}$, compact and zero-dimensional bitopological spaces (denoted ${\bf BiTop}_{\rm KZ}$) and compact and zero-dimensional biframes (denoted ${\bf BiFrm}_{\rm KZ}$). A few years later, Priestley duality was considered from a bitopological point of view [16], with Priestley spaces being identified with $T_{0}$, compact and zero-dimensional bitopological spaces, and lattices being identified with compact and zero-dimensional biframes. The point-set half of this correspondence was then rediscovered in [6], where $T_{0}$ compact zero-dimensional bitopological spaces were named pairwise Stone spaces.111111Note that pairwise Stone spaces are the same as $T_{0}$, compact and zero-dimensional bitopological spaces only under the assumption of the Prime Ideal Theorem. It is then clear that $\mathbf{CPervin}$ and $\mathbf{CFrith}$ are equivalent to ${\bf BiTop}_{\rm KZ}$ and ${\bf BiFrm}_{\rm KZ}$, respectively. In this section, we will make these equivalences explicit, using the adjunctions derived in Section 3.1.

Let us start with the equivalence between $T_{0}$ complete Pervin spaces and $T_{0}$, compact, and zero-dimensional bitopological spaces. Recall that we have an idempotent adjunction ${\bf Clop}_{+}\dashv{\bf Sk}_{\rm Pervin}$ whose fixpoints are, respectively, the zero-dimensional bitopological spaces and the strongly exact Pervin spaces. To conclude that this adjunction further restricts to an equivalence between ${\bf BiTop}_{\rm KZ}$ and $\mathbf{CPervin}$, it suffices to show that $T_{0}$ complete Pervin spaces are strongly exact (cf. Corollary 5.9) and that the equality ${\bf Sk}_{\rm Pervin}[\mathbf{CPervin}]={\bf BiTop}_{\rm KZ}$ holds (cf. Lemmas 5.8 and 5.10). For that, we will need to assume the Prime Ideal Theorem.

Lemma 5.8**.**

The following are equivalent.

1. $(a)$

The Prime Ideal Theorem holds. 2. $(b)$

For a $T_{0}$ complete Pervin space $(X,{\mathcal{S}})$, the bispace ${\bf Sk}_{\rm Pervin}(X,{\mathcal{S}})$ is compact. 3. $(c)$

For a $T_{0}$ symmetric complete Pervin space $(X,{\mathcal{B}})$, the bispace ${\bf Sk}_{\rm Pervin}(X,{\mathcal{B}})$ is compact.

Proof.

We first argue that $(b)$ and $(c)$ are equivalent. Clearly, $(b)$ implies $(c)$. For the converse, we only need to remind the reader that a Pervin space $(X,{\mathcal{S}})$ is complete if and only if so is its symmetrization $(X,\overline{{\mathcal{S}}})$ and observe that, by definition of compact bispace, ${\bf Sk}_{\rm Pervin}(X,{\mathcal{S}})$ is compact if and only if so is ${\bf Sk}_{\rm Pervin}(X,\overline{{\mathcal{S}}})$.

Now, taking the equivalence between statements $(a)$ and $(c)$ of Proposition 4.10 into account, it suffices to show that, for every $T_{0}$ symmetric Pervin space $(X,{\mathcal{B}})$, the bispace ${\bf Sk}_{\rm Pervin}(X,{\mathcal{B}})$ is compact if and only if the Frith frame ${\bf\Omega}(X,{\mathcal{B}})$ is coherent (recall that, by Theorem 4.8, a Frith frame is coherent if and only if it is complete). If ${\bf Sk}_{\rm Pervin}(X,{\mathcal{B}})$ is compact, that is, if the topological space $(X,\Omega_{{\mathcal{B}}}(X))$ is compact, then every element of ${\mathcal{B}}$ is compact in the frame $\Omega_{{\mathcal{B}}}(X)$. Indeed, if $B=\bigcup{\mathcal{U}}$ for some family ${\mathcal{U}}\subseteq\Omega_{{\mathcal{B}}}(X)$, then ${\mathcal{U}}\cup\{B^{c}\}$ is an open cover of $(X,\Omega_{{\mathcal{B}}}(X))$ and, if the latter is compact, then ${\mathcal{U}}\cup\{B^{c}\}$ has a finite subcover ${\mathcal{U}}^{\prime}$. This yields $B=\bigcup{\mathcal{U}}^{\prime}\setminus\{B^{c}\}$, with ${\mathcal{U}}^{\prime}\setminus\{B^{c}\}$ finite, thereby showing compactness of $B$. Thus, the Frith frame ${\bf\Omega}(X,{\mathcal{B}})=(\Omega_{\mathcal{B}}(X),{\mathcal{B}})$ is coherent. Conversely, suppose that ${\bf\Omega}(X,{\mathcal{B}})$ is coherent. In particular, its underlying frame $\Omega_{\mathcal{B}}(X)$ is compact. But this is precisely the frame of opens of the patch topology of ${\bf Sk}_{\rm Pervin}(X,{\mathcal{B}})$. Thus, the latter is compact as well. ∎

As a consequence, we immediately obtain that, under the Prime Ideal Theorem, every $T_{0}$ complete Pervin space is strongly exact. We do not know whether this is a necessary hypothesis.

Corollary 5.9**.**

If the Prime Ideal Theorem holds, then $T_{0}$ complete Pervin spaces are strongly exact.

Proof.

Let $(X,{\mathcal{S}})$ be a Pervin space. By Lemma 5.8, we only need to show that if ${\bf Sk}_{\rm Pervin}(X,{\mathcal{S}})$ is compact then $(X,{\mathcal{S}})$ is strongly exact. Let $\bigcap_{i\in I}S_{i}$ be an open intersection of ${\mathcal{S}}$, say $\bigcap_{i\in I}S_{i}=\bigcup_{j\in J}S_{j}^{\prime}$, for some $\{S_{j}\}_{j\in J}\subseteq{\mathcal{S}}$. Then, we have

[TABLE]

and, by compactness of ${\bf Sk}_{\rm Pervin}(X,{\mathcal{S}})$, it follows that there exists a finite subset $J^{\prime}\subseteq J$ such that $X=\bigcup_{i\in I}S_{i}^{c}\cup\bigcup_{j\in J^{\prime}}S_{j}^{\prime}$. But then, we have $\bigcap_{i\in I}S_{i}=\bigcup_{j\in J^{\prime}}S_{j}^{\prime}$, and thus, the intersection $\bigcap_{i\in I}S_{i}$ belongs to ${\mathcal{S}}$, as required. ∎

It only remains to show the inclusion ${\bf Sk}_{\rm Pervin}[\mathbf{CPervin}]\supseteq{\bf BiTop}_{\rm KZ}$.

Lemma 5.10**.**

If ${\mathcal{X}}=(X,\tau_{+},\tau_{-})$ is a compact bitopological space, then the Pervin space ${\bf Clop}_{+}({\mathcal{X}})$ is complete. In particular, every $T_{0}$, compact, and zero-dimensional bitopological space is of the form ${\bf Sk}_{\rm Pervin}(X,{\mathcal{S}})$, for some $T_{0}$ complete Pervin space $(X,{\mathcal{S}})$.

Proof.

We let $\tau$ denote the patch topology of ${\mathcal{X}}$, and we suppose that ${\mathcal{X}}$ is compact, that is, that the space $(X,\tau)$ is compact. We let $(X,{\mathcal{S}})={\bf Clop}_{+}({\mathcal{X}})$ and $F\subseteq{\mathcal{P}}(X)$ be a Cauchy filter. Since $F$ is proper, it has the finite intersection property, and therefore, so does $F\cap\overline{{\mathcal{S}}}$ (which is a subset of ${\rm Clop}(X,\tau)$). By compactness of $(X,\tau)$ it follows that the intersection $\bigcap(F\cap\overline{{\mathcal{S}}})$ is nonempty. Thus, by Lemma 4.2, $F$ converges and $(X,{\mathcal{S}})$ is complete.

Finally, let ${\mathcal{X}}=(X,\tau_{+},\tau_{-})$ be a bitopological space. By Proposition 3.2, if ${\mathcal{X}}$ is zero-dimensional, then it is isomorphic to ${\bf Sk}_{\rm Pervin}\circ{\bf Clop}_{+}({\mathcal{X}})$. If furthermore ${\mathcal{X}}$ is compact then, by the first part of the claim, ${\bf Clop}_{+}({\mathcal{X}})$ is complete. It is also easy to see that ${\bf Clop}_{+}({\mathcal{X}})$ is $T_{0}$ provided ${\mathcal{X}}$ is $T_{0}$ and zero-dimensional. Thus, if ${\mathcal{X}}$ is $T_{0}$, compact, and zero-dimensional, then $(X,{\mathcal{S}})={\bf Clop}_{+}({\mathcal{X}})$ is a $T_{0}$ complete Pervin space satisfying ${\mathcal{X}}\cong{\bf Sk}_{\rm Pervin}(X,{\mathcal{S}})$. ∎

As already explained, we may thus derive the following:

Corollary 5.11**.**

If the Prime Ideal Theorem holds, the adjunction ${\bf Clop}_{+}\dashv{\bf Sk}_{\rm Pervin}$ restricts to an equivalence ${\bf BiTop}_{\rm KZ}\cong\mathbf{CPervin}$.

Let us now consider the pointfree setting. We have seen in Section 3.1 the existence of an idempotent adjunction ${\bf Sk}_{\rm Frith}:{\bf Frith}\leftrightarrows{\bf BiFrm}:{\bf B}_{+}$. Although we were not able to describe the underlying categorical equivalence, we have shown that the fixpoints of ${\bf Frith}$ are the strongly exact Frith frames and that every compact zero-dimensional biframe is a fixpoint of ${\bf BiFrm}$. Thus, we will follow the same strategy as for Pervin spaces and show that complete Frith frames are strongly exact (cf. Lemma 5.14) and the equality ${\bf Sk}_{\rm Frith}[\mathbf{CFrith}]={\bf BiFrm}_{\rm KZ}$ holds (cf. Lemmas 5.15 and 5.16).

Before proceeding, we need to state a technical result. Recall that a filter $F\subseteq L$ on a frame $L$ is Scott-open if whenever $D\subseteq F$ is a directed subset whose join belongs to $F$, the intersection $D\cap F$ is nonempty.

Proposition 5.12** ([13, 14]).**

Scott-open filters are closed under strongly exact meets.

Proof.

It is shown in [13, Lemma 3.4] that every Scott-open filter $F\subseteq L$ is of the form $\{x\in L\mid\Delta_{x}\subseteq\bigvee_{a\in P}\Delta_{a}\}$, for some subset $P\subseteq L$. In turn, filters of this form are shown in [14, Theorem 4.5] to be closed under strongly exact meets. ∎

Remark 5.13**.**

In the proof of Proposition 5.12 we invoked [13, Lemma 3.4], whose proof uses ordinal induction (although no choice principles are required). A constructive alternative proof is provided in [22, Theorem 1.9].

We may now show that complete Frith frames are strongly exact.

Lemma 5.14**.**

Complete Frith frames are strongly exact.

Proof.

Let $(L,S)$ be a complete Frith frame and $P\subseteq S$ be such that $a=\bigwedge P$ is a strongly exact meet. Since, by Theorem 4.8, $P$ consists of compact elements and finite meets of compact elements are compact too, the filter $F\subseteq L$ generated by $P$ is Scott-open. By Proposition 5.12, $a$ belongs to $F$. Thus, there exist $s_{1},\dots,s_{n}\in P$ such that $a\geq s_{1}\wedge\dots\wedge s_{n}$, and therefore also $a=s_{1}\wedge\dots\wedge s_{n}$. This means that $a\in S$, as required. ∎

Lemma 5.15**.**

If $(L,S)$ is a complete Frith frame, then the biframe ${\bf Sk}_{\rm Frith}(L,S)$ is compact (and zero-dimensional).

Proof.

By definition, $(L,S)$ is complete if and only if so is ${\bf Sym}_{\rm Frith}(L,S)=({\mathcal{C}}_{S}L,\overline{S})$. By Theorem 4.8, $({\mathcal{C}}_{S}L,\overline{S})$ is complete if and only if it is coherent. In particular, if $(L,S)$ is complete, then ${\mathcal{C}}_{S}L$ is compact. But, by definition, this means that ${\bf Sk}_{\rm Frith}(L,S)=({\mathcal{C}}_{S}L,\nabla L,\Delta S)$ is compact. Finally, ${\bf Sk}_{\rm Frith}(L,S)$ is clearly zero-dimensional, for every Frith frame $(L,S)$. ∎

Lemma 5.16**.**

If ${\mathcal{L}}$ is a compact biframe, then the Frith frame ${\bf B}_{+}({\mathcal{L}})$ is complete. In particular, every compact and zero-dimensional biframe is of the form ${\bf Sk}_{\rm Frith}(L,S)$, for some complete Frith frame $(L,S)$.

Proof.

Let ${\mathcal{L}}=(L,L_{+},L_{-})$ be a compact biframe and $(M,T)={\bf B}_{+}({\mathcal{L}})$ (that is, $T$ is the lattice of bicomplemented elements of $L_{+}$ and $M$ is the subframe of $L$ it generates). By Theorem 4.8, ${\bf B}_{+}({\mathcal{L}})$ is complete provided $T$ consists of compact elements of $M$. Since $M$ is, by definition, a subframe of $L_{+}$, it suffices to show that bicomplemented elements of $L_{+}$ are compact in $L_{+}$. Let then $t\in L_{+}$ be bicomplemented and suppose that $t\leq\bigvee P$, for some subset $P\subseteq L_{+}$. Then, we have $1=t\vee t^{*}\leq\bigvee P\vee t^{*}$ and, since $L$ is compact, there exists a finite subset $P^{\prime}\subseteq P$ such that $1\leq\bigvee P^{\prime}\vee t^{*}$. But this implies that $t\leq\bigvee P^{\prime}$, as required.

Finally, if ${\mathcal{L}}$ is compact and zero-dimensional then, by Proposition 3.8, ${\mathcal{L}}\cong{\bf Sk}_{\rm Frith}\circ{\bf B}_{+}({\mathcal{L}})$ and, in particular, it is of the form ${\bf Sk}_{\rm Frith}(L,S)$ for some complete Frith frame $(L,S)$. ∎

We may thus conclude the following:

Corollary 5.17**.**

The adjunction ${\bf Sk}_{\rm Frith}\dashv{\bf B}_{+}$ restricts to an equivalence $\mathbf{CFrith}\cong{\bf BiFrm}_{\rm KZ}$.

Corollary 5.18**.**

If the Prime Ideal Theorem holds, then the duality between compact zero-dimensional bitopological spaces and compact zero-dimensional biframes may be seen as restriction and co-restriction of the dual adjunction ${\bf\Omega}:{\bf Pervin}\leftrightarrows{\bf Frith}:{\bf pt}$ along full subcategory embeddings.

We remark that, in [16], the duality between compact zero-dimensional bispaces and compact zero-dimensional biframes is seen as a restriction and co-restriction of the classical dual adjunction ${\bf\Omega}_{b}:{\bf BiTop}\leftrightarrows{\bf BiFrm}:{\bf pt}_{b}$. However, although bitopological spaces and biframes are related to Pervin spaces and Frith frames (namely, via the functors ${\bf Sk}_{\rm Pervin}$ and ${\bf Sk}_{\rm Frith}$, respectively), as seen in Example 3.11, the two extensions of the adjunction ${\bf\Omega}:{\bf Top}\leftrightarrows{\bf Frm}:{\bf pt}$ are not comparable. The situation is different when we restrict to $T_{0}$ complete and to $T_{0}$ compact and zero-dimensional structures, as in that case, both ${\bf\Omega}_{b}:{\bf BiTop}\leftrightarrows{\bf BiFrm}:{\bf pt}_{b}$ and ${\bf\Omega}:{\bf C{\bf Pervin}}\leftrightarrows{\bf C{\bf Frith}}:{\bf pt}$ coincide, up to equivalence. Therefore, the duality of [16] ends up being equivalent to ours.

5.4 Summary

We summarize in the diagram below the categorical equivalences shown in Sections 5.1–5.3, which exhibit several Stone-type dualities as restrictions of the dual adjunction between Pervin spaces and Frith frames. The results marked with $*$ require the use of the Prime Ideal Theorem.

{\bf BiTop}$${\bf Pervin}$${\bf Frith}$${\bf BiFrm}$${\bf BiTop}_{\rm Z}$${\bf BiTop}_{\rm KZ}?{\bf BiFrm}_{\rm KZ}$${\bf Pervin}_{se}$$\bf C{\bf Pervin}$${\bf Frith}_{se}$$\bf C{\bf Frith}$${\bf DLat}$${\bf Spec}$$\bf Priest

$\cong$

Thm. 4.8

$\cong$

Prop. 5.2 ∗

$\cong$

Prop. 5.6 ∗

Cor. 5.9 ∗

Lem. 5.14

Prop. 3.8

${\bf Clop}_{+}$

$\vdash$

{\bf Sk}_{\rm Pervin}$${\bf\Omega}$${\bf pt}$${\bf B}_{+}

$\vdash$

${\bf Sk}_{\rm Frith}$Prop. 2.12?$$\congCor. 3.3$\cong$Cor. 3.6$\cong$Cor. 5.11 ∗$\cong$Thm. 4.13 ∗$\cong$Cor. 5.17

6 The Pervin-$T_{D}$ axiom and locale-based Frith

frames

In [7, Section 4.5] the Pervin-$T_{D}$ axiom is introduced as a Pervin equivalent of the $T_{D}$ axiom for topological spaces. A Pervin space is called Pervin-$T_{D}$ if for every $x\in X$ there is $S\in{\mathcal{S}}$ such that $x\in S$ and $S{\setminus}\{x\}\in{\mathcal{S}}$. In there, the following slight variants of this definition were shown to be equivalent:

Lemma 6.1**.**

Let $(X,{\mathcal{S}})$ be a Pervin space. Then, the following are equivalent:

1. $(a)$

$(X,{\mathcal{S}})$* is Pervin-$T_{D}$,* 2. $(b)$

for every $x\in X$, there are distinct $S_{1},S_{2}\in{\mathcal{S}}$ such that $S_{1}\setminus\{x\}=S_{2}\setminus\{x\}$, 3. $(c)$

for every $x\in X$, there are $S_{1},S_{2}\in{\mathcal{S}}$ such that $S_{1}\setminus S_{2}=\{x\}$.

On the other hand, in [5] the $T_{D}$ axiom is compared to sobriety and it is highlighted that the two axioms are, in some sense, duals of each other. In particular, the following is proven.

Proposition 6.2** ([5, Proposition 4.3]).**

Let $X$ be a topological space. In the category of $T_{0}$ topological spaces we have the following:

1. $(a)$

The space $X$ is sober if and only if whenever we have an extremal monomorphism $f:X\hookrightarrow Y$ such that ${\bf\Omega}(f)$ is an isomorphism $f$ must be an isomorphism. 2. $(b)$

The space $X$ is $T_{D}$ if and only if whenever we have an extremal monomorphism $f:Y\hookrightarrow X$ such that ${\bf\Omega}(f)$ is an isomorphism $f$ must be an isomorphism.

We will now show a Pervin version of this proposition, where sober is replaced by complete and the $T_{D}$-axiom is replaced by the Pervin-$T_{D}$ axiom, being the next lemma the key ingredient. Recall the forgetful function ${\bf L}_{\rm Pervin}:{\bf Pervin}\to{\bf DLat}^{op}$ introduced in Section 2.6.

Lemma 6.3**.**

Let $f:(X,{\mathcal{S}})\to(Y,{\mathcal{T}})$ be a morphism of Pervin spaces. Then,

1. $(a)$

${\bf L}_{\rm Pervin}(f):{\mathcal{T}}\to{\mathcal{S}}$* is injective if and only if ${\bf Sym}_{\rm Perv}(f):(X,\overline{{\mathcal{S}}})\to(Y,\overline{{\mathcal{T}}})$ is dense;* 2. $(b)$

${\bf L}_{\rm Pervin}(f):{\mathcal{T}}\to{\mathcal{S}}$* is surjective if and only if ${\bf\Omega}(f):(\Omega_{\mathcal{T}}(Y),{\mathcal{T}})\to(\Omega_{\mathcal{S}}(X),{\mathcal{S}})$ is an extremal epimorphism of Frith frames. Moreover, if $(X,{\mathcal{S}})$ is $T_{0}$, these are further equivalent to $f$ being an extremal monomorphism of Pervin spaces.*

Proof.

Let us start by proving $(a)$. Since ${\bf L}_{\rm Pervin}(f)$ is a lattice homomorphism, being injective is equivalent to having

[TABLE]

which is easily seen to be equivalent to having

[TABLE]

Since $\overline{{\mathcal{T}}}$ consists of the finite joins of elements of the form $T_{1}\cap T_{2}^{c}$, with $T_{1},T_{2}\in{\mathcal{T}}$, this means that ${\bf Sym}_{\rm Perv}(f)$ is dense, as required.

Finally, the first assertion of $(b)$ is a trivial consequence of the characterization of extremal epimorphisms of Frith frames (recall Proposition 2.4), while the second one is the content of [7, Corollary 4.17]. ∎

Proposition 6.4**.**

Let $(X,{\mathcal{S}})$ and $(Y,{\mathcal{T}})$ be $T_{0}$ Pervin spaces. We have the following.

1. $(a)$

The space $(X,{\mathcal{S}})$ is complete if and only if whenever there is a map $f:(X,{\mathcal{S}})\rightarrow(Y,{\mathcal{T}})$ such that ${\bf L}_{\rm Pervin}(f)$ is an isomorphism $f$ must be an isomorphism. 2. $(b)$

The space $(X,{\mathcal{S}})$ is Pervin-$T_{D}$* if and only if whenever there is a map $f:(Y,{\mathcal{T}})\rightarrow(X,{\mathcal{S}})$ such that ${\bf L}_{\rm Pervin}(f)$ is an isomorphism $f$ must be an isomorphism.*

Proof.

Since $(X,{\mathcal{S}})$ is $T_{0}$, by Lemma 6.3, ${\bf L}_{\rm Pervin}(f)$ is an isomorphism if and only if $f$ is an extremal monomorphism and ${\bf Sym}_{\rm Perv}(f)$ is dense. Thus, part $(a)$ follows from Theorem 4.6$(c)$.

To prove $(b)$, let us first suppose that $(X,{\mathcal{S}})$ is Pervin-$T_{D}$ and let $f:(Y,{\mathcal{T}})\to(X,{\mathcal{S}})$ be such that $(Y,{\mathcal{T}})$ is $T_{0}$ and ${\bf L}_{\rm Pervin}(f)$ is an isomorphism. Since $(Y,{\mathcal{T}})$ is $T_{0}$, by Lemma 6.3$(b)$, $f$ is an extremal monomorphism. Thus, it suffices to show that $f$ is an epimorphism, that is, surjective. Fix $x\in X$. Since $(X,{\mathcal{S}})$ is Pervin-$T_{D}$, by Lemma 6.1$(c)$, the singleton $\{x\}$ belongs to $\overline{{\mathcal{S}}}$. Since, by Lemma 6.3$(a)$, ${\bf Sym}_{\rm Perv}(f)$ is dense, it follows that $\{x\}$ intersects $f[Y]$ (recall Lemma 2.9), that is, $x$ belongs to the image of $f$ as we intended to show. Conversely, let $f:(Y,{\mathcal{T}})\hookrightarrow(X,{\mathcal{S}})$ be the extremal monomorphism induced by $Y:=X\setminus\{x\}$, that is, ${\mathcal{T}}=\{S\setminus\{x\}\mid S\in{\mathcal{S}}\}$. Clearly, $(Y,{\mathcal{T}})$ is $T_{0}$ and $f$ is not an isomorphism. Thus, by assumption, ${\bf L}_{\rm Pervin}(f)$ cannot be injective. That is to say that, there exist distinct $S_{1},S_{2}\in{\mathcal{S}}$ such that $S_{1}\setminus\{x\}=S_{2}\setminus\{x\}$ and thus, by Lemma 6.1$(b)$, $(X,{\mathcal{S}})$ is Pervin-$T_{D}$. ∎

We finish this section by exhibiting a pointfree version of Proposition 6.4, which will now involve the forgetful functor ${\bf L}_{\rm Frith}:{\bf Frith}\to{\bf DLat}$ (cf. Section 2.6). Let us start with a version of Lemma 6.3 for Frith frames.

Lemma 6.5**.**

Let $h:(L,S)\to(M,T)$ be a homomorphism of Frith frames. Then,

1. $(a)$

${\bf L}_{\rm Frith}(h):S\to T$* is injective if and only if ${\bf Sym}_{\rm Frith}(h):({\mathcal{C}}_{S}L,\overline{S})\to({\mathcal{C}}_{T}M,\overline{T})$ is dense;* 2. $(b)$

${\bf L}_{\rm Frith}(h):S\to T$* is surjective if and only if $h$ is an extremal epimorphism.*

Proof.

By definition of ${\bf Sym}_{\rm Frith}$, we have that ${\bf Sym}_{\rm Frith}(h)$ is dense if and only if for every $s_{1},s_{2}\in S$, having $\nabla_{h(s_{1})}\wedge\Delta_{h(s_{2})}=0$ implies that $\nabla_{s_{1}}\wedge\Delta_{s_{2}}=0$. But this is easily seen to be equivalent to having that $h(s_{1})\leq h(s_{2})$ implies that $s_{1}\leq s_{2}$, that is to say that ${\bf L}_{\rm Frith}(h)$ is injective. This proves $(a)$. Part $(b)$ is a straightforward consequence of the definition of ${\bf L}_{\rm Pervin}(h)$ and of the characterization of extremal epimorphisms of Frith frames (cf. Proposition 2.4). ∎

We may then prove the following version of Proposition 6.4$(a)$. In particular, note that it provides an alternative criterion for a Frith frame to be complete, which does not depend on its symmetrization.

Proposition 6.6**.**

A Frith frame $(L,S)$ is complete if and only if for every map $h:(M,T)\rightarrow(L,S)$ such that ${\bf L}_{\rm Frith}(h)$ is an isomorphism, $h$ is an isomorphism.

Proof.

We first observe that $(L,S)$ is complete if and only if every dense extremal epimorphisms $(K,C)\to({\mathcal{C}}_{S}L,\overline{S})$, with $(K,C)$ symmetric, is an isomorphism. Suppose that $(L,S)$ is complete and let $h:(M,T)\rightarrow(L,S)$ be such that ${\bf L}_{\rm Frith}(h)$ is an isomorphism. By Lemma 6.5$(b)$, $h$ is an extremal epimorphism. Thus, we only need to show that it is also a monomorphism, that is, injective. Consider the homomorphism ${\bf Sym}_{\rm Frith}(h):({\mathcal{C}}_{T}M,\overline{T})\to({\mathcal{C}}_{S}L,\overline{S})$. Then, ${\bf Sym}_{\rm Frith}(h)$ is an extremal epimorphism because so is $h$ and, by Lemma 6.5$(a)$, it is dense. Thus, since $(L,S)$ is complete, it is an isomorphism and, in particular, injective. Thus, its restriction $h$ is also injective as required. Conversely, let $h:(K,C)\to({\mathcal{C}}_{S}L,\overline{S})$ be a dense extremal epimorphism, with $(K,C)$ symmetric. Since $h$ is already a morphism in ${\bf Frith}_{\rm sym}$, and thus, ${\bf Sym}_{\rm Frith}(h)=h$, by Lemma 6.5, ${\bf L}_{\rm Frith}(h)$ is an isomorphism. Thus, by hypothesis, $h$ is an isomorphism, which proves that $(L,S)$ is complete. ∎

In order to get an analogue of Proposition 6.4$(b)$, we need to introduce the notion of locale-based Frith frame, which will replace the Pervin-$T_{D}$ axiom in our statement.

We say that a Frith frame $(L,S)$ is locale-based if the smallest sublocale of $L$ that contains $S$ is the whole frame $L$. It is not hard to see that such sublocale consists of the arbitrary meets of elements of the form $a\to s$, where $a\in L$ and $s\in S$. As a consequence, we have the following characterization of locale-based Frith frames, that we state for later reference.

Lemma 6.7**.**

A Frith frame is locale-based if and only if, for every $a\in L$, the following equality holds:

[TABLE]

The following technical result will also be useful:

Lemma 6.8**.**

Let $h:(L,S)\to(M,T)$ be a morphism of Frith frames. If ${\bf L}_{\rm Frith}(h)$ is injective, then $h_{*}\circ h(s)=s$, for every $s\in S$.

Proof.

Since $h_{*}$ is right adjoint to $h$, we have $h\circ h_{*}\circ h=h$. Thus, the claim follows from injectivity of ${\bf L}_{\rm Frith}(h)$. ∎

We are now ready to show the already announced analogue of Proposition 6.4$(b)$.

Proposition 6.9**.**

A Frith frame $(L,S)$ is locale-based if and only if for every map $h:(L,S)\rightarrow(M,T)$ such that ${\bf L}_{\rm Frith}(h)$ is an isomorphism, $h$ is an isomorphism.

Proof.

Let $(L,S)$ be a locale-based Frith frame, and $h:(L,S)\to(M,T)$ be a homomorphism such that ${\bf L}_{\rm Frith}(h)$ is an isomorphism. By Lemma 6.5$(b)$, we know that $h$ is an extremal epimorphism. It remains to show it is injective or, equivalently, that $h_{*}\circ h(a)\leq a$, for every $a\in L$. Let us fix $a\in L$. Since $(L,S)$ is locale-based, by Lemma 6.7, it suffices to show that $h_{*}\circ h(a)\leq b\to s$, whenever $b\in L$ and $s\in S$ satisfy $a\leq b\to s$. That is indeed the case because, given such $b$ and $s$, we have the following:

[TABLE]

For the converse, suppose that $(L,S)$ is such that all maps $h:(L,S)\rightarrow(M,T)$ such that ${\bf L}_{\rm Frith}(h)$ is an isomorphism are isomorphisms. We let $\langle S\rangle_{\bf Loc}$ be the smallest sublocale of $L$ that contains $S$. Since $\langle S\rangle_{\bf Loc}$ is a subposet of $L$, each join computed in $\langle S\rangle_{\bf Loc}$ is greater than or equal to the same join computed in $L$. Thus, $(\langle S\rangle_{\bf Loc},S)$ is also a Frith frame. Finally, we let $q:L\twoheadrightarrow\langle S\rangle_{\bf Loc}$ be the frame quotient defined by the sublocale embedding $\langle S\rangle_{\bf Loc}\hookrightarrow L$. Since the restriction of $q$ to $\langle S\rangle_{\bf Loc}$ is the identity, $q$ induces a morphism of Frith frames $q:(L,S)\to(\langle S\rangle_{\bf Loc},S)$. Clearly we have that ${\bf L}_{\rm Frith}(q)$ is an isomorphism, and so, by hypothesis, $h$ is an isomorphism. This proves that $(L,S)$ is locale-based, as required. ∎