Proposition 8

— Let $X = (X_i)_i$, be a finite family of indeterminates. (i) Every derivation of the ring of formal power series $\mathbf{A}[[X]]$ is continuous. (ii) Every derivation of the polynomial ring $\mathbf{A}[X]$ into the ring of formal power series $\mathbf{A}[[X]]$ extends in a unique fashion to a derivation of the ring $\mathbf{A}[[X]]$. (iii) The family $(D_i)_{i \in I}$ is a basis of the $\mathbf{A}[[X]]$-module of A-derivations of $\mathbf{A}[[X]]$ into itself. Let $b_n$ be the set of all formal power series of order $\geq n$. It is clear that $b_n$ is an ideal in the ring $\mathbf{A}[[X]]$, generated by the monomials of degree $n$. Hence $b_n$ consists of finite sums of products of $n$ formal power series without constant terms; if $D$ is a derivation of $\mathbf{A}[[X]]$, we have

whence it follows at once that $Db_n \subset b_{n-1}$ for $n \geq 1$. Since the sequence $(b_n)_{n \geq 0}$ is a fundamental system of neighbourhoods of 0 in $\mathbf{A}[[X]]$ (IV, p. 26 remark), D is continuous and (i) is proved.

Let $A$ be a derivation of $A[X]$ into $A[[X]]$. Arguing as before, we can show that $A(h)$ belongs to $b, -_1$, for every homogeneous polynomial $h$ of degree $n \geq 1$. Now let $u \in A[[X]]$ and let $u_n$ be the homogeneous component of degree $n$ of $u$. Since $A(u_n) \in b, -_1$ for $n \geq 1$, the family $(A(u)), \ldots$, is summable in $A[[X]]$ and we can define a derivation $D$ of $A[[X]]$ into itself by

We have $D(b_n) \subset b_{n-1}$, hence $D$ is a continuous endomorphism of the additive group of $A[[X]]$. The mapping $\Phi : (u, v) \mapsto D(uv) - uD(v) - D(u)v$ of $A[[X]] \times A[[X]]$ into $A[[X]]$ is continuous and zero on $A[X] \times A[X]$. Since $A[X]$ is dense in $A[[X]]$, we have $\Phi = 0$; in other words, $D$ is a derivation of $A[[X]]$ into itself, extending $A$.

Finally, $A[X]$ is dense in $A[[X]]$ and every derivation of $A[[X]]$ is continuous by (i); hence there exists a unique extension of $A$ to a derivation of $A[[X]]$. This proves (ii).

It remains to prove (iii). Formula (18) (IV, p. 33) shows that the family $(D_i)_{i \in I}$ is linearly independent over $A[[X]]$, and formula (16) (IV, p. 32), applied in the case $E = A[[X]]$, shows that every $A$-derivation is a linear combination of the $D_i$ with coefficients in $A[[X]]$.