# The etale locale of a sheaf?

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$ ?

• I would recommend section 1.1, 'A crash course in sheaf theory', from Chapter V of Johnstone's book "Stone Spaces". It provides a more or less explicit description of the equivalence: if $F$ is a sheaf then you get the display space by quotienting the disjoint union of $Fa \times a$ over every open $a$ of your base locale $X$. (Treat $Fa$ as a discrete locale.) The other direction (i.e. getting the sheaf from the display space) is the same as the usual topological situation - you take the sections of each open. This 'crash course' is only 11 short pages, It is a really remarkable and succinct – Christopher Townsend Nov 1 '18 at 14:18

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)$$
• Thank you for your answer ! I don't know enough topos theory to appreciate the high level answer but I understand the second one, though (and this shows maybe I don't understand it so well) it seems to me that the $\varphi_U$ are redundant in a way - is there a reason for adding them ? And can the high level give a high level explanation of why $Y$ is a spatial locale when $X$ is a space ? – Max Oct 3 '18 at 18:25