Product of topological spaces and product of corresponding locales

Question

Let $\Omega : \mathbf{Top} \to \mathbf{Loc}$ the functor that takes a topological space to its locale of opens. For a locale morphism $f$, write $f^*$ for the correspoding morphism in $\mathbf{Frm}$, the category of frames and frame homomorphisms. Let $\times_t$ denote the product in $\mathbf{Top}$ and $\times_{\ell}$ the product in $\mathbf{Loc}$ (= the coproduct in $\mathbf{Frm}$).

Let $X$ and $Y$ be topological spaces. We can describe $\Omega X \times_{\ell} \Omega Y$ as the locale generated by pairs $[a, b]$, where $a \in X$ and $b \in Y$, subject to the relations \begin{align*} &[\top, \top] = \top \\ &[a, b] \wedge [a', b'] = [a \wedge a', b \wedge b'] \\ &[a, \bigvee S] = \bigvee \{ [a, b] \mid b \in S \} \\ &[\bigvee T, b] = \bigvee \{ [a, b] \mid a \in T \} \end{align*} where $T \subseteq X$ and $S \subseteq Y$.

Define $f : \Omega(X \times_t Y) \to \Omega X \times_{\ell} \Omega Y$ by $$ f^*([a, b]) = a \times b, $$ where $a \times b$ denotes the open rectangle in $X \times_t Y$. Then it is easy to verify that $f^*$ is a frame homomorphism, hence $f$ is a locale morphism. Furthermore, $f^*$ is onto, since the topology of $X \times_t Y$ is generated by a base consisting of open rectangles $a \times b$.

Question: Is $f$ an isomorphism? In other words, is $f^*$ injective?

Answer 1

Your map $f$ is known to be an injective dense localic map. See, for example, Proposition 4.2.2 in [1]. In general, it isn't an isomorphism. The reason for this is that $\Omega(X \times_t Y)$ is quotiented by more equations than $\Omega(X) \times_\ell \Omega(Y)$ is.

We can think of $\Omega(X \times_t Y)$ as if it was generated from the same set of generators as $\Omega(X) \times_\ell \Omega(Y)$ but quotiented with respect to the following equation:

$$ \bigvee_i [U_i, V_i] \sim \bigvee_j [U'_j, V'_j] \quad\text{ iff }\quad \bigcup_i (U_i\times V_i) = \bigcup_j (U'_j \times V'_j). $$

The right-hand size is computed with respect to the points of $X\times Y$. It is easy to see that $\sim$ is a stronger relation than the one that defines $\Omega(X) \times_\ell \Omega(Y)$.

It is also known that, if $X$ and $Y$ are sober locally compact, then $f$ is an isomorphism. (Proposition 4.4.1. in [1]).

In many ways, the frame-theoretic product behaves the same way as the tensor product of abelian groups. For details see [1,2].

References

1. Jorge Picado, Aleš Pultr. Notes on the product of locales. Mathematica Slovaca 65.2 (2015): 247-264. PDF
2. Jorge Picado and Aleš Pultr. Frames and Locales: topology without points. Springer Science & Business Media, 2011.