Factorizing the Top-Loc adjunction through positive topologies

TL;DR

This paper characterizes positive topologies as a fibration over locales, constructs an adjunction with topological spaces, and shows how the classical Top-Loc adjunction factors through this new framework.

Contribution

It introduces a novel categorical framework relating positive topologies, locales, and topological spaces via fibrations and adjunctions.

Findings

Positive topologies form a fibration over locales.

An adjunction between positive topologies and Top is constructed.

The classical Top-Loc adjunction factors through the new adjunction.

Abstract

We characterize the category of Sambin's positive topologies as a fibration over the category of locales Loc. The fibration is obtained by applying the Grothendieck construction to a doctrine over Loc. We then construct an adjunction between the category of positive topologies and that of topological spaces Top, and show that the well-known adjunction between Top and Loc factors through the newly constructed adjunction.

Equations

$$f\big{(}\bigvee_{i\in I}x_{i}\big{)}=\bigvee_{i\in I}f(x_{i})$$

$$\text{if }asb\text{ and }b{◃}_{2}V\text{, then }a{◃}_1{s}^{-}V$$

$$\begin{array}[]{ccccc}\varphi_{Z}&:&\mathcal{P}(S)/=_{\triangleleft}&\longrightarrow&\Omega\phantom{\ \ }\\ &&{[U]}&\longmapsto&U\between Z\ \end{array}$$

$$\text{if }asb\text{ and }a{⋉}_{1}U\text{, then }b{⋉}_{2}sU$$

$$\text{if }{L}_1\stackrel{\phi }{⟶}\Omega \text{ belongs to }{\Phi }_1\text{, then }{L}_2\stackrel{f}{⟶}{L}_1\stackrel{\phi }{⟶}\Omega \text{ belongs to }{\Phi }_2$$

$$\big{(}{\bigvee_{i\in I}}\varphi_{i}\big{)}(x):={\bigvee_{i\in I}}\big{(}\varphi_{i}(x)\big{)}\ .$$

$$\mathbf{SL}(\__{,}L)\,:\,\mathbf{SL}\to\mathbf{SL}^{op}\$$

$$\mathbf{Sub}:{\mathbf{SL}}^{op}\to \mathbf{PreOrd}$$

$$\mathbf{Sub}(f)(I)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\mathbf{P}:\mathbf{SL}\to \mathbf{PreOrd}$$

$$\mathbf{P}:({\mathbf{SL}}^{op}{)}^{op}\to \mathbf{PreOrd},$$

$$\Phi \subseteq \mathbf{P}(f)(\Psi ).$$

$$\Phi \circ f\subseteq \Psi ,$$

$$\mathbf{\Delta }:{\mathbf{SL}}^{op}\to \int \mathbf{P},$$

$$\mathbf{BTop}\ =\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.48613pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\}}}\ignorespaces{\hbox{\kern-8.48613pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\int\mathbf{P}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}\ignorespaces\ignorespaces{\hbox{\kern 33.68523pt\raise 11.38263pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.39166pt\hbox{$\scriptstyle{\mathbf{U}}$}}}\kern 3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 70.27095pt\raise 2.92981pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}{\hbox{\kern 32.48613pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\bot}$}}}}}}}{\hbox{\kern 70.26393pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathbf{SL}^{op}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}}\ignorespaces\ignorespaces{\hbox{\kern 33.38013pt\raise-11.3825pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.39166pt\hbox{$\scriptstyle{\mathbf{\Delta}}$}}}\kern 3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 8.48135pt\raise-2.2272pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces}}}}\ignorespaces$$

$$\mathbf{SL}(X,Y)\cong \mathbf{SL}(Y^{op},X^{op})$$

$$\tilde{\mathbf{P}}:{\mathbf{Loc}}^{op}=\mathbf{Frm}⟶\mathbf{PreOrd}$$

$$\int \tilde{\mathbf{P}}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$(\forall I\in \tau )(x\in I\Rightarrow C\between I)⟹x\in C$$

$$\begin{array}[]{rcrcl}\varphi_{C}&:&\tau&\longrightarrow&\Omega\\ &&I&\longmapsto&C\between I\end{array}$$

$$\begin{array}[]{rcl}\mathsf{Closed}(X,\tau)&\longrightarrow&\mathbf{SL}(\tau,\Omega)\\ C&\longmapsto&\varphi_{C}\end{array}$$

$$X\hookrightarrow \{C\subseteq X|C\text{ irreducible closed}\}\hookrightarrow \mathbf{Frm}(\tau ,\Omega ).$$

$$\mathbf{Top}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\mathbf{\Lambda}(X,\tau)\ =\ \big{(}\tau,\{\varphi_{C}\mid C\textrm{ is closed}\}\big{)}.$$

