Let $f : X \to Y$ be an open (and continuous) map of locales. Suppose the relative diagonal $\Delta_f : X \to X \times_Y X$ is an open embedding of locales. Does it follow that $f : X \to Y$ is a local homeomorphism?

The answer is yes if I replace "locale" with "topological space". Indeed, by the definition of the product topology, there must exist an open covering of the image of $\Delta_f$ by "rectangles", i.e. open subspaces of the form $U \times_Y V \subseteq X \times_Y X$ for open subspaces $U \subseteq X$, $V \subseteq X$; but if $U \times_Y V \subseteq \operatorname{im} \Delta_f$, then the restriction $f : U \cap V \to Y$ must be injective, hence is an open embedding (because $f : X \to Y$ is an open map). But $\{ U \cap V : U \times_Y V \subseteq \operatorname{im} \Delta_f \}$ is an open covering of $X$, so we are done.

In fact, everything in the above argument goes through for locales, except for the very last step where I assert that we have an open covering of $X$. There, I have used the fact that a collection of open subspaces is an open covering if and only if every point is contained in some member of the collection. So the argument would work if $X$ is a spatial locale. But can we avoid the use of points?

For reference, here are some standard definitions:

The **image** of a locale morphism $f : X \to Y$ is the locale $\operatorname{Im} f$ corresponding to the frame
$$\Omega (\operatorname{Im} f) = \{ v \in \Omega (Y) : f_* (f^* (v)) = v \}$$
where $f^* : \Omega (Y) \to \Omega (X)$ is the frame homomorphism corresponding to $f : X \to Y$ and $f_* : \Omega (X) \to \Omega (Y)$ is the right adjoint; the "inclusion" $\operatorname{Im} f \hookrightarrow Y$ corresponds to the frame homomorphism $v \mapsto f_* (f^* (v))$.

An **open sublocale** of a locale $Y$ is a locale $Y_v$ that corresponds to a frame of the form
$$\Omega (Y_v) = \{ v' \in \Omega (Y) : v' \le v \}$$
for some $v \in Y$; the "inclusion" $Y_v \hookrightarrow Y$ corresponds to the frame homomorphism $v' \mapsto v' \land v$.

An **open embedding** of locales is a morphism $f : X \to Y$ that is isomorphic to the inclusion of some open sublocale of $Y$.

An **open map** of locales is a morphism $f : X \to Y$ such that the image of every open sublocale of $X$ is an open sublocale of $Y$.

A **local homeomorphism** of locales is a morphism $f : X \to Y$ for which there is a set $\mathfrak{U} \subseteq \Omega (X)$ such that:

- $\sup \mathfrak{U} = \bigvee_{u \in \mathfrak{U}} u = \top$.
- For each $u \in \mathfrak{U}$, the composite $X_u \hookrightarrow X \to Y$ is an open embedding.

Stone spaces. $\endgroup$ – Zhen Lin Apr 9 '15 at 12:18Stone spacesmaybe you could include the definition in the post such that it is more clear. $\endgroup$ – Dominic van der Zypen Apr 9 '15 at 13:09Stone spaces, so I have added it. $\endgroup$ – Zhen Lin Apr 10 '15 at 0:53