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

  • $\begingroup$ 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 $\endgroup$ – Christopher Townsend Nov 1 '18 at 14:18
  • $\begingroup$ +1 for "the point of locales is to avoid points" :D $\endgroup$ – mattecapu May 30 '20 at 15:56

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)$
  • $\begingroup$ 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 ? $\endgroup$ – Maxime Ramzi Oct 3 '18 at 18:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.