Let's suppose by $k[[x]]$ we mean the formal power series ring in variables $x_1, x_2, \dots$ which is literally the space of sequences of monomials that individually involve only finitely many variables per monomial (so set-theoretically a direct product of copies of $k$ indexed by such monomials, with a "cofinite" topology). This is of course different from the $(x)$-adic completion of $k[x] := k[x_1,x_2,\dots]$ as noted by Francois, since the latter has as a cofinal system of discrete quotients the rings $k[x]/(x)^m$ of infinite $k$-dimension whereas the former has as a cofinal system of discrete quotients the artinian $k[x_1,\dots,x_r]/(x_1,\dots,x_r)^m$ of finite $k$-dimension.

I claim that $k[[x]]$ in the sense I have specified *is* flat over $k[x]$ (though I also think this is probably completely useless and so I don't claim this is interesting -- maybe just amusing). The key input is buried near the end of volume 1 of SGA3. These methods have no relevance to the $(x)$-adic completion of $k[x]$ (which is an entirely different beast than $k[[x]]$ as defined above).

First, some preliminary reductions. We have to show that if $I$ is a finitely generated ideal of $k[x]$ then the injection $I \rightarrow k[x]$ remains injective after tensoring against $k[[x]]$ over $k[x]$. By finite generation, $I$ "comes from" an ideal $I' \subset k[x_1,\dots,x_r]$ for some $r$, and more specifically the natural map $$I' \otimes_{k[x_1,\dots,x_r]} k[x] \rightarrow k[x]$$ is injective since $k[x]$ is certainly flat (even free) over $k[x_1,\dots,x_r]$. So in fact
$$I = I' \otimes_{k[x_1,\dots,x_r]} k[x],$$
and hence our problem is to show that the injection $I' \rightarrow k[x_1,\dots,x_r]$ remains injective after tensoring over $k[x_1,\dots,x_r]$ against $k[[x]]$. More specifically, we claim this latter ring map is flat.

This final scalar extension process decomposes as a composition of two scalar extensions:
$$k[x_1,\dots,x_r] \rightarrow k[[x_1,\dots,x_r]] \rightarrow k[[x]].$$
Since the first step is known to be flat by usual commutative algebra with noetherian ring, we're reduced to proving flatness of the second map. But this is a special case of the Gabriel-Grothendieck theory of pseudo-compact rings in SGA3, in which they systematically develop a good theory of "pseudo-compact modules" and "topological flatness" for "pseudo-compact rings", which are topological rings that are arbitrary inverse limits of artinian rings. This theory includes as a key ingredient a relationship between topological flatness and ordinary flatness when the base ring is *noetherian* (analogous to completions in the noetherian setting, but logically requiring more work).

More specifically, since $A := k[[x_1,\dots,x_r]]$ is noetherian, so any finitely generated $A$-module is finitely presented (and is pseudo-compact for its max-adic topology), for any finitely generated $A$-module $M$ and *pseudo-compact* $A$-algebra $A'$ the natural map
$$M \otimes_A A' \rightarrow M \widehat{\otimes}_A A'$$
is bijective (ultimately because the left side is a cokernel of a map between finite free $A'$-modules and any such map automatically has *closed* image by a variant of Artin-Rees proved in SGA3). Thus, the preservation of injectivity of the left as a functor in finitely generated $M$ (which is equivalent to $A$-flatness of $A'$) is reduced to topological flatness of $A'$ over $A$.

Note that one can "distribute" formal power series over other formal power series when extracting out a *finite* set of variables into the *coefficients* over infinitely many variables (think for a minute, using *our* running definition of "formal power series" for a possibly infinite set of variables). Thus, in our case of interest $A' = k[[x]]$ is a formal power series ring over $A = k[[x_1,\dots,x_r]]$ in infinitely many variables. Thus, we're finally reduced to the question: if $A$ is a pseudo-compact ring (such as $k[[x_1,\dots,x_r]]$) then is $A[[y_1,\dots]]$ topologically flat over $A$? The answer is "yes" because such formal power series rings (in the sense of our running definition) are "topologically free", and a basic fact in the theory is that topological freeness (suitably defined...) implies topological flatness.

QED

3more comments