$$\mathbf{Top}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\tilde{f}(x):={\phi }_{\mathsf{cl}\{x\}}\circ f,$$

$$\hat{g}(y):=g^{-1}(\{\phi \in \mathbf{Pt}(Y)\cap \Psi |\phi (y)=1\})\in \tau$$

$$\prod _{i\in I}(L_i,{\Phi }_i)=\left(\prod _{i\in I}{L}_i,\underset{i\in I}{\bigwedge }\mathbf{P}({\pi }_i)({\Phi }_i)\right)$$

$$\sum _{i\in I}(L_i,{\Phi }_i)=\left(\sum _{i\in I}{L}_i,\underset{i\in I}{\bigvee }{\exists }_{j_i}({\Phi }_i)\right)$$

Full text

Keywords: Grothendieck constructions; suplattices; locales; formal topologies.

Mathematics Subject Classification (2010): 06D22; 18B30; 03G30.

1 Introduction

Positive topologies are introduced in [10] (see also [5]) as a natural structure for developing pointfree constructive topology. The category PTop of positive topologies can be regarded as a natural extension of the category Loc of locales; actually Loc is a reflective subcategory of PTop. In a predicative setting, the role of a locale is played by a formal cover $(S,\triangleleft)$ which can be read as a presentation of a frame by generators and relations. A positive topology is then a formal cover endowed with a positivity relation, that is a relation $\ltimes$ between $S$ and $\mathcal{P}(S)$ such that for every $a\in S$ and $U,V\subseteq S$

$a\ltimes U$ $\Longrightarrow$ $a\in U$; 2. 2.

$a\ltimes U\wedge(\forall b\in S)(b\ltimes U\rightarrow b\in V)$ $\Longrightarrow$ $a\ltimes V$; 3. 3.

$a\triangleleft U\wedge a\ltimes V$ $\Longrightarrow$ $(\exists b\in U)(b\ltimes V)$.

The motivating example of a positive topology is built from a topological space, in such a way to keep the information about its closed subsets (classically, all such information is already encoded by the opens); see Section 5.2.

In [6] the first author and S. Vickers characterize positive topologies as locales endowed with a family of suplattice homomorphisms. Here we show that this characterization can be organized into a fibration arising from a doctrine via the so-called Grothendieck construction (see, e.g. [8]).

We will then use this representation to give an adjunction between the category Top of topological spaces and PTop; in particular, the notion of sobriety provided by this adjunction coincides with the one introduced in [10], which is known to be constructively weaker than the usual one [1]. Moreover, the usual Top–Loc adjunction can be factorized as the composition of the Top–PTop adjunction above and the reflection PTop–Loc.

As a by-product, we get the completeness and cocompleteness of the category PTop (and of the wider category BTop). This completes the picture in [7], where the pointwise counterparts of BTop and PTop were shown to be complete and cocomplete.

Our foundational framework is intuitionistic and impredicative, like that provided by the internal language of a topos. We use the term “constructive” in this sense.

2 Basic topologies and positive topologies

According to the usual definition, a suplattice (aka complete join semilattice) is a poset $(L,\leq)$ with all joins, that is $\bigvee X$ exists for all subsets $X\subseteq L$.111In particular, $L$ has the least element 0, namely the empty join. (Actually $L$ has the top element 1 as well, although this should be understood as the empty meet.)

A map $f:L\to M$ preserves joins if

[TABLE]

for every family $(x_{i})_{i\in I}$ in $L$. Suplattices and join-preserving maps form a category $\mathbf{SL}$. We hence refer to join-preserving maps between suplattices as suplattice homomorphisms.

A base for $L$ is a subset $S\subseteq L$ such that $p$ = $\bigvee\{a\in S\ |\ a\leq p\}$ for all $p\in L$. For instance, the powerset $\mathcal{P}(S)$ of a set $S$ is a suplattice (with respect to union); a base for $\mathcal{P}(S)$ is given by all singletons.222Incidentally, note that $\mathcal{P}(S)$ is the free suplattice over the set $S$. Given a base $S$, let $\triangleleft\subseteq S\times\mathcal{P}(S)$ be the relation defined as $a\triangleleft U$ iff $a\leq\bigvee U$. It is easy to check that $\triangleleft$ satisfies the following properties

$a\in U\ \Longrightarrow\ a\triangleleft U$ 2. 2.

$a\triangleleft U\ \land\ (\forall u\in U)(u\triangleleft V)\ \Longrightarrow\ a\triangleleft V$

