Holomorphic inverse function theorem

Remarks

Viewed as a map of $\R^{2n}$, $F$ has real Jacobian determinant $\abs{\det (\partial F_k / \partial z_j)}^2$, which is not zero at $a$. The real inverse function theorem gives a $C^1$ local inverse $G$. Its derivative at each point is the inverse of the $\C$-linear map $DF$, hence $\C$-linear, so $G$ is holomorphic. Example: $F(z_1, z_2) = (e^{z_1}, \ z_2 e^{z_1})$ has complex Jacobian determinant $e^{2 z_1} \ne 0$ everywhere, so it is a local biholomorphism near every point, though it is not injective on $\C^2$, since $F(z_1 + 2\pi i, z_2) = F(z_1, z_2)$. The hypothesis is needed: $F(z) = z^2$ on $\C$ has derivative $0$ at $0$, and it is not injective on any neighbourhood of $0$.

Going deeper

For a student

This theorem is the basic local tool for complex manifolds and holomorphic maps. Together with the holomorphic implicit function theorem, it shows that the zero set of holomorphic functions with independent differentials is locally a complex submanifold. A stronger fact holds in the complex case: an injective holomorphic map between open subsets of $\C^n$ automatically has nonzero Jacobian determinant, so it is a biholomorphism onto its image. The real analogue fails, as $x \mapsto x^3$ shows.