The Stacks project

Proof. First, suppose that $P' = A[y_1, \ldots , y_ m]$ is a polynomial algebra over $A$. In this case, we can find ring maps $P \to P'$ and $P' \to P$ compatible with the maps to $C$ which induce maps $a : D \to D'$ and $b : D' \to D$ as in the lemma. Using completed base change along $a$ and $b$ we obtain functors between the categories of modules with connection satisfying properties (1), (2), (3), and (4) simply because these these categories are equivalent to the category of quasi-coherent crystals by Proposition 60.17.4 (and this equivalence is compatible with the base change operation as shown in the proof of the proposition).

Proof for general smooth $P'$. By the first paragraph of the proof we may assume $P = A[y_1, \ldots , y_ m]$ which gives us a surjection $P \to P'$ compatible with the map to $C$. Hence we obtain a surjective map $a : D \to D'$ by functoriality of divided power envelopes and completion. Pick $e$ large enough so that $D_ e$ is a divided power thickening of $C$ over $A$. Then $D_ e \to C$ is a surjection whose kernel is locally nilpotent, see Divided Power Algebra, Lemma 23.2.6. Setting $D'_ e = D'/p^ eD'$ we see that the kernel of $D_ e \to D'_ e$ is locally nilpotent. Hence by Algebra, Lemma 10.138.17 we can find a lift $\beta _ e : P' \to D_ e$ of the map $P' \to D'_ e$. Note that $D_{e + i + 1} \to D_{e + i} \times _{D'_{e + i}} D'_{e + i + 1}$ is surjective with square zero kernel for any $i \geq 0$ because $p^{e + i}D \to p^{e + i}D'$ is surjective. Applying the usual lifting property (Algebra, Proposition 10.138.13) successively to the diagrams

we see that we can find an $A$-algebra map $\beta : P' \to D$ whose composition with $a$ is the given map $P' \to D'$. By the universal property of the divided power envelope we obtain a map $D_{P', \gamma }(J') \to D$. As $D$ is $p$-adically complete we obtain $b : D' \to D$ such that $a \circ b = \text{id}_{D'}$.

Consider the base change functors

on modules with connections satisfying (1), (2), and (3). See Remark 60.6.9. Since $a \circ b = \text{id}_{D'}$ we see that $F \circ G$ is the identity functor. Let us say that $(M', \nabla ')$ has property (4) if this is true for $G(M', \nabla ')$. A formal argument now shows that to finish the proof it suffices to show that $G(F(M, \nabla ))$ is isomorphic to $(M, \nabla )$ in the case that $(M, \nabla )$ satisfies all four conditions (1), (2), (3), and (4). For this we use the functorial isomorphism

of the proof of Proposition 60.17.4 (which requires the topological quasi-nilpotency of $\nabla $ which we have assumed). It remains to prove that this map is horizontal, i.e., compatible with connections, which we omit.

The last statement of the proof now follows. $\square$