= Solution
Put $R=\mathcal O_{X,x}$, $\mathfrak m=\mathfrak m_x$ and $d=\dim R$. Smoothness makes $R$ a <regular local ring>, with <residue field> $k$. A list of local parameters $t_1,\ldots,t_d$ is a <regular system of parameters>: its images form a basis of the <cotangent space of a local ring> $\mathfrak m/\mathfrak m^2$. Set $J=(t_1,\ldots,t_d)$. The basis condition says $\mathfrak m=J+\mathfrak m^2$, so the finitely generated module $\mathfrak m/J$ equals $\mathfrak m(\mathfrak m/J)$. The <Nakayama lemma> gives
$$
\boxed{\mathfrak m=(t_1,\ldots,t_d).}
$$
We now construct the requested <formal power series>, rather than assert that a local function has a convergent expansion. The <associated graded ring of a regular local ring> is
$$
\operatorname{gr}_{\mathfrak m}R\cong k[T_1,\ldots,T_d],\qquad T_i\longmapsto t_i\bmod\mathfrak m^2.
$$
Indeed these initial forms generate the graded ring, since the $t_i$ generate $\mathfrak m$. The <Dimension theorem for Noetherian local rings> gives $\dim\operatorname{gr}_{\mathfrak m}R=d$. A nonzero kernel in the surjection from the <polynomial ring> would make its quotient have dimension at most $d-1$, so that kernel is zero.
For $f\in R$, choose $P_0\in k$ to be its residue at $x$. Inductively suppose homogeneous polynomials $P_0,\ldots,P_{n-1}$ have been chosen such that
$$
r_n=f-\sum_{j<n}P_j(t_1,\ldots,t_d)\in\mathfrak m^n.
$$
The graded-ring isomorphism gives a unique homogeneous polynomial $P_n(T_1,\ldots,T_d)$ of degree $n$ representing the class of $r_n$ in $\mathfrak m^n/\mathfrak m^{n+1}$. Subtracting $P_n(t)$ makes the next remainder lie in $\mathfrak m^{n+1}$. Hence
$$
\boxed{f\longleftrightarrow\sum_{n\ge0}P_n(T_1,\ldots,T_d)\in k[[T_1,\ldots,T_d]].}
$$
This equality is interpreted in the <adic completion of a module> $\widehat R=\varprojlim R/\mathfrak m^n$. The same induction applies to every compatible sequence of residues in this inverse limit, so evaluation $T_i\mapsto t_i$ defines an isomorphism $k[[T_1,\ldots,T_d]]\cong\widehat R$. It is injective because the lowest nonzero homogeneous term of a series has nonzero initial form. The <Krull intersection theorem> gives $\bigcap_n\mathfrak m^n=0$, so $R$ embeds in its completion and the series determines $f$. This is the <formal expansion at a smooth point>; it depends on the chosen <regular system of parameters>, and does not claim that the infinite sum converges inside $R$. If $d=0$, the <local ring> is just $k$, and only the constant term is needed.
Back to article page
