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?