Formal inverse function theorem

Statement

f=(f_1,\ldots,f_n)\in(X_1,\ldots,X_n)R[[X_1,\ldots,X_n]]^n.

Write $J_f(0)\in M_n(R)$ for the matrix of linear coefficients of $f$ . The formal inverse function theorem says that the following are equivalent:

$J_f(0)$ is invertible over $R$ ;
there is a unique tuple $g\in(X)R[[X]]^n$ satisfying $f(g(X))=X=g(f(X))$ ;
substitution by $f$ is a continuous $R$ -algebra automorphism of $R[[X]]$ .

Recursive construction

Decompose $f=f^{(1)}+f^{(2)}+\cdots$ into homogeneous terms. The degree-one equation forces $g^{(1)}=(f^{(1)})^{-1}$ . Once $g^{(1)},\ldots,g^{(d-1)}$ are known, the degree- $d$ part of $f(g)=X$ is a linear equation for $g^{(d)}$ with coefficient matrix $J_f(0)$ . Inverting that matrix determines $g^{(d)}$ uniquely. Completeness of $R[[X]]$ assembles the degreewise solution.

Consequences

A pointed formal map is a coordinate change exactly when its tangent map is an isomorphism. In particular, a morphism of formal group laws whose linear coefficient is invertible is automatically an isomorphism.

Formal, not analytic

This theorem is coefficientwise and valid over any commutative base ring. It does not claim that the series defines a convergent function on an open subset of $\mathbb R^n$ or $\mathbb C^n$ ; no norm or analytic convergence is part of the statement.

References

Michiel Hazewinkel, Formal Groups and Applications, AMS Chelsea Publishing, 2012. AMS book record. Relevant: Appendix A, “Homomorphisms and isomorphisms; formal inverse function theorem.”
Nicolas Bourbaki, Algebra II: Chapters 4–7, Springer, 1990. Relevant: Chapter 4, formal series and substitution.