I heard several times the inverse function theorem fails in algebraic geometry. Now I realize I'm pretty confused by this. This question has two parts. The first part asks for the correct formulation of synthetic inverse function theorems. The second asks for clarifications and intuitions about Penon's paper.

Detailed references would be much appreciated - I only know about Kock's two texts, Lavedhomme's book, and Kostecki's notes on SDG and these do not discuss these things, and I don't know the algebraic geometry literature well enough to find this stuff...

Apologies if this is all too elementary!

**Part I**

In *Synthetic Geometry of Manifolds*, Kock writes the inverse function theorem takes us "from infinitesimal invertibility to local invertibility", which sounds morally right.

- For "local invertibility" I can only think of one interpretation - $f$ étale at a point $x$ implies an open $U\ni x$ such that $f|_U$ is an isomorphism.
- For "infinitesimal invertibility" I can think of two options:
- (2a) the usual unique lifting property against infinitesimal neighborhoods;
- (2b) the differential $\operatorname{d}_x\!f$ being an isomorphism at all points.

I'll go with the second option trying to parallel classic differential geometry.

Following Kock's words, am I right to call the following condition "an inverse function theorem"?

**Condition IFT1.** (2b)$\implies$(1).

Or is this the wrong idea completely?

Also, is the Henselian property all about the implication (2a)$\implies$(1)?

I ask because of the following excerpt from section 2.3 of *Néron Models*, which, at least for schemes over fields, seems similar.

Let $R$ be a local ring with maximal ideal $\mathfrak m$ and residue field $k$. Let $S$ be the affine (local) scheme of $R$, and let $s$ be the closed point of $S$. From a geometric point of view, Henselian and strictly Henselian rings can be introduced via schemes which satisfy certain aspects of the inverse function theorem.

Definition 1.The local scheme $S$ is calledHenselianif each étale map $X\to S$ is a local isomorphism at all points of $X$ over $s$ with trivial residue field extension $k(x)=k(s)$. If, in addition, the residue field $k(s)$ is separably closed, $S$ is calledstrictly Henselian.

Also, for a morphism $f:X\to S$ for schemes, $f$ is smooth at $x$ iff it's étale-locally a projection, i.e there's an open neighborhood $U\ni x$ such that $f|_U$ factors through an étale morphism followed by a canonical projection from $\mathbb A_S^n$. Replacing smooth with étale looks like an implicit function theorem and I think this is precisely what is meant by the Henselian property over a field. Is this correct, or is some other notion of "local isomorphism" is meant in the excerpt above?

**Part II**

This paper by Penon formulates a synthetic inverse function theorem and moreover claims that a morphism of equidimensional varieties is étale in several equivalent senses iff it satisfies the usual synthetic definition - the square below is a pullback. $$\require{AMScd} \begin{CD} TM @>{df}>> TN\\ @VVV @VVV\\ M @>>{f}> N \end{CD}$$

I don't read French and I can't make much sense of the pullback square he describes, but I know it only involves infinitesimal objects. Hence, it seems Penon's paper couldn't possibly address "local invertibility" in the sense of open neighborhoods. If so, what's the point of the paper? Note his notion are also used in this paper by Marta Bunge.

**Added.** Here's Penon's Thesis. Again, from what I can make out, there's no mention of neighborhoods in the local context.