EGA IV 17.1.6(i) states that formal smoothness is a source-local property. In other words, a map $X\to Y$ of schemes is formally smooth if and only if there is an open cover $U_i$ ($i\in I$) of $X$ such that each restriction $U_i\to Y$ is formally smooth.

It seems however that there is a gap in the proof. The problem is in the third paragraph on page 59 (Pub IHES v 32). The reference to (16.5.17) does not give the conclusion they need. Corollary (16.5.18) does give this conclusion, but it requires a finite presentation assumption. (So, everything is OK for smoothness instead of formal smoothness.)

Quesiton 1: Can someone give a counterexample or a complete proof of 17.1.6(i)? (My bet would be that there's a counterexample.)

I think the right way of fixing this is to change the definition of formal smoothness. Recall that a map $X\to Y$ is said to be formally smooth if for any closed immersion $X'\to Y'$ of affine schemes defined by a square-zero ideal and for map $X'\to X$ and $Y'\to Y$ making the induced square commute, there is a map $Y'\to X$ commuting with all the other maps in the diagram. I think a better definition would to require only that the map $Y'\to X$ exists *locally* on $Y'$.

If I'm not mistaken, this definition has the following advantages over the old one: a) The definition of smoothness (=formally smooth and locally of finite presentation) would remain unchanged. b) It would make formal smoothness a source-local property. (Or if there is no counterexample to 17.1.16(i), then the argument with the new definition would be much easier than an argument like the one in EGA, in that it would not depend on the facts in scheme theory that the sheaf of lifts $Y'\to X$ is a torsor for a sheaf derivations and that therefore, since $Y'$ is affine, there is always a global section.) In particular, it would probably be better suited for maps of general sheaves of sets on the big Zariski topology, rather than just schemes. d) It's a general rule of thumb that, in sheaf theory, it's easier to work with local existential quantifiers than global ones.

Question 2: Does anyone know of any reason why this new definition would be bad?

Logarithmic geometry and algebraic stacksdefinition 4.5. $\endgroup$