for every $a\in S$ and $U,V\subseteq S$. A pair $(S,\triangleleft)$ satisfying 1 and 2 above is called a basic cover. A basic cover has to be understood as a presentation of a suplattice by generators and relations. Indeed, any cover induces an equivalence relation $=_{\triangleleft}$ on $\mathcal{P}(S)$ where $U=_{\triangleleft}V$ is $(\forall u\in U)(u\triangleleft V)\land(\forall v\in V)(v\triangleleft U)$. The quotient collection $\mathcal{P}(S)_{/_{=_{\triangleleft}}}$ is a suplattice (with a base indexed by $S$) where joins $\bigvee_{i}[U_{i}]$ can be computed as $[\bigcup_{i}U_{i}]$. To complete the picture, one should note that the cover induced by a suplattice $L$ presents a suplattice which is isomorphic to $L$ itself.

Two basic covers $\mathcal{S}_{1}=(S_{1},\triangleleft_{1})$ and $\mathcal{S}_{2}=(S_{2},\triangleleft_{2})$ are isomorphic if they induce isomorphic suplattices. More generally we say that a morphism from $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ is a suplattice homomorphism from $\mathcal{P}(S_{2})/=_{\triangleleft_{2}}$ and $\mathcal{P}(S_{1})/=_{\triangleleft_{1}}$.333Contravariance is chosen to match the direction of locales. This corresponds to having a relation $s\subseteq S_{1}\times S_{2}$ which respects the covers in the following sense:

[TABLE]

where $s^{-}V=\{x\in S_{1}\ |\ (\exists v\in V)(x\,s\,v)\}$. Actually, the same homomorphism corresponds to several relations which we want to consider equivalent; explicitly, two relations $s$ and $s^{\prime}$ are equivalent if $s^{-}V=_{\triangleleft_{1}}s^{\prime-}V$ for all $V\subseteq S_{2}$.

Basic covers and their morphisms form a category which is dual to the category ${\bf SL}$ of suplattices, that is, equivalent to $\mathbf{SL}^{op}$.

2.1 Basic topologies

A basic topology is a triple $(S,\triangleleft,\ltimes)$ where $(S,\triangleleft)$ is a basic cover and $\ltimes$ is a relation between $S$ and $\mathcal{P}(S)$ such that

$a\ltimes U$ $\Longrightarrow$ $a\in U$; 2. 2.

$a\ltimes U\wedge(\forall b\in S)(b\ltimes U\rightarrow b\in V)$ $\Longrightarrow$ $a\ltimes V$; 3. 3.

$a\triangleleft U\wedge a\ltimes V$ $\Longrightarrow$ $(\exists b\in U)(b\ltimes V)$.

The relation $\ltimes$ is called a positivity relation on $(S,\triangleleft)$. Thus, a basic topology can be regarded as a suplattice together with the extra structure specified by a positivity relation.

The powerset $\Omega=\mathcal{P}(1)$ of a singleton can be identified with the algebra of propositions up to logical equivalence. The last condition in the definition above says that the map

[TABLE]

is well-defined if $Z$ is of the form $\{a\in S\ |\ a\ltimes V\}$, in which case, $\varphi_{Z}$ is a suplattice homomorphism. In other words, each $\{a\in S\ |\ a\ltimes V\}$ gives a suplattice interpretation of $(S,\triangleleft)$ into the set $\Omega$ of truth values. Given any positivity relation $\ltimes$ on $(S,\triangleleft)$, the collection of all such $\varphi_{Z}$ forms a sub-suplattice of $\mathbf{SL}({\mathcal{P}(S)/\!=_{\triangleleft}}\,,\,\Omega)$. Ciraulo and Vickers [6, Theorem 2.3] have shown that there is a bijective correspondence between positivity relations on $(S,\triangleleft)$ and sub-suplattices of $\mathbf{SL}({\mathcal{P}(S)/\!=_{\triangleleft}}\,,\,\Omega)$. Thus, a basic topology can be identified with a pair $(L,\Phi)$ of a suplattice $L$ and a sub-suplattice $\Phi$ of the collection $\mathbf{SL}(L,\Omega)$ of suplattice homomorphisms from $L$ to $\Omega$.

Let $\mathcal{S}_{1}=(S_{1},\triangleleft_{1},\ltimes_{1})$ and $\mathcal{S}_{2}=(S_{2},\triangleleft_{2},\ltimes_{2})$ be basic topologies, and $(L_{1},\Phi_{1})$ and $(L_{2},\Phi_{2})$ be the corresponding suplattices together with sub-suplattices of suplattice homomorphisms into $\Omega$. According to [10], a morphism between basic topologies $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ is a morphism $s$ between $(S_{1},\triangleleft_{1})$ and $(S_{2},\triangleleft_{2})$ satisfying the following additional condition

