Pullback of a scheme along the Frobenius morphism

Question

Let $S$ be an $\mathbb{F}_p$-scheme for a given prime $p$. Let $X$ be a scheme over $S$. Then, we can consider the Frobenius morphism of $X$ relative to $S$, defined by taking the unique morphism given by universal property from $X$ to $X^{(p)}:=X\times_{S,\phi} S$, where $\phi$ is the absolute Frobenius of $S$. Now, if we have another scheme $Y$, over $X^{(p)}$, and we consider its base change along Frobenius, this defines a scheme $Y\times_{X^{(p)}}X$, and a morphism $\psi:Y\times_{X^{(p)}}X\rightarrow Y$. Is it true that $Y\cong (Y\times_{X^{(p)}}X)^{(p)}$ and that the morphism $\psi$ is the Frobenius of $Y\times_{X^{(p)}}X$ relative to $S$? Thank you for any kind of suggestion!

Answer 1

No, this is false.

Counterexample 1: Take $S = X$. In this case, the relative Frobenius $X \rightarrow X^{(p)}$ is an isomorphism. Let $Y$ be any $S$-scheme such that the relative Frobenius $Y \rightarrow Y^{(p)}$ is not an isomorphism (e.g. $S = \mathbb{F}_p$ and $Y = \mathbb{A}^1$).

Counterexample 2: Take $S = \mathrm{Spec}~\mathbb{F}_p$ and let $X = \mathbb{A}^1$. We can identify $X^{(p)}$ with $X$, and the relative Frobenius $X \rightarrow X^{(p)}$ is induced by the ring map $\mathbb{F}_p[x] \rightarrow \mathbb{F}_p[x]$ given by $x \mapsto x^p$. Let $Y$ be any $S$-point of $X^{(p)}$. The fiber product $Y \times_{X^{(p)}} X$ is non-reduced, so your map $\psi$ is not an isomorphism. It thus cannot coincide with the relative Frobenius $Y \rightarrow Y^{(p)}$ (which is an isomorphism).