Hensel's Lemma and Implicit Function Theorem In the literature and on the web happened to me several times to read confused or simply cryptic assertions regarding the fact that Hensel's Lemma is the algebraic version of Implicit Function Theorem.
I tried to explicit this relation but I failed, here there are some observations I made. 
A first good property of Henselian rings, so rings that satisfy Hensel's Lemma, is that their spectrum is homotopically equivalent to their closed point in the sense of Grothendieck. Precisely, if $\widehat{\pi}$ is the pro-fundamental group of a scheme as in SGA1, then $\widehat{\pi}(\operatorname{Spec}(A)) \simeq \widehat{\pi}(\operatorname{Spec}(k(m))$, where $A$ is an Henselian ring and $k(m)$ is the residue field of the maximal ideal $m$ of $A$.
So I thought that spectra of Henselian rings were the kind of "small neighborhoods" in which you can write a "function" explicitly, thanks to Hensel's Lemma. But I'm confused in trying to understand what kind of functions I have to examine. 
Another observation is that Henselianity is exactly the condition needed for a local ring $R$ for having no non-trivial étale coverings of $\operatorname{Spec}(R)$ which are trivial on the closed point. Since these coverings are in correspondence with ètale algebras of $R$ I examined this direction and I found that, for any field $k$, the $k$-algebra of the form $k[x]/f(x)$ is ètale over $k$ if and only if $f'(x)$ is invertible in the algebra.
There is also a more complicated criterion for ètale algebras over rings which uses the invertibility of the determinant of the Jacobian of a system of polynomials. This is very reminiscent of the key condition of the Implicit Function Theorem, but I don't know why.
Here I put the link for the wikipedia pages of some related concepts, such as the implicit function theorem, Henselian rings and Hensel's lemma. Moreover here you can find an article with a large introduction about Henselian rings.
Thank you in advance for your time.
 A: Bill Dubuque has largely answered the question, but just to be explict:
Suppose that you have an equation 
$f(x,y) = 0$, which you want to solve to express $y$ as a function of $x$.
(This is a typical implicit function theorem situation.)
Well, the implicit function theorem says that first, you should choose a small
n.h. of a point, say $x = 0$ to fix ideas.  You should then choose a value $y_0$
of $y$ at this point, i.e. fix a solution to $f(y_0,0) = 0$; again, let's assume
that we can take $y_0 = 0$. (In other words, we assume that $f(x,y)$ has no
constant term, i.e. that $f(0,0) = 0$.)
Now the implicit function theorem says that we can solve for $y$ locally as a function of $x$ provided that $\dfrac{\partial f}{\partial y}(0,0) \neq 0.$  (Of course, there are other technical assumptions --- $f$ should be smooth and so on; let's ignore those, since in a moment I will take $f$ to be a polynomial.)
Now we could think about the implicit function theorem for analytic functions, and then for formally analytic functions, i.e. for formal power series.
So now the question is: given $f(x,y) = 0$, with $f$ a polynomial with no constant term, when we can find a solution $y \in \mathbb C[[x]]$ with no constant term.  A sufficient condition is given by Hensel's lemma: one needs
that $f'(0)$ be a unit in $\mathbb C[[x]]$ (thinking of $f$ as a polynomial in $y$ with
coeficients in $x$, and taking the derivative in $y$).  A formal power series is a unit precisly if its constant term is non-zero, so this can be rephrased as $\dfrac{\partial f}{\partial y}f(0,0) \neq 0,$
which is exactly the same condition as in the implicit function theorem.
In short, Hensel's Lemma in the case of a formal power series ring is 
exactly the same as an implicit function theorem (for polynomial equations,
say) in which one only asks for formal power series solutions.
Incidentally, the connection with Newton's Method is easy to see too:
Suppose that we are trying to solve $f(x,y) = 0$ for $y$ in terms of $x$,
under the assumption that $f(0,0) = 0$ and that $\dfrac{\partial f}{\partial y}(0,0) \neq 0.$  We may assume that the latter quantity equals $1$, by rescaling $f$ if necessary, so our equition has the form
$$0 = a x +  y + b x^2 + c xy + d y^2 + \cdots,$$
which we can rewrite as
$$ y = -a x - b x^2 - c x y - d y^2 + \cdots .$$
Note that this already determines $y$ up to second order terms.
Now subsitute this expression for $y$ back into the right hand side, to 
get 
$$y = - a x - b x^2 - c x (- a x - b x^2 - \cdots) - d (- a x - b x^2 - \cdots)^2 + \cdots,$$
to get $y$ up to third order terms.  Now substitute in again, to 
get $y$ up to fourth order terms, and so on.
This is just Newton's Method.
This proves Hensel's Lemma in this context.  It is also easy to estimate
the size of the power series coefficients for $y$ that one obtains, and
to prove that $y$ has a positive radius of convergence.  Thus we also 
establish a version of the implicit function theorem for analytic functions with the same argument.
Summary: The Implicit Function Theorem, Hensel's Lemma, and Newton's Method are all variants of the same theme.
A: Although it might not be exactly the same result, you can see both principles as a way to go from "local" solutions to "global" solutions for an equation. Here's a very rough sketch of how I think about it (in each case there are some adjustments to be made if you want a rigorous statement). 
First, note that the implicit function theorem is usually formulated with a function of two variables $x$ and $y$  (it  goes "for all y, there is a unique x ..."), but $y$ will be fixed throughout so I'll omit it. Start form an "approximate" solution $x$ to your equation (in the implicit theorem case, you take $(x_0, y_0)$ an actual solution, and then $(x_0, y)$ is an approximate solution). In each case, you want to solve $f(x+h) = 0$. Now when $h$ is "small", because $f$ is "sufficiently regular", you can write
$$f(x+h) = f(x) + f'(x).h +o(h)$$
So the rough idea (or guess), would be that has unique solution $f(x+h) = 0$ if $f(x) + f'(x).h = 0$ has one, which would be the case if $f'(x)$ is invertible (if $f$ is multivariate, $f'(x)$ is understood as the differential, meaning it's invertible when the Jacobian is non zero). Both theorems more or less state that it actually works. 
A: This is elaborated in various places, e.g. see Kuhlman's paper Valuation theoretic and model theoretic aspects of local uniformization in Hauser et al. Resolution of singularities p.389 ff. excerpted below. You can find full proofs in the links following the excerpt. See also Ribenboim,
Equivalent forms of Hensel's lemma, Exposition. Math. 3 (1985), no. 1, 3-24.


[K2] 10.5 The multidimensional Hensel's Lemma, in Ch. 10, Hensel's Lemma, in
Draft of Franz-Viktor Kuhlmann's book on Valuation Theory.
[PZ] A. Prestel, M. Ziegler, Model-theoretic methods in the theory of topological fields.
J. Reine Angew. Math. 299(300) (1978), 318-341