[TABLE]

for all $a\in S_{1}$, $b\in S_{2}$ and $U\subseteq S_{1}$, where $s\,U=\{y\in S_{2}\mid(\exists\,u\in U)(u\,s\,y)\}$. This corresponds to having a suplattice homomorphism $f:L_{2}\to L_{1}$ such that $\Phi_{1}\circ f\subseteq\Phi_{2}$, where $\Phi_{1}\circ f=\left\{\varphi\circ f\mid\varphi\in\Phi_{1}\right\}$; in other words

[TABLE]

(see [6, Proposition 2.9]).

Let $\mathbf{BTop}$ be the category whose objects are pairs $(L,\Phi)$ of a suplattice $L$ and a sub-suplattice $\Phi$ of $\mathbf{SL}(L,\Omega)$ and whose arrows $f:(L_{1},\Phi_{1})\to(L_{2},\Phi_{2})$ are suplattice homomorphisms $f:L_{2}\to L_{1}$ such that $\Phi_{1}\circ f\subseteq\Phi_{2}$. Apart from the impredicativity involved, $\mathbf{BTop}$ is equivalent to the category of basic topologies in [10].

2.2 Positive topologies

A positive topology is a basic topology $(S,\triangleleft,\ltimes)$ such that the underlying basic cover $(S,\triangleleft)$ is a formal cover [3] (sometimes called formal topology). This means that the suplattice presented by $(S,\triangleleft)$ is a frame, that is, binary meets distribute over arbitrary joins.

By a similar observation as we have made for basic topology in Section 2.1, a positive topology can be identified with a pair $(L,\Phi)$ where $L$ is a frame and $\Phi$ is a sub-suplattice of $\mathbf{SL}(L,\Omega)$. A morphism between such pairs $(L,\Phi)$ and $(M,\Psi)$ is a frame homomorphism $f:M\to L$ such that $\Phi\circ f\subseteq\Psi$, which corresponds to a formal map between positive topologies as described in [10].

Let $\mathbf{PTop}$ be the subcategory of $\mathbf{BTop}$ consisting of objects whose underlying suplattice is a frame and arrows which are frame homomorphisms between underlying frames. The category $\mathbf{PTop}$ is thus essentially equivalent to that of positive topologies in [10].

3 A categorical characterization of BTop and PTop

In this section, we are going to give a categorical characterization of BTop and PTop in terms of Grothendieck constructions over two doctrines on suplattices and locales, respectively.

If $X$ is a set and $L$ is (the carrier of) a suplattice, then the collection of maps $\mathbf{Set}(X,L)$ has a natural suplattice structure where joins are computed pointwise, that is,

[TABLE]

When $X$ has a suplattice structure, then $\mathbf{SL}(X,L)$ is a suplattice as well, actually a sub-suplattice of $\mathbf{Set}(X,L)$.

3.1 A doctrine on suplattices

For $L$ a suplattice, the (contravariant) hom-functor \mathbf{SL}(\__{,}L)\,:\,\mathbf{SL}^{op}\to\mathbf{Set}\ can be also regarded as a functor

[TABLE]

where, for $f\in\mathbf{SL}(X,Y)$ and $\varphi\in\mathbf{SL}(Y,L)$, we have $\mathbf{SL}(f,L)(\varphi)$ = $\varphi\circ f$.

Another well-known contravariant endofunctor is the subobject functor

[TABLE]

which sends each suplattice $L$ to the preorder $\mathbf{Sub}(L)$ of subobjects of $L$ in $\mathbf{SL}$. Recall that a suboject of $L$ can be represented as a subset $I\subseteq L$ closed under joins in $L$. Given $f:M\rightarrow L$ in $\mathbf{SL}$ and $I\in\mathbf{Sub}(L)$, $\mathbf{Sub}(f)$ sends $I$ to the pullback $\{x\in M\ |\ f(x)\in I\}$ of $I$ along $f$.

[TABLE]

The composition $\mathbf{Sub}\circ\mathbf{SL}(\__{,}\Omega)$ is a functor

[TABLE]

which, of course, can also be read as a contravariant functor on $\mathbf{SL}^{op}$

[TABLE]

that is, a doctrine on $\mathbf{SL}^{op}$. By the so-called Grothendieck construction [8], we get a category $\int\mathbf{P}$ whose objects are pairs $(L,\Phi)$ with $L$ a suplattice and $\Phi$ a subobject of $\mathbf{SL}(L,\Omega)$ in $\mathbf{SL}$. An arrow $(L,\Phi)\to(M,\Psi)$ in $\int\mathbf{P}$ is a suplattice homomorphism $f:M\rightarrow L$ such that

