Is formal smoothness a local property?

Is the following statement true?

Let $R\to S$ be a morphism of commutative rings giving $S$ an $R$-algebra structure. Suppose that the induced maps $R\to S_{\mathfrak{p}}$ are formally smooth for all prime ideals $\mathfrak{p}\subset S$. Then $R\to S$ is formally smooth.

I've looked all over, and I have not been able to find a proof or counterexample for this claim. It might even be an open problem. This statement is true for formally unramified and formally étale morphisms, but the proof for formally étale morphisms uses the fact that the module of Kähler differentials is $0$, so it doesn't seem like the same approach will work for the formally smooth case.

-
The cotangent complex seems to be natural tool for this, via which it should suffice to show projectivity of $R$-module $\Omega^1_ {R/S}$ can be checked on stalks. In other words, one strategy is to determine criteria for when projectivity of some module (without finiteness hypotheses) can be checked on stalks. That sounds hopeless, but familiarity with the techniques of the unique paper of Raynaud and Gruson would seem to be an essential prerequisite for thinking seriously about this (but I do not recommend it; this is a time-waster just like the "weird" spaces of intro point-set topology). – BCnrd Apr 24 '10 at 2:50
Very interesting. – Harry Gindi Apr 24 '10 at 4:03
Does anyone understand the proof of the claim (EGA IV 17.1.6) that formal smoothness is local (in the Zariski topology)? The authors refer to 16.5.17 but to me it seems that what they really are referring to is 16.5.18 and there they have explicitly made the assumption that $\Omega^1_{X/Y}$ should be locally finitely presented an assumption which is not part of 17.1.6. Until I understand that proof I am not sure I believe the statement that formal smoothness is local which should be weaker than what you ask. – Torsten Ekedahl Apr 24 '10 at 5:53
Yes, there is a gap in the proof of 17.1.6 in EGA because the surprisingly difficult statement about projectivity was not proven until Raynaud-Gruson. The details are available at mathoverflow.net/questions/10731/… . Even though the claim is true, it is very different from the question that I'm asking here, which is an even sharper characterization (i.e. we can check the condition on stalks). – Harry Gindi Apr 24 '10 at 6:45

I think this works. Suppose we have a ring $R$ and an $R$-module $M$ all of whose localisations are projective and consider $S=S^\ast_RM$, the symmetric algebra on $M$. Then $R \rightarrow S$ is formally smooth precisely when $M$ is projective. Let $\mathfrak p$ be a prime ideal of $S$ and $\mathfrak q$ the prime ideal of $R$ lying below $\mathfrak p$. Then $S_{\mathfrak p}$ is a localisation of $S_{\mathfrak q}=S^\ast_{R_{\mathfrak q}}M_{\mathfrak q}$ which is a formally smooth $R_{\mathfrak q}$-algebra and hence $S_{\mathfrak p}$ is a formally smooth $R$-algebra (localisations being formally étale). To show that the statement is false it thus is enough to find a non-projective $R$-module all of localisation are projective.
If $R$ is a boolean ring (i.e., $r^2=r$ for all $r\in R$) then all its localisations are isomorphic to $\mathbb Z/2$ all of whose modules are projective. Hence it suffices to find a boolean ring $R$ and a non-projective $R$-module. This is easy: Let $S$ be a totally disconnected compact topological space and $s\in S$ a non-isolated point and put $R$ equal to the boolean ring of continuous maps $S \rightarrow \mathbb Z/2$. Evaluation at $s$ gives a ring homomorphism $R \rightarrow \mathbb Z/2$ making $\mathbb Z/2$ an $R$-module. If it were projective there would be a module section $\mathbb Z/2 \rightarrow R$. Let $e$ be the image of $1$. Then for any $f\in R$ we have $fe=f(s)e$. This means that $e$ must be the characteristic function of $s$. Indeed, as $e \mapsto 1$ under evaluation at $s$ we have $e(s)=1$. On the other hand, if $t\neq s$ there is an $f\in R$ with $f(t)=1$ and $f(s)=0$ giving $e(t)=f(t)e(t)=f(s)e(t)=0$. Hence $\{s\}=\{t\in S:e(t)=1\}$ is open so that $s$ is isolated.
Note that we may take for $S$ any infinite compact totally disconnected set as some point of it must be non-isolated. Nice examples are the Cantor set (all of whose points are non-isolated) and the spectrum of $\prod_T\mathbb Z/2$ for any infinite set $T$ (which is the ultrafilter compactification of $T$, any non-principal ultrafilter is non-isolated I think).