Automorphism of a formal power series ring Is the following theorem true?
If yes, how would you prove it?
Theorem
Let $A$ be a commutative ring.
Let $A[[x]]$ be the ring of formal power series in one variable.
Let $\mathfrak{m}$ be the ideal of $A[[x]]$ generated by $x$.
Let $u$ be an invertible element of $A$.
Let $f(x) = ux + g(x)$, where $g(x) \in \mathfrak{m}^2$.
Then there exists a unique automorphism $\psi$ of $A[[x]]$ fixing every element of $A$ such that
$\psi(x) = f$.
 A: According to Eisenbud Theorem 7.16a, there is a unique homomorphism $\psi$ defined as in the question. To see that $\psi$ is an isomorphism, it suffices to check that $\ker\psi=0.$ But this is immediate, since, assuming that $p$ is a power series we have $0=\psi(p(x))=p(\psi(x))$ which implies the coefficient $u=0.$
A: $\psi$ is "evaluate at $f(x)$" is a homomorphism is a standard (and not very enlightening) manipulation of power series, so I'll omit it.
To check that it's invertible, it suffices to find $f^{-1}(x)$. To solve $f(y) = x$, or $x = uy + g(y)$:
$$y = u^{-1} x + u^{-1} g(y) = u^{-1} x + u^{-1} g\left(u^{-1} x + u^{-1} g(y)\right) = \cdots $$
Because $g(x) \equiv 0 \mod{x^2}$, it's not hard to see that this series converges. The inverse of $\psi$ is then "Evaluate at $y$".
It might be easier to use Newton's method, starting with the initial approximation
$$y \approx u^{-1} x$$
I do not know a proof that $\psi$ is the only ring homomorphism (over $A$) that sends $x$ to $f(x)$, though it's obviously the only one that's continuous.
