I am trying to understand the proof of Cartier’s theorem on pages 370-371 (pages 17-18 of the PDF file) of Katz’s “Nilpotent connections and the monodromy theorem: applications of a result of Turrittin”, but I am stuck.

For simplicity, let us assume that we are given a smooth scheme $S$ over $\mathbb{F}_p$. Let $S^{(p)}$ denote the fibre product of the absolute Frobenius of $\mathbb{F}_p$ and the structure map of $S$ as an $\mathbb{F}_p$-scheme, and $F$ the relative Frobenius map. We want to prove that there is an equivalence of categories between the category of quasi-coherent sheaves on $S^{(p)}$ and the category of sheaves of $\mathcal O_S$-modules on $S$ with integrable ($\mathbb{F}_p$-)connection whose $p$-curvature is $0$. The functor in the forward direction simply maps a quasicoherent sheaf $\mathscr F$ on $S^{(p)}$ to its pullback $F^*\mathscr F$ under the relative Frobenius and the functor in the reverse direction maps a pair $(E, \nabla)$ to $E^{\nabla}$, the sheaf of germs of horizontal sections of $(E, \nabla)$. To prove the result, he shows that the canonical mapping of $\mathcal O_S$-modules from the pullback of $E^{\nabla}$ (under $F$) to $E$ is an isomorphism. I cannot understand *how* he does that; in particular, the construction he gives is completely opaque to me. Could you please explain the *main idea* of the proof to me? Any hints on why the claims he makes along the way are true would also be appreciated. If you could point me to alternative proofs of the theorem, that would be great!

Are there any standard books that contain the proof of this theorem? I have seen at least one version of it stated without proof in the language of $D_S$-modules. Are there any references that I could look at for complete proofs of these and other related results?