[TABLE]

Since $\mathbf{P}(f)(\Psi)$ = $\{\varphi\in\mathbf{SL}(L,\Omega)\ |\ \varphi\circ f\in\Psi\}$ by definition, such a condition is equivalent to the following

[TABLE]

where $\Phi\circ f:=\{\varphi\circ f\mid\varphi\in\Phi\}$. Therefore, $\int\mathbf{P}$ is exactly the category $\mathbf{BTop}$ of Sambin’s basic topologies [10], which we introduced in Section 2.1 above.

This construction yields a forgetful functor $\mathbf{U}:\int\mathbf{P}\rightarrow\mathbf{SL}^{op}$, which is in fact a fibration. The functor has a right adjoint, the constant object functor

[TABLE]

which sends each suplattice $L$ to the object $(L,\mathbf{SL}(L,\Omega))$ and each $f:L\rightarrow M$ in $\mathbf{SL}^{op}$ to itself as an arrow from $\mathbf{\Delta(L)}$ to $\mathbf{\Delta(M)}$ in $\int\mathbf{P}$.

[TABLE]

Moreover $\mathbf{U}\circ\mathbf{\Delta}$ is just the identity functor on $\mathbf{SL}^{op}$. Thus, $\mathbf{\Delta}$ is full and faithful, and so $\mathbf{SL}^{op}$ can be regarded as a reflective subcategory of $\int\mathbf{P}$. In this way, we recover the result in [4].

Note that the monad $T$ induced by the adjunction $\mathbf{U}\dashv\mathbf{\Delta}$ is an idempotent monad. By the results in Section $4.2$ of [2], we have that ${\bf SL}^{op}$ is equivalent both to the category of free algebras (the Kleisli category) and to the category of algebras (the Eilenberg–Moore category) on $T$. Hence the adjunction $\mathbf{U}\dashv\mathbf{\Delta}$ is monadic.

Remark.

In a suplattice, arbitrary meets always exist, that is, if $(L,\leq)$ is a suplattice, then $(L,\leq)^{op}:=(L,\geq)$ is a suplattice as well. Moreover, every suplattice homomorphism $f$ has a right adjoint $f^{op}$ which preserves all meets. This determines a contravariant functor $(\_)^{op}$, which is in fact a self-duality of $\mathbf{SL}$, and

[TABLE]

for all $X$ and $Y$.

Classically, $\mathbf{SL}(\__{,}\Omega)$ is naturally isomorphic to the functor $(\_)^{op}$ because $\Omega^{op}\cong\Omega$ so that $\mathbf{SL}(L,\Omega)$ $\cong$ $\mathbf{SL}(\Omega,L^{op})$ $\cong$ $L^{op}$.555This cannot hold constructively, for if $\varphi:\Omega^{op}\to\Omega$ were an isomorphism, then we could prove $\neg\neg p\leq p$ for every $p\in\Omega$ as follows. Indeed $p=0$ implies $\neg\neg p=0$, and so $\varphi(p)=1$ implies $\varphi(\neg\neg p)=1$. By a characteristic feature of $\Omega$, this gives $\varphi(p)\leq\varphi(\neg\neg p)$, hence $\neg\neg p\leq p$. Therefore, for every $L$, $\mathbf{P}(L)=\mathbf{Sub}(\mathbf{SL}(L,\Omega))\cong\mathbf{Sub}(L^{op})$ which is isomorphic to the lattice of all suplattice quotients of $L$. In other words, an object $(L,\Phi)$ corresponds to an epimorphism $e:L\to\Phi^{op}$, and an arrow $(L,\Phi)\to(M,\Psi)$ is a suplattice homomorphism $f:M\to L$ such that $e\circ f:M\to\Phi^{op}$ preserves the congruence relation on $M$ corresponding to $\Psi$.

3.2 The case of frames (and locales)

The category $\mathbf{Frm}$ of frames is the subcategory of $\mathbf{SL}$ whose objects are frames and whose arrows preserve finite meets (in addition to arbitrary joins). The category $\mathbf{Loc}$ of locales is defined as $\mathbf{Frm}^{op}$. By restricting the functor $\mathbf{P}$ to frames, we get a doctrine

[TABLE]

on $\mathbf{Loc}$, which gives rise to a fibration $\mathbf{U}:\int\widetilde{\mathbf{P}}\rightarrow\mathbf{Loc}$ fitting in a pullback square in $\mathbf{Cat}$ as follows.

[TABLE]

Here $\int\widetilde{\mathbf{P}}$ is exactly the category $\mathbf{PTop}$ as introduced in Section 2.2.

4 Weakly sober spaces

4.1 Irreducible closed subsets

