If $X/S$ is smooth of relative diemsnion $n$ over characteristic $p$, then $F_{X/S}$ is finite locally free of rank $p^n$?

Question

Given a morphism $f:X\to Y $, we say $f$ is finite locally free of rank $k$ if $f_* \mathcal{O}_X$ is locally free of rank $k$ as an $\mathcal{O}_Y$-module. see this tag for details about finite locally free morphism.

See this tag for details about relative Frobenius morphism

Let $S$ be a scheme of characterisctic $p$, and $f:X\to S$ be a smooth morphism of relative dimension $n$, (so locally it factors through $\mathbb{A}^n_S$, $U\stackrel{etale}{\to} \mathbb{A}_S^n\to S$), then we want to show that the relative Frobenius morphism $F_{X/S}$ is finite locally free of rank $p^n$.

Since this question is local, We can assume $X\stackrel{etale}{\to} \mathbb{A}_S^n\to S$. It is not hard to show $F_{\mathbb{A}^n_S/S}$ is finite locally free of rank $p^n$, but I can't relate it with $F_{X/S}$.

Answer 1

It's not hard to see that the three squares are cartesian. Since $X/\mathbb{A}_S^n$ is étale, $F_{X/\mathbb{A}_S^n}$ is an isomorphism. Then $F_{X/S}$ is a base change of $F_{\mathbb{A}_S^n/S}$ which is already finite locally free of rank $p^n$. For detail, see this link.