Dwork's lemma: a Frobenius lift gives a section R → W(R)

Let $R$ be a commutative ring, let $p$ be a prime, assume that the image of $p$ in $R$ is a non-zero-divisor, and let $\sigma \colon R \to R$ be a ring endomorphism with $\sigma(a) - a^p \in (p)$ for every $a \in R$, i.e. $\sigma$ lifts the $p$-power Frobenius modulo the principal ideal generated by $p$. The assertion is the existence of a ring homomorphism $s \colon R \to W(R)$ into the ring of $p$-typical Witt vectors of $R$ such that for every $a \in R$ and every $n \in \mathbb{N}$ the $n$-th ghost component of $s(a)$ equals the $n$-th iterate $\sigma^n(a)$ (iteration of the underlying function of $\sigma$, with $\sigma^0 = \mathrm{id}$). In particular, taking $n = 0$, the zeroth ghost component of $s(a)$ is $a$, so $s$ is a section of the projection $W(R) \to R$ onto the zeroth coefficient. The statement provides existence only; no uniqueness of $s$ is asserted, although it follows from the hypothesis on $p$.

This is the Cartier–Dieudonné–Dwork lemma: on a ring in which $p$ is a non-zero-divisor, a Frobenius lift determines a $\delta$-ring structure and hence a ring-theoretic section into Witt vectors, the ghost components being the iterates of the lift. It is used in the project for constructions of $\mathbb{Z}_p$-actions and gradings on Cartier and formal-module data, such as MvFormalGroup.CartierModule.exists_zp2Action_of_graded_frobenius_expansion and the complementarity results for graded pieces in CerednikDrinfeld.FormalODModule.