A pro-set is a pro-object in the category Set.

This should not be confused with proset, an abbreviation of “preordered set.”

Pro-sets versus locales

The classifying locale of a pro-set

Since Pro(Set)Pro(Set) is the free completion of Set under cofiltered limits, any functor out of SetSet into a category with cofiltered limits extends uniquely to a cofiltered-limit-preserving functor from Pro(Set)Pro(Set). In particular, we can consider the functor SetLocSet \to Loc from SetSet to the category of locales which regards a set as a discrete locale.

If (S i) i(S_i)_i is a pro-set, which we may WLOG assume to be indexed on a directed poset, then the corresponding locale limS i\lim S_i is presented by the following posite. Its underlying poset is the category of elements of the diagram (S i) i(S_i)_i, i.e. its elements are pairs (i,x)(i,x) with xS ix\in S_i, and we have (i,x)(j,y)(i,x)\le (j,y) if iji\le j and s ij(x)=ys_{i j}(x)=y, where s ij:S iS js_{i j} \colon S_i \to S_j is the transition map. The covers in the posite are generated by (i,x)s ij 1(x)(i,x) \lhd s_{i j}^{-1}(x) for any i,j,xi,j,x.

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

The pro-set Π 0\Pi_0 of a locale

On the other hand, there is a naturally defined functor Π 0:LocPro(Set)\Pi_0\colon Loc \to Pro(Set) which sends a locale to its pro-set of connected components. The vertices of the cofiltered diagram defining Π 0(X)\Pi_0(X) are decompositions X= iIU iX = \coprod_{i\in I} U_i of XX as a coproduct of open subsets, and the corresponding set is the index set II. A morphism (U i)(V j)(U_i) \to (V_j), called a refinement, consists of a function f:IJf:I\to J such that U iU_i is contained in V f(i)V_{f(i)}; the corresponding function is of course ff.

This diagram is cofiltered: 1. It is nonempty, since XX is the 1-ary coproduct of itself. 1. Given decompositions (U i)(U_i) and (V j)(V_j), the decomposition (U iV j) i,j(U_i \cap V_j)_{i,j} refines both of them. 1. Given parallel refinements f,g:(U i)(V j)f,g:(U_i)\to (V_j), for each ii we have U iV f(i)V g(i)U_i \subseteq V_{f(i)} \cap V_{g(i)}. If we define K={i|f(i)=g(i)}K = \{ i | f(i) = g(i) \} and W i=U iW_i = U_i for iKi\in K, then we have an obvious refinement h:(W k)(U i)h\colon (W_k) \to (U_i) and fh=ghf h = g h. It remains to show that (W k)(W_k) is actually a cover of XX.

Since V j 1V j 2={V j 1|j 1=j 2}V_{j_1} \cap V_{j_2} = \bigcup \{ V_{j_1} | j_1 = j_2 \} (the latter being the join of a subsingleton), we have U i{U i|f(i)=g(i)}U_i \subseteq \bigcup \{ U_i | f(i) = g(i) \} (another join of a subsingleton) and thus U i kKW kU_i \subseteq \bigcup_{k\in K} W_k. Thus, since the U iU_i cover XX, so do the W kW_k.

The classical mathematician may be forgiven for thinking this last argument to be more confusing than necessary, since classically, either f(i)=g(i)f(i)=g(i) (in which case W i=U iW_i = U_i) or f(i)g(i)f(i)\neq g(i) (in which case U i=U_i = \emptyset). Constructively, however, the more involved argument is required.

Note that if XX is locally connected, then it has a “minimal” such decomposition, namely its decomposition into connected components. Thus, in this case Π 0(X)\Pi_0(X) is a mere set.

This is the (0,1)-topos version of the fundamental group of a topos or the fundamental ∞-groupoid of an (∞,1)-topos.


The functor Π 0:LocPro(Set)\Pi_0\colon Loc \to Pro(Set) is left adjoint to lim:Pro(Set)Loc\lim\colon Pro(Set)\to Loc.


Since lim\lim 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 Π 0(X)S\Pi_0(X) \to S, for a set SS, are equivalent to morphisms of locales XS discX \to S_{disc}. But a locale map XS discX \to S_{disc} is precisely a decomposition of XX into disjoint opens indexed by SS, which exactly defines a map Π 0(X)S\Pi_0(X) \to S.

If XX 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 Π 0\Pi_0 becomes a codirected poset, since (in the argument above) each (U i)(U_i) is covered by {U i|f(i)=g(i)}\{ U_i | f(i) = g(i) \}, which must therefore be an inhabited set for all ii, so that f=gf=g. Moreover, since in any refinement f:(U i)(V j)f\colon (U_i) \to (V_j), each V jV_j is covered by {U i|f(i)=j}\{ U_i | f(i)=j\}, 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 Π 0(X)\Pi_0(X) need not be surjective in this sense.

The classifying locale functor is not an embedding

It is well-known that when restricted to the subcategory Pro(FinSet)Pro(FinSet) of profinite sets, the functor lim\lim 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 lim:Pro(Grp)Grp(Loc)\lim\colon Pro(Grp) \to Grp(Loc) into localic groups is fully faithful when restricted to strict or surjective progroups (those whose transition maps are surjective).

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

Specifically, consider the following pro-set, which is indexed on the natural numbers with the inverse ordering:

S iS 2S 1S 0 \cdots \to S_i \to \cdots \to S_2 \to S_1 \to S_0

We define S i=(×{a,b})/ iS_i = (\mathbb{N} \times \{a,b\}) / {\sim_i}, where i\sim_i is the equivalence relation generated by (k,a) i(k,b)(k,a) \sim_i (k,b) for kik \ge i. The transition maps are the obvious projections, which are surjective. Define

A ={(i,(k,a))|k<i}andA ={(i,(k,b)|k<i}. A^\bot = \{ (i,(k,a)) | k \lt i \} \quad\text{and}\quad A^\top = \{ (i,(k,b) | k \lt i \}.

Then A A A^\bot \cup A^\top generates the improper ideal, since for any ii we have {(i+1,(i,a)),(i+1,(i,b))}A A \{ (i+1, (i,a)), (i+1,(i,b)) \} \subset A^\bot \cup A^\top, which covers (i,(i,?))(i,(i,?)), which covers (i1,(i,?))(i-1,(i,?)), and so on down to (0,(i,?))(0,(i,?)). However, no S iS_i can be partitioned as S i=S i S i S_i = S_i^\bot \sqcup S_i^\top in such a way that S i S_i^\bot generates A A^\bot and S i S_i^\top generates A A^\top. Thus, this defines a locale map limS i2\lim S_i \to 2 which does not arise from a pro-set morphism S2S\to 2.

Last revised on January 8, 2018 at 11:49:39. See the history of this page for a list of all contributions to it.