Corollary 1

Let $k_0$ be a ring, $k$ a noetherian $k_0$-algebra formally smooth, and $B$ a local $k$-algebra essentially of finite type. If the $k_0$-algebra $B$ is formally smooth for the $\mathfrak{m}_B$-adic topology, it is formally smooth.

There exist an integer $n \geqslant 0$, a multiplicative subset $S$ of $k[T_1, \ldots, T_n]$, and a surjective $k$-homomorphism $S^{-1} k[T_1, \ldots, T_n] \to B$. The algebra $S^{-1} k[T_1, \ldots, T_n]$ is noetherian and formally smooth over $k$ (No. 3, Example 2 and No. 2, Prop. 4, a)), hence over $k_0$ (No. 2, Prop. 3, a)). The corollary then follows from Th. 3, c).