The etale locale of a sheaf?

Question

It's well-known that sheaves over a topological space are equivalent to etale spaces over the same space.

Now if we replace "topological space" by "locale", we can still define sheaves over a locale, and we can define etale locales over the same locale (at least it seems to me : the notion of local homeomorphism of locales seems pretty easy to guess). Are they still the same (i.e. equivalent) ?

I could (easily) prove that given an etale locale over a given locale $X$ we may form a sheaf over $X$ in the obvious way (the "sheaf of sections") but the reverse direction is giving me more imaginative trouble : the construction I know for topological spaces of the etale space of a sheaf is not that easily transportable to locales (the construction I know uses stalks at points of the space, but the point of locales is to avoid points); at least not at first sight.

But I believe (hope ?) that there is such a construction and that if I was more comfortable with sheaves on a space I would probably see it; but it turns out I'm wondering about this before being comfortable with them, so I wanted to know: thus there are two questions :

Is it true that for a locale $X$, $\mathbf{Sh}(X)\simeq \mathrm{Etale}(X)$ (with obvious notations ) ? If it is, how may we construct the etale locale of a given sheaf over $X$ ?

Answer 1

This is indeed true. A high-level way of seeing this is as follows.

Given a sheaf $E$ over a locale $X$, we can form the slice topos $\mathrm{Sh}(X)/E$. The unique geometric morphism from this topos to $\mathrm{Set}$ is a localic geometric morphism since it can be written as the composition $\mathrm{Sh}(X)/E \to \mathrm{Sh}(X) \to \mathrm{Set}$ and each of the factors is a localic geometric morphism. Hence $\mathrm{Sh}(X)/E$ is of the form $\mathrm{Sh}(Y)$ for some unique locale $Y$. This locale is the étale locale associated to $E$.

It's also possible to describe the étale locale in explicit terms, though I never worked out the details. If I had to guess, my proposed description would look as follows. The étale locale associated to $E$ might be the classifying locale of the following propositional geometric theory (this means that the underlying frame is freely generated by the "atomic propositions" modulo the "axioms"):

• Atomic propositions: $\varphi_U$ (one for each open $U$ of $X$), $\psi_{U,s}$ (one for each section $s \in E(U)$ on some open $U$)
• Axioms:
  • $\varphi_U \vdash \varphi_V$ for each pair $(U,V)$ of opens such that $U \leq V$
  • $\top \vdash \varphi_\top$
  • $\varphi_U \wedge \varphi_V \vdash \varphi_{U \wedge V}$ for each pair $(U,V)$ of opens
  • $\varphi_{\bigvee_i U_i} \vdash \bigvee_{i \in I} \varphi_{U_i}$ for each family $(U_i)_i$ of opens
  • $\psi_{U,s} \vdash \varphi_U$ for each section $s \in E(U)$ on some open $U$
  • $\varphi_U \vdash \bigvee_{s \in E(U)} \psi_{U,s}$ for each open $U$
  • $\psi_{U,s|_U} \vdash \psi_{V,s}$ for each triple $(U,V,s)$ such that $U \leq V$ and $s \in E(V)$
  • $\psi_{U,s} \wedge \psi_{V,t} \vdash \bigvee\{ \psi_{W,f} \,|\, W \leq U \wedge V, s|_W = f, t|_W = f \}$ for each tuple $(U,V,s,t)$ such that $s \in E(U)$, $t \in E(V)$