Universally closed implies proper for locales

Question

It is well known that:

Theorem. For a locale (resp. topological space) $X$, the following are equivalent:

• $X$ is compact, i.e. every open cover of $X$ has a finite subcover.

• For every locale (resp. topological space) $Y$, the projection $X \times Y \to Y$ is closed.

Question. Is there a "natural" locale (resp. topological space) $Y$ constructed from $X$ such that the projection $X \times Y \to Y$ is closed if and only if $X$ is compact? In other words, instead of checking universal closedness, does it suffice to check closedness of a particular morphism?

---

For topological spaces, there is a canonical choice (if you believe in the ultrafilter theorem, at least): take $Y$ to be the space of ultrafilters on $X$ and consider the convergence relation; closedness immediately implies that every ultrafilter on $X$ converges, which implies $X$ is compact. What about locales? Is there an intuitionistic proof?

It seems to me possible to improve the proof mentioned above, for topological spaces at least. Instead of the space of ultrafilters on $X$, take $Y$ to be the space of ideals of $\Omega (X)$, where $\Omega (X)$ is the frame of open subspaces of $X$ and "ideal" means downward-closed upward-directed subset. The basic open subsets of $Y$ are of the form ${\uparrow} \{ {\downarrow} \{ u \} \}$ (i.e. $\{ U \in Y : u \in U \}$) for $u \in \Omega (X)$. Consider the following open subspace $e$ of the product $X \times Y$: $$e = \bigvee \{ u \otimes {\uparrow} \{ {\downarrow} \{ u \} \} : u \in \Omega (X) \}$$

In the case $X$ is a topological space, $e$ corresponds to the following open subset: $$E = \{ (x, U) \in X \times Y : \exists u \in U . x \in u \}$$ Put it even more simply, $(x, U) \in E$ if and only if $x \in \bigcup U$. Define: $$\forall_\pi (E) = \{ U \in Y : \forall x \in X . (x, U) \in E \}$$ If $\forall_\pi (E)$ contains a basic open subset ${\uparrow} \{ {\downarrow} \{ u \} \}$, then $u$ must be $\top_X$, so the interior of $\forall_\pi (E)$ is just $\{ {\downarrow} \{ \top_X \} \}$. But if the projection $\pi : X \times Y \to Y$ is closed, then $\forall_\pi (E)$ is open, therefore any ideal of $\Omega (X)$ that is also an open cover of $X$ must be the trivial ideal – in other words, $X$ is compact. (Notice this argument makes no appeal to the ultrafilter characterisation of compactness – it even avoids the double-negations that frequently appear when working with closed subsets by working only with open subsets.)

Adapting the above argument for the case where $X$ is a locale is trickier: in the localic context, $\forall_\pi (e)$ is open by definition but does not immediately tell us anything about ideals of $\Omega (X)$ that are open covers. We have to instead consider the following pullback square, $$\require{AMScd} \begin{CD} X \times 1 @>{\operatorname{id} \times y}>> X \times Y \\ @V{X}VV @VV{\pi}V \\ 1 @>>{y}> Y \end{CD}$$ where $y : 1 \to Y$ is the morphism corresponding to the point $U \in Y$. Then, by definition, $${\uparrow} \{ {\downarrow} \{ u \} \} \cdot y \text{ is inhabited if and only if } u \in U$$ and therefore: $$e \cdot (\operatorname{id} \times y) = \bigvee \{ u \otimes ({\uparrow} \{ {\downarrow} \{ u \} \} \cdot y) : u \in \Omega (X) \} = \left( \bigvee U \right) \otimes \top$$ To show $X$ is compact, it suffices to verify: $$\forall_X (e \cdot (\operatorname{id} \times y)) = \forall_\pi (e) \cdot y$$ Unfortunately, this equality – which comes for free in the point set context because $\forall$ is defined differently – is itself a non-trivial consequence of properness! So this argument appears to beg the question...

Answer 1

It turns out that Vermeulen has essentially answered the question in [A note on stably closed maps of locales]. The argument there implies:

Theorem. Let $g : X \to S$ be a morphism of locales. The following are equivalent:

• $g : X \to S$ is proper, i.e. $g : X \to S$ is closed and the right adjoint $\forall_g : \Omega (X) \to \Omega (S)$ preserves joins of upward-directed subsets.

• The product morphisms $g \times \textrm{id}_Y : X \times Y \to S \times Y$ and $g \times \textrm{id}_\tilde{Y} : X \times \tilde{Y} \to S \times \tilde{Y}$ are both closed, where $Y$ is the locale of ideals of $\Omega (X)$ and $\tilde{Y}$ is the dissolution of $Y$, i.e. $\Omega (\tilde{Y}) = \textrm{Sub} (Y)^\textrm{op}$.

(We can take the disjoint union $Y \amalg \tilde{Y}$ to reduce to a single locale, but this seems less natural.)

---

The key idea in Vermeulen's argument seems to be to use these three features of the splitting cover $q : \tilde{Y} \to Y$:

