Relative local compactness for locales? I am looking for informations on the relative version of local compactness for locales:
If $f:X \rightarrow Y$ is a morphism of locales I want to say that $f$ is relatively locally compact if internally in the topos $Sh(Y)$, $X$ is a locally compact locale.
It is equivalent to the fact that $X$ is exponentiable in the category $Locale/Y$ of locales over $Y$. This shows that it is an interesting notion and that it has some stability properties (at least stability under composition and pullback). But I haven't been able to find a simple characterization of this notion not involving internal logic.
In fact, I am mostly after an explicit characterization of those maps:
For example I have not been able to understand when a map between two finite locale satisfies this condition ? (by finite locale, I mean corresponding to a finite frame)
Also, what does it means for a locale $X$ that the map $X \rightarrow X \times X$ satisfies this condition ?
I have been able to get an answer for open maps:
if $f$ is an open map, then $f$ is relatively locally compact if for every $b \in \mathcal{O}(X)$ one has:
$$ b = \bigcup_{a <<_Y B} a $$
Where $a <<_Y b$ is a relative way beow relation defined by: if $I$ is a binary join stable, downard directed, subset of $\mathcal{O}(X)$ such that $ b = \bigcup I$ and  $( \forall i,x \wedge f^*(u_i) \in I) \Rightarrow x \wedge \bigcup f^*(u_i) \in I$; then $a \in I$.
 A: I finally have been able to handle the case of inclusions which already gives some examples and settle the case of diagonal maps very well, but if someone can do better I would still be very interested to know.
By "Hausdorff locale" I mean a locale with a closed diagonal.
Lemma: If $A$ is a locally compact locale, $X$ is a Hausdorff locale and $A \subset X$ is an inclusion, then $A$ is locally closed in $X$ (i.e. $A$ is open in $\overline{A}$ or $A$ is the intersection of a closed and an open sublocale).
The proof is exactly the same as for ordinary topological spaces (and is constructive).
Prop : An inclusion $i:A \hookrightarrow X$ is relatively locally compact if and only if $A$ is locally closed in $X$.
Proof: internally in $sh(X)$, the terminal locale is always Haussdorff, so if $A$ is locally compact internally in $sh(X)$ it is internally locally closed in the terminal sublocale, but this implies that externally $A$ locally closed in $X$. Conversely, if $A$ is exeternaly locally closed in $X$ then $A$ is internally locally closed in the terminal locale which is locally compact and Hausdorff hence $A$ is internally locally compact.
Corollary: The diagonal map of a locale $X$ is relatively locally compact if and only if $X$ is locally Hausdorff.
Proof: If $\Delta$ is locally closed in $X \times X$, then there is an open sublocale $U \subset X \times X$ such that $\Delta \subset U$ is a closed inclusion. As any other open sublocale of $X \times X$, one can write $U = \bigcup A_i \times B_i$ for $A_i,B_i$ open sublocales of $X$. Now as $\Delta \subset U$ one has $X = \Delta^* U = \bigcup A_i \wedge B_i $ and if $V_i= A_i \wedge B_i$ then $V_i \times V_i \subset U$ hence $\Delta_{V_i} = \Delta \wedge V_i \times V_i$ is closed in $V_i \times V_i$, hence $V_i$ is a covering of $L$ by open Hausdorff sublocale. The converse works essentially the same.
As an other corollary, one has plenty of examples of maps of finite locale that are not locally compact ! (for example the diagonal of any non discrete finite locales)