The open sets of a topological space $(X,\tau)$ form a frame with respect to the set-theoretic unions and intersections. A subset $C\subseteq X$ is closed if

[TABLE]

for all $x\in X$. The collection $\mathsf{Closed}(X,\tau)$ of closed subsets in $(X,\tau)$ is a complete lattice (where infima are given by intersections, and joins are given by closure of unions), but constructively need not be a co-frame.666For a Brouwerian counterexample consider the discrete space and recall that the so-called “constant domain axiom” $\forall x(\varphi\vee\psi)\to\varphi\vee\forall x\,\psi$, with $x$ not free in $\varphi$, is not provable constructively.

As usual, it makes sense to define the closure $\mathsf{cl}D$ of a subset $D\subseteq X$ as the intersection of all closed subsets containing $D$.

Every closed subset $C$ of $X$ determines a map

[TABLE]

which preserves joins, that is, $\varphi_{C}\in\mathbf{SL}(\tau,\Omega)$. Note that $\varphi_{D}$ makes sense also when $D$ is an arbitrary subset; however $\varphi_{D}=\varphi_{\mathsf{cl}D}$ because $I\between D$ if and only if $I\between\mathsf{cl}D$ for every $I\in\tau$. So the mapping

[TABLE]

is injective and preserves joins. Thus $\mathsf{Closed}(X,\tau)$ is a subobject of ${\bf SL}(\tau,\Omega)$.777Classically, every $\varphi\in\mathbf{SL}(\tau,\Omega)$ is of the form $\varphi_{C}$: take $C$ to be the closed subset $X\setminus\bigcup\left\{I\in\tau\mid\varphi(I)=0\right\}$. Hence $\mathsf{Closed}(X,\tau)$ $\cong$ ${\bf SL}(\tau,\Omega)$. This cannot be the case constructively, as we will see in Section 4.2.

A closed subset $C\subseteq X$ is irreducible if any of the following equivalent conditions holds:

$\varphi_{C}$ preserves finite meets; 2. 2.

$C$ is inhabited and for every $I,J\in\tau$, if $I\between C$ and $J\between C$, then $(I\cap J)\between C$; 3. 3.

$\{I\in\tau\ |\ I\between C\}$ is a completely-prime filter of opens.

In other words, a closed subset $C$ is irreducible if and only if $\varphi_{C}$ is a frame homomorphism, that is, a point in the sense of locale theory. However we cannot show constructively that all frame homomorphisms $\tau\to\Omega$ arise in this way; see Section 4.2.

Classically, $C$ is irreducible if and only if it is non-empty and cannot be written as a disjoint union of two non-empty closed subsets [9]. Therefore, $\{C\subseteq X\ |\ C\textrm{ irreducible closed}\}$ can be identified with $\mathbf{Frm}(\tau,\Omega)$.

4.2 Weak sobriety

Recall that a space is $T0$ or Kolmogorov if $x=y$ follows from the assumption that $\mathsf{cl}\{x\}=\mathsf{cl}\{y\}$. Since $\mathsf{cl}\{x\}$ is always irreducible, we have the following embedding for a $T0$ space $(X,\tau)$:

[TABLE]

A $T0$ space is weakly sober if every irreducible closed subset is the closure of a singleton, that is, if the embedding $X\hookrightarrow\{C\subseteq X\ |\ C\textrm{ irreducible closed}\}$ is an isomorphism. It is sober if the embedding $X\hookrightarrow\mathbf{Frm}(\tau,\Omega)$ is an isomorphism. Note that every weakly sober space is sober classically.

Constructively, every Hausdorff space is weakly sober. However, if every weakly sober space were sober, the non-constructive principle LPO (the Limited Principle of Omniscience) would be derivable [1]. Thus, we cannot prove that all $\varphi\in\mathbf{SL}(\tau,\Omega)$ are of the form $\varphi_{C}$ for some closed subset $C$; otherwise $\mathbf{Frm}(\tau,\Omega)$ could be identified with the irreducible closed subsets, which would make sobriety and weak sobriety coincide.

5 Factorizing the $\mathbf{Top}$–$\mathbf{Loc}$ adjunction

The usual $\mathbf{\Omega}\dashv\mathbf{Pt}$ adjunction between the category $\mathbf{Top}$ of topological spaces and the category $\mathbf{Loc}$ of locales does not compose with the adjunction $\mathbf{U}\dashv\mathbf{\Delta}$ between $\mathbf{Loc}$ and $\mathbf{PTop}$ to give an adjunction between $\mathbf{Top}$ and $\mathbf{PTop}$.

[TABLE]

