Convergence of localic maps

Question

We can define a limit of a sequence of points in a locale in the usual way: $x$ is a limit of $\{ x_i \}_{i \in \mathbb{N}}$ if, for every open $U$ containing $x$, there exists $N$ such that $x_n$ belongs to $U$ for every $n > N$. Now, let's say that we have a sequence of localic maps $\{ f_i : X \to Y \}_{i \in \mathbb{N}}$. Can we define a limit of such a sequence? For topological spaces, we can use pointwise convergence. Of course, we can do the same thing for locales, but it seems less natural and I don't think we can do much with such a definition.

If $X$ is exponential, then we can consider $f_i$ as points in the locale $Y^X$, so we can apply the definition that I gave before. The problem here is that the definition of $Y^X$ is rather complicated and I'm not sure how to prove anything about such a notion of convergence (like uniqueness) or how to prove that any given specific sequence of maps converges to something. So, is this definition a reasonable one or is there some other definition of convergence for localic maps? It's OK to assume that $X$ and $Y$ satisfy some properties like Hausdorffness or metrizability.

Answer 1

There is a pretty good notion of convergence of maps of locales, though I have never seen anything in the literature about it (maybe I should write something about it ?).

A map of locale $f:X \to Y$ can be thought of as a point of $Y$ in the internal logic of the sheaf topos $Sh(X)$. And a sequence/net of such maps $(f_i)_{i\in I}$ can be thought of as an $I$-indexed sequence of points of $Y$ in the internal logic of $Sh(X)$.

Definition 1: I say that the sequence/net $(f_i)_{i\in I}$ converge to $f$ if the statement "$(f_i)_{i\in I}$ converge de $f$ as points of $Y$" holds in the internal logic of the topos $Sh(X)$.

If you are fluent in internal/external translation, it is not too hard to write down explicitly what this means:

Definition 2: $(f_i)_{i\in I}$ converge to $f$, if for each open $U \in \mathcal{O}(Y)$ there exists a covering $(V_j)$ of $f^*(U)$ and for each $j$ an index $i_j \in I$ such that for all $i > i_j$, $V_j \subset f_i^*(U)$.

And you can use definition 2 as your starting point if you don't like internal logic. Note that definition $2$ can also be written in the more compact, though harder to read way:

Definition 3: $(f_i)_{i \in I} \to f$ if for all $U \in \mathcal{O}(Y)$ one has

$$ f^* U \subset \bigcup_{i\in I} \left( \bigcap_{j>i} f_j^*(U) \right) $$

It is easy to see that if $X$ is compact then this is the same as uniform convergence and if $X$ is locally compact then this corresponds to uniform convergence on all compacts.

It seems the analogue notion for topological spaces has been studied under the name "continuous convergence". I had mention this a few years ago in another MO answer. (I had given a reference in this other answer, but I honestly don't remember it).

There is also another point of view on this notion of convergence which is quite convenient. I'll restrict to $I = \mathbb{N}$ for simplicity. I'm writting $\overline{\mathbb{N}}$ for the topological space $\mathbb{N} \cup \{ \infty \}$ with the topology whose open are all subsets of $\mathbb{N}$ and all subsets containing $\infty$ and all large enough integer. So a continuous map $f:\overline{\mathbb{N}} \to X$ is the same as a sequence of points $(f(n))_{n\in \mathbb{N}}$ that converge to $f(\infty)$. Then we have:

Proposition: A sequence of maps of locale $(f_n:X \to Y)_{n \in \mathbb{N}}$ converge to $f :X \to Y$ in the sense above if and only if there exists a map of locale $F: X \times \overline{\mathbb{N}} \to Y$ such that $F$ restricted to $X \times \{n\}$ is $f_n$ and $F$ restricted to $X \times \{\infty\}$ if $f$.

I feel like writting the details of the proof would be a bit too long for an MO answer, but a key point if you are trying to prove it is that one can describe explicitly the locale $X \times \overline{\mathbb{N}}$ : an open is a collection $(U_i)_{i \in \overline{\mathbb{N}}}$ such that:

$$U_\infty \subset \bigcup_{n \in \mathbb{N}} \left( \bigcap_{m >n} U_m \right) $$

In particular, if $X$ is exponentiable, then as a morphism $X \times \overline{\mathbb{N}} \to Y$ is the same as a morphism $\overline{\mathbb{N}} \to Y^X$, one deduces that:

Corollary: If $X$ is exponentiable, then a sequence of function $f_n:X \to Y$ converge to $f:X \to Y$ in the sense above if and only if $f_n$ converge to $f$ as points of $Y^X$.