The Stacks project

Proof. Let $A$ be an $S$-algebra which is a complete local Noetherian ring with maximal ideal $\mathfrak m$ whose residue field $k$ is of finite type over $S$. We have to show that the category of objects over $A$ is equivalent to the category of formal objects over $A$. Since we know this holds for the category $\mathcal{S}_ B$ fibred in sets associated to $B$ by Artin's Axioms, Lemma 98.9.5, it suffices to prove this for those objects lying over a given morphism $\mathop{\mathrm{Spec}}(A) \to B$.

Set $X_ A = \mathop{\mathrm{Spec}}(A) \times _ B X$ and $X_ n = \mathop{\mathrm{Spec}}(A/\mathfrak m^ n) \times _ B X$. By Grothendieck's existence theorem (More on Morphisms of Spaces, Theorem 76.42.11) we see that the category of coherent modules $\mathcal{F}$ on $X_ A$ with support proper over $\mathop{\mathrm{Spec}}(A)$ is equivalent to the category of systems $(\mathcal{F}_ n)$ of coherent modules $\mathcal{F}_ n$ on $X_ n$ with support proper over $\mathop{\mathrm{Spec}}(A/\mathfrak m^ n)$. The equivalence sends $\mathcal{F}$ to the system $(\mathcal{F} \otimes _ A A/\mathfrak m^ n)$. See discussion in More on Morphisms of Spaces, Remark 76.42.12. To finish the proof of the lemma, it suffices to show that $\mathcal{F}$ is flat over $A$ if and only if all $\mathcal{F} \otimes _ A A/\mathfrak m^ n$ are flat over $A/\mathfrak m^ n$. This follows from More on Morphisms of Spaces, Lemma 76.24.3. $\square$