Is an open map with open relative diagonal necessarily a local homeomorphism?

Question

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.

Answer 1

The answer is yes.

It appears for example as lemma C3.1.15 in Johnstone's sketches of an elephant.

Roughly, it can be proved by working in the internal logic of the target (hence assuming that the target is a point) and considering open subspaces $U$ of $X$ such that $U \times U \subset \Delta$, on can then show that such $U \times U$ cover the diagonal, hence the $U$ cover $X$ and that if they are positive they correspond to isolated points of $X$.

The proof in Johnstone's book is an external formulation of this argument and hence looks a bit more technical.

Edit : I didn't read your post well enough and didn't see you already proposed a proof. The trick you are missing is I think the following: If the $U \times V$ form a covering of $\Delta$ then the $\Delta^{-1}(U \times V)$ form a covering of $X$, and $\Delta^{-1}(U \times V) = U \cap V$.