1. The pullback along $q : \tilde{Y} \to Y$ of any subspace of $Y$ whatsoever is a closed subspace of $\tilde{Y}$.

2. Every closed subspace of $\tilde{Y}$ is the preimage of some subspace of $Y$.

3. The pullback of $q : \tilde{Y} \to Y$ along any morphism $Z \to Y$ whatsoever is an epimorphism.

In principle, any other locale $\tilde{Y}$ and morphism $q : \tilde{Y} \to Y$ with the same formal properties would work, but in fact the above completely characterises the dissolution locale.

To establish feature 3, Vermeulen relativises the notion of splitting cover by introducing a parameter $\mathcal{A} \subseteq \textrm{Sub} (Y)$ and replacing the "any subspace of $Y$" in feature 1 with "any member of $\mathcal{A}$". Feature 3 can then be split in two:

• $q : \tilde{Y} \to Y$ is an epimorphism.

• The pullback of $q : \tilde{Y} \to Y$ along any morphism $f : Z \to Y$ is an $\mathcal{A}'$-splitting cover of $Z$, where $\mathcal{A}'$ consists of the pullbacks along $f : Z \to Y$ of members of $\mathcal{A}$.

Using this, Vermeulen shows a Beck–Chevalley condition is obtained:

Lemma. Let $Y$ be any locale, let $\mathcal{A} \subseteq \textrm{Sub} (Y)$, and let $q : \tilde{Y} \to Y$ be an $\mathcal{A}$-splitting cover. Consider a pullback square: $$\require{AMScd} \begin{CD} \tilde{Z} @>{r}>> Z \\ @V{\tilde{f}}VV @VV{f}V \\ \tilde{Y} @>>{q}> Y \end{CD}$$ If both $f : Z \to Y$ and $\tilde{f} : \tilde{Z} \to \tilde{Y}$ are closed, then $$\exists_f (z \cap f^- (y)) = \exists_f (z) \cap y$$ for all closed subspaces $z$ of $Z$ and all $y \in \mathcal{A}$, where $f^- : \textrm{Sub} (Y) \to \textrm{Sub} (Z)$ is pullback and $\exists_f : \textrm{Sub} (Z) \to \textrm{Sub} (Y)$ is its left adjoint.

Corollary. The pullback of $f : Z \to Y$ along any member of $\mathcal{A}$ is closed.

(In fact, the corollary only depends on the conclusion of the lemma and the hypothesis that $f : Z \to Y$ itself is closed.)

Proof of the interesting part of the theorem, assuming the lemma. Let $Y$ be the space of ideals of $\Omega (X)$ and let $q : \tilde{Y} \to Y$ be the (absolute) splitting cover. Then $\textrm{id}_X \times q : X \times \tilde{Y} \to X \times Y$ is a (relative) splitting cover. Consider the following pullback diagram: $$\begin{CD} X \times 1 @>{\textrm{id}_X \times y}>> X \times Y \\ @V{g \times \textrm{id}_1}VV @VV{g \times \textrm{id}_Y}V \\ S \times 1 @>>{\textrm{id}_S \times y}> S \times Y \end{CD}$$ Applying the lemma, we have the following equation in $\textrm{Sub} (S \times Y)$: $$\exists_{g \times \textrm{id}_Y} (w \cap (\top_X \times y)) = \exists_{g \times \textrm{id}_Y} (w) \cap (\top_S \times y)$$ Hence, in $\textrm{Sub} (S \times 1)$: $$\exists_{g \times \textrm{id}_1} ((\textrm{id}_X \times y)^- (w)) = (\textrm{id}_S \times y)^- (\exists_{g \times \textrm{id}_Y} (w))$$ Restricting to the case where $w$ is a closed sublocale of $X \times Y$ and using the fact that $g \times \textrm{id}_Y : X \times Y \to S \times Y$ (by hypothesis) and $g \times \textrm{id}_1 : X \times 1 \to S \times 1$ (by the corollary) are closed, we obtain (by taking open complements) in $\Omega (S \times 1)$: $$\forall_{g \times \textrm{id}_1} (e \cdot (\textrm{id}_X \times y)) = \forall_{g \times \textrm{id}_S} (e) \cdot (\textrm{id}_S \times y)$$ Let $U$ be the point of $Y$ (= ideal of $\Omega (X)$) selected by $y : 1 \to Y$. Unwinding definitions, we find $$t \otimes \top \le \forall_{g \times \textrm{id}_1} (e \cdot (\textrm{id}_X \times y)) \text{ if and only if } t \cdot g \le \bigvee U$$ $$t \otimes \top \le \forall_{g \times \textrm{id}_S} (e) \cdot (\textrm{id}_S \times y) \text{ if and only if } \forall u \in U . t \cdot g \le u$$ therefore: $$\forall_g \left( \bigvee U \right) = \bigvee \{ \forall_g (u) : u \in U \}$$ Since $y$ (hence $U$) is arbitrary, we conclude that $\forall_g : \Omega (X) \to \Omega (S)$ preserves joins of upward-directed subsets, as required.