Nevertheless, a meaningful adjunction between $\mathbf{Top}$ and $\mathbf{PTop}$ can be given, as explained in the following, through which the usual $\mathbf{Top}$–$\mathbf{Loc}$ adjunction factors.

5.1 Points of a positive topology

The suplattice $\Omega$ is an initial frame, that is, a terminal locale. Hence $\mathbf{\Delta}(\Omega)$ is a terminal object in $\mathbf{PTop}$. We define a point of a positive topology $(L,\Phi)$ as a global point $\mathbf{\Delta}(\Omega)\to(L,\Phi)$ in $\mathbf{PTop}$, and we write $\mathbf{Pt}^{+}(L,\Phi)$ instead of $\mathbf{PTop}(\mathbf{\Delta}(\Omega),(L,\Phi))$. Thus, a point of $(L,\Phi)$ is a frame homomorphism $f:L\to\Omega$ such that $\mathbf{SL}(\Omega,\Omega)\circ f\subseteq\Phi$. Since $\mathbf{SL}(\Omega,\Omega)$ contains the identity map, we have $f\in\Phi$. Conversely, if $f\in\Phi$ and $\varphi\in\mathbf{SL}(\Omega,\Omega)$, then we have $\varphi\circ f=\bigvee\{x\in\{f\}|\,\varphi=\mathsf{id}_{\Omega}\}\in\Phi$. In other words, the points of $(L,\Phi)$ are exactly those points of the locale $L$ that are in $\Phi$. Hence, $\mathbf{Pt}^{+}(L,\Phi)$ can be regarded as a subspace of the topological space $\mathbf{Pt}(L)$.

The construction $\mathbf{Pt}^{+}$ can be extended to a functor from $\mathbf{PTop}$ to $\mathbf{Top}$ as follows. Given an arrow $(L,\Phi)\to(M,\Psi)$ with underlying frame homomorphism $f:M\to L$, the continuous map $\mathbf{Pt}(f):\mathbf{Pt}(L)\to\mathbf{Pt}(M)$, which sends a point $p:L\to\Omega$ to the point $p\circ f:M\to\Omega$, can be restricted to a continuous map $\mathbf{Pt}^{+}(L,\Phi)\to\mathbf{Pt}^{+}(M,\Psi)$ because $\Phi\circ f\subseteq\Psi$.

5.2 The canonical positive topology associated with a space

As shown in Section 4.1, the closed subsets $\mathsf{Closed}(X,\tau)$ of a topological space $(X,\tau)$ can be seen as a sub-suplattice of $\mathbf{SL}(\tau,\Omega)$ via the mapping $C\mapsto\varphi_{C}$. Thus, we can define a functor $\mathbf{\Lambda}:\mathbf{Top}\to\mathbf{PTop}$ whose object part is

[TABLE]

For a continuous map $f:(X,\tau_{X})\to(Y,\tau_{Y})$, the $\mathbf{PTop}$-morphism $\mathbf{\Lambda}(f)$ is just the locale morphism corresponding to the frame homomorphism $f^{-1}:\tau_{Y}\to\tau_{X}$. This makes sense because for any closed subset $C\subseteq X$, the suplattice homomorphism $\varphi_{C}\circ f^{-1}:\tau_{Y}\to\Omega$ is precisely $\varphi_{D}$, where $D=\mathsf{cl}f(C)$.

5.3 The adjunction between $\mathbf{Pt}^{+}$ and $\mathbf{\Lambda}$

Theorem**.**

The following hold:

$\mathbf{Pt}=\mathbf{Pt}^{+}\circ\mathbf{\Delta}$; 2. 2.

$\mathbf{\Omega}=\mathbf{U}\circ\mathbf{\Lambda}$; 3. 3.

$\mathbf{\Lambda}\dashv\mathbf{Pt}^{+}$.

As a consequence, the adjunction between $\mathbf{Top}$ and $\mathbf{Loc}$ factors through an adjunction between $\mathbf{PTop}$ and $\mathbf{Loc}$.

[TABLE]

Proof.

For every locale $L$, $\mathbf{Pt}(L)=\mathbf{Pt}(L)\cap\mathbf{SL}(L,\Omega)=\mathbf{Pt}^{+}(\mathbf{\Delta}(L))$, and for every topological space $(X,\tau)$, $\mathbf{U}(\mathbf{\Lambda}(X,\tau))=\tau=\mathbf{\Omega}(X,\tau)$. Hence 1 and 2 hold.

For 3, if $f:\mathbf{\Lambda}(X,\tau)\to(L,\Phi)$, then one can define a continuous function $\widetilde{f}$ from $(X,\tau)$ to $\mathbf{Pt}^{+}(L,\Phi)$ as follows:

[TABLE]

