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?



Product of topological spaces and product of corresponding locales
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](https://eg.uc.pt/bitstream/10316/43902/1/products%28revised%29.pdf)
2. Jorge Picado and Aleš Pultr. *Frames and Locales: topology without points.* Springer Science & Business Media, 2011.


