Do strict pro-sets embed in locales?

Question

It is well-known that the category of profinite groups (by which I mean Pro(FiniteGroups), i.e. the category of formal cofiltered limits of finite groups) is equivalent to a full subcategory of topological groups, namely those with "profinite topologies." In fact this is a specialization to groups of a more general statement: the category of pro-(finite sets) is equivalent to the category of topological spaces with profinite topologies, via the functor which says "take the limit in the category of topological spaces, where your finite sets all have the discrete topology."

It is proven in the paper "Prodiscrete groups and Galois toposes" by Moerdijk that more generally, the category of pro-groups with surjective transition maps (aka "strict" or "surjective" pro-groups) is equivalent to that of prodiscrete localic groups, i.e. groups in the category of locales which are a cofiltered limit of ordinary groups, regarded as localic groups with discrete topologies. Is there a non-group version of this? Can "strict pro-sets" be identified with "pro-discrete locales"?

Note that some hypothesis such as "surjective transition maps" is necessary. For instance, the pro-set $\cdots \xrightarrow{+1} \mathbb{N} \xrightarrow{+1} \mathbb{N} \xrightarrow{+1} \mathbb{N}$ is not isomorphic to the trivial pro-set ∅, but its limit in the category of locales is just as empty as its limit in the category of sets.

Answer 1

I think the answer is no.

First note that if $(S_i)_i$ is a pro-set, which we may WLOG assume to be indexed on a directed poset, then the corresponding prodiscrete locale $\lim S_i$ is presented by the following posite. Its underlying poset is the category of elements of the diagram $(S_i)_i$, i.e. its elements are pairs $(i,x)$ with $x\in S_i$ and we have $(i,x)\le (j,y)$ if $i\le j$ and $s_{i j}(x)=y$, where $s_{i j} \colon S_i \to S_j$ is the transition map. The covers are generated by $(i,x) \lhd s_{i j}^{-1}(x)$ for any $i,j,x$.

Thus, the open sets in $\lim S_i$ are the "ideals" for this coverage, i.e. sets $A$ of pairs $(i,x)$ which are down-closed and such that if $(j,y)\in A$ for some $j$ and all $y\in s_{i j}^{-1}(x)$, then $(i,x)\in A$.

Now consider morphisms $S\to 2$, where $2=\{\bot,\top\}$, regarded as a pro-set in the trivial way, giving rise to a discrete locale. A morphism of pro-sets $S\to 2$ is determined by a partition of some $S_i = S_i^\bot \sqcup S_i^\top$ (modulo a suitable equivalence relation as we change $i$). But a morphism of locales $\lim S_i \to 2$ consists of two ideals $A^\bot$ and $A^\top$ which are disjoint and whose union generates the improper ideal (which consists of all pairs $(i,x)$). A pro-set morphism $S\to 2$ induces a locale map $\lim S_i \to 2$ where $A^\bot$ and $A^\top$ are the ideals generated by $S_i^\bot$ and $S_i^\top$, but in general not every morphism $\lim S_i \to 2$ is induced by one $S\to 2$.

Specifically, consider the following pro-set, which is indexed on the natural numbers with the inverse ordering: $$ \dots \to S_i \to \dots \to S_2 \to S_1 \to S_0 $$ We define $S_i = (\mathbb{N} \times \{a,b\}) / \sim_i$, where $\sim_i$ is the equivalence relation generated by $(k,a)\sim_i (k,b)$ for $k\ge i$. The transition maps are the obvious projections, which are surjective. Define $$ A^\bot = \{ (i,(k,a)) | k < i \} \quad\text{and}\quad A^\top = \{ (i,(k,b) | k < i \}.$$ Then $A^\bot \cup A^\top$ generates the improper ideal, since for any $i$ we have $\{ (i+1, (i,a)), (i+1,(i,b)) \} \subset A^\bot \cup A^\top$, which covers $(i,(i,?))$, which covers $(i-1,(i,?))$, and so on down to $(0,(i,?))$. However, no $S_i$ can be partitioned as $S_i = S_i^\bot \sqcup S_i^\top$ in such a way that $S_i^\bot$ generates $A^\bot$ and $S_i^\top$ generates $A^\top$. Thus, this defines a locale map $\lim S_i \to 2$ which does not arise from a pro-set morphism $S\to 2$.