This should not be confused with proset, an abbreviation of “preordered set.”
Since is the free completion of Set under cofiltered limits, any functor out of into a category with cofiltered limits extends uniquely to a cofiltered-limit-preserving functor from . In particular, we can consider the functor from to the category of locales which regards a set as a discrete locale.
If is a pro-set, which we may WLOG assume to be indexed on a directed poset, then the corresponding locale is presented by the following posite. Its underlying poset is the category of elements of the diagram , i.e. its elements are pairs with , and we have if and , where is the transition map. The covers in the posite are generated by for any .
Thus, the open sets in the locale are the “ideals” for this coverage, i.e. sets of pairs which are down-closed and such that if for some and all , then .
On the other hand, there is a naturally defined functor which sends a locale to its pro-set of connected components. The vertices of the cofiltered diagram defining are decompositions of as a coproduct of open subsets, and the corresponding set is the index set . A morphism , called a refinement, consists of a function such that is contained in ; the corresponding function is of course .
This diagram is cofiltered:
It is nonempty, since is the 1-ary coproduct of itself.
Given decompositions and , the decomposition refines both of them.
Given parallel refinements , for each we have . If we define and for , then we have an obvious refinement and . It remains to show that is actually a cover of .
The classical mathematician may be forgiven for thinking this last argument to be more confusing than necessary, since classically, either (in which case ) or (in which case ). Constructively, however, the more involved argument is required.
The functor is left adjoint to .
Since is given by regarding a pro-set as a diagram of discrete locales and taking its limit, it suffices to show that morphisms of pro-sets , for a set , are equivalent to morphisms of locales . But a locale map is precisely a decomposition of into disjoint opens indexed by , which exactly defines a map .
If is an overt locale, then every decomposition is refined by a decomposition into positive elements, so we may as well consider only decompositions into positive opens. If we do this, the cofiltered category indexing becomes a codirected poset, since (in the argument above) each is covered by , which must therefore be an inhabited set for all , so that . Moreover, since in any refinement , each is covered by , in this case the transition maps of the resulting pro-set are surjective. However, for a non-overt locale (which, recall, cannot exist classically, it seems that the pro-set need not be surjective in this sense.
It is well-known that when restricted to the subcategory of profinite sets, the functor is fully faithful and in fact lands inside the subcategory of topological locales, its image being the category of Stone spaces.
It is also true that when lifted to progroups, the functor into localic groups is fully faithful when restricted to strict or surjective progroups (those whose transition maps are surjective).
However, in general the functor is not an embedding. For a counterexample, consider morphisms , where is a pro-set and , regarded as a pro-set in the trivial way (and thus giving rise to a discrete locale). A morphism of pro-sets is determined by a partition of some (modulo a suitable equivalence relation as we change ). But a morphism of locales consists of two ideals and which are disjoint and whose union generates the improper ideal (which consists of all pairs ). A pro-set morphism induces a locale map where and are the ideals generated by and , but in general not every morphism is induced by one .
Specifically, consider the following pro-set, which is indexed on the natural numbers with the inverse ordering:
We define , where is the equivalence relation generated by for . The transition maps are the obvious projections, which are surjective. Define
Then generates the improper ideal, since for any we have , which covers , which covers , and so on down to . However, no can be partitioned as in such a way that generates and generates . Thus, this defines a locale map which does not arise from a pro-set morphism .