Product of topological spaces and product of corresponding locales 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?
 A: 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


*

*Jorge Picado, Aleš Pultr. Notes on the product of locales. Mathematica Slovaca 65.2 (2015): 247-264. PDF

*Jorge Picado and Aleš Pultr. Frames and Locales: topology without points. Springer Science & Business Media, 2011.

