Let $k$ be a field, and let $X$ be a scheme over $k$. Let $f:k\to k$ be the embedding of fields defined by $f(\lambda)=\lambda^p$. Define the first Frobenius twist of $X$ to be the scheme $X\times_f k$, where we consider $\operatorname{spec}k$ as a scheme over itself via $f$. The first Frobenius twist can be viewed as a functor from the category of schemes over $k$ to itself.
I'd like to show that the bifunctors $(-\times_k-)^{(1)}$ and $(-)^{(1)}\times_k(-)^{(1)}$ are naturally isomorphic. To do so, for any schemes $X$ and $Y$, I need to define an isomorphism
$$\varphi_{X,Y}:(X\times_kY)\times_fk\to(X\times_fk)\times_k(Y\times_fk)$$
I don't know how to think about schemes very well, so I've resorted to using the universal property of the fiber product many different times to arrive at some fairly large and complicated commutative diagrams in order to define $\varphi_{X,Y}$. Even though this method gives me the existence of such a morphism, it is not clear to me how to show this is an isomorphism (perhaps larger commutative diagrams, which would be horrible).
I would like to know if there is a better way to think about the above canonical identification, or in other words, how would someone well-versed in algebraic geometry solve my exercise (if at all!).
In the affine case, I can think of the isomorphism of commutative $k$-algebras
$$(k[X]\otimes_fk)\otimes_k(k[Y]\otimes_fk)\cong(k[X]\otimes_kk[Y])\otimes_fk$$
but I'd like to be able to think in the language of general schemes (I'm always more comfortable in the affine case, because all of the information is contained in a nice, concrete $k$-algebra).
Essentially, what you state in the affine case globalizes.
What follows works for $S$ any scheme over $\mathbb F_p$. In our case we can take $S=\textrm{Spec }k$. Let $f^\ast:S'\to S$ be the morphism corresponding to the Frobenius endomorphism (Here, $S'$ is $S$, with the new structure given by $f$). Then, for an $S$-scheme $X$, when we form the fiber product $X^{(1)}=X\times_SS'$, the structural morphism of this scheme is the second projection onto $S'$, so $S'$ is the scheme over which $X^{(1)}$ and $Y^{(1)}$ are defined. This said, we have, as $S'$-schemes, \begin{align} (X\times_SY)^{(1)}&\overset{\textrm{def}}{=}(X\times_SY)\times_SS'\cong X\times_S(Y\times_SS')=X\times_S Y^{(1)}\cong X\times_{S}(S'\times_{S'}Y^{(1)})\notag\\ &\cong (X\times_SS')\times_{S'}Y^{(1)}=X^{(1)}\times_{S'} Y^{(1)}. \end{align} This is also an isomorphism over $S$.