that is, for every $y\in L$, $\widetilde{f}(x)(y):=\mathsf{cl}\{x\}\between f(y)\in\Omega$.

Conversely, if $g$ is a continuous function from $(X,\tau)$ to $\mathbf{Pt}^{+}(L,\Phi)$, then an arrow $\widehat{g}$ from $\mathbf{\Lambda}(X,\tau)$ to $(L,\Phi)$ is defined as follows:

[TABLE]

for every $y\in L$. This is an arrow in $\mathbf{PTop}$ because for every closed subset $C\subseteq X$, we have $\varphi_{C}\circ\widehat{g}$ = $\bigvee\{\varphi\in\mathbf{Pt}^{+}(L,\Phi)\ |\ \varphi\in g(C)\}\in\Phi$.

The maps $\widetilde{(\_)}$ and $\widehat{(\_)}$ define a natural isomorphism between the functors $\mathbf{PTop}(\mathbf{\Lambda}(\_),\_)$ and $\mathbf{Top}(\_\,,\mathbf{Pt}^{+}(\_))$. ∎

A topological space $(X,\tau)$ is weakly sober when $(X,\tau)\cong\mathbf{Pt}^{+}(\mathbf{\Lambda}(X,\tau))$, while it is sober when $(X,\tau)\cong\mathbf{Pt}(\mathbf{\Omega}(X,\tau))$.

Classically, $\mathbf{SL}(\tau,\Omega)$ = $\{\varphi_{C}\ |\ C\textrm{ is closed}\}$ holds. Hence $\mathbf{\Lambda}=\mathbf{\Delta}\circ\mathbf{\Omega}$, and thus $\mathbf{Pt}^{+}\circ\mathbf{\Lambda}=\mathbf{Pt}^{+}\circ\mathbf{\Delta}\circ\mathbf{\Omega}=\mathbf{Pt}\circ\mathbf{\Omega}$. Therefore, as already noted, sobriety and weak sobriety coincide classically.

6 Limits and colimits in BTop and PTop

Whenever the base $\mathbb{C}$ of a doctrine $\mathbf{P}:\mathbb{C}^{op}\rightarrow\mathbf{PreOrd}$ is complete and the same holds for every fiber $\mathbf{P}(A)$, the Grothendieck construction $\int\mathbf{P}$ gives a complete category. If $(L_{i},\Phi_{i})_{i\in I}$ is a set-indexed family of objects in $\int\mathbf{P}$, its product is given by the object

[TABLE]

together with the projections $\pi_{i}$ inherited from $\mathbb{C}$. The equalizer of two parallel arrows $f,g:(L,\Phi)\rightarrow(M,\Psi)$ in $\int\mathbf{P}$ is e:\big{(}E,\mathbf{P}(e)(\Phi)\big{)}\rightarrow(L,\Phi), where $e:E\rightarrow L$ is the equalizer of $f$ and $g$ in $\mathbb{C}$.

If, moreover, $\mathbb{C}$ is cocomplete and, for every arrow $f$ of $\mathbb{C}$, the monotone map $\mathbf{P}(f)$ has a left adjoint $\exists_{f}$, then $\int\mathbf{P}$ is cocomplete as well. The coproduct of a family of objects $(L_{i},\Phi_{i})_{i\in I}$ in $\int\mathbf{P}$ is given by the object

[TABLE]

together with the injections $j_{i}$ inherited from $\mathbb{C}$. Finally, the coequalizer of $f,g:(L,\Phi)\rightarrow(M,\Psi)$ is $q:(M,\Psi)\rightarrow(Q,\exists_{q}(\Psi))$, where $q:M\rightarrow Q$ is the coequalizer of $f$ and $g$ in $\mathbb{C}$.

The doctrines $\mathbf{P}$ and $\widetilde{\mathbf{P}}$ introduced in Section 3.1 and Section 3.2, respectively, satisfy the above requirements. Indeed, every fiber of $\mathbf{P}$ and $\widetilde{\mathbf{P}}$ is a complete lattice because an arbitrary intersection of sub-suplattices is a sub-suplattice. Moreover, it is well known that both $\mathbf{SL}^{op}$ and $\mathbf{Loc}$ are complete and cocomplete. Finally, every $\mathbf{P}(f)$ has a left adjoint, namely $\exists_{f}(\Phi)=\Phi\circ f$, essentially by the very definition of $\mathbf{P}$. Hence, the categories $\mathbf{PTop}$ and $\mathbf{BTop}$ are complete and cocomplete.

Acknowledgements

Part of this work was carried out while the second author was visiting University of Padova in December 2018. The visit was supported by Core-to-Core Program (A. Advanced Research Networks) of Japan Society for the Promotion of Science.