Formalism behind local characterizations of formal smoothness/unramifiedness/étaleness over algebraically closed fields

In synthetic differential geometry, one way to define formally étale morphisms is as follows.

Say $f:M\to N$ is formally étale if $TM\cong TN\times _N M$, in other words if the unique map from $TM$ to the pullback is an isomorphism. (A generalization of) this approach is taken e.g in definition 8.10 of Kostecki's notes.

One could also say $f$ is formally unramified/smooth/étale if the induced arrow $TM\to TN\times _NM$ is injective/surjective/bijective.

The classical differential-geometric definition for a smooth map of manifolds says $f$ is an immersion/submersion/étale if each $d_xf:T_xM\to T_{f(x)}N$ is injective/surjective/bijective.

Coming back to SDG, I'm pretty sure $T_{f(x)}N\cong T_{f(x)}N\times _N M$ holds in complete generality, so say $f$ is formally unramified/smooth/étale at a point $x:1\to M$ if $d_xf:T_xM\to T_xN$ is monic/epic/invertible.

For nonsingular varieties over algebraically closed fields, it's known that $f$ is étale iff it's étale at every point. For general varieties over algebraically closed fields, I see from snooping around the net that we need 'tangent cones', and I don't really know anything about those yet. At any rate, the proofs of these equivalences seem to rely on the Jacobian criterion, and t, so I take it they also work for just formally unramified/smooth maps.

In the nonsingular case, this characterization kind of makes sense since the nullstellensatz says points give good information - the singular case I'll have to tackle some time.

Anyway, the point of this story is that over algebraically closed fields, we're getting really clean formal equivalences. For example the formally étale case is:

$$\require{AMScd} \begin{CD} TM @>{df}>> TN\\ @VVV @VVV\\ M @>>{f}> N \end{CD}\text{ pullback}\iff \require{AMScd} \begin{CD} T_xM @>{d_xf}>> T_xN\\ @VVV @VVV\\ M @>>{f}> N \end{CD}\text{ pullback for all points}$$

and analogously for formally unramified/smooth. At least the equivalence of the formally étale case above looks completely categorical. The only similar property I know of that seems relevant is universal coproducts, which is equivalent to the equivalence below.

$$\require{AMScd} \begin{CD} \coprod_iP_i @>>> \coprod_iX_i\\ @VVV @VVV\\ A @>>> B \end{CD}\text{ pullback}\iff \require{AMScd} \begin{CD} P_i @>>> X_i\\ @VVV @VVV\\ A @>>> B \end{CD}\text{ pullback for all }i$$

But tangent bundles are more than just the tangent spaces side by side...

My qusetions:

1. What's the categorical property of algebraic closedness that gives the first equivalence above?
2. Is there any relation to universal products, and if so, what is it?

Added. Wandering the internet some more, I see strictly Henselian rings pop up in context of inverse function theorems for schemes. In fact, in section 2.3 of the book Néron Models, it's said (strictly) Henselian rings are described geometrically by schemes satisfying "certain aspects of the inverse function theorem". Since the inverse function theorem (I think) is responsible for the equivalence in the case of smooth manifolds, perhaps Henselian properties, and not algebraic closedness, are what makes things tick. I really have no idea about Henselian stuff though, so just throwing it out there...

• I can't parse this identity you write $T_{f(x)}N\cong T_{f(x)}N\times _N M$. The thing on the left is the tangent space of $N$ at the point $f(x)$. What is the one on the right? – Michael Bächtold Aug 31 '16 at 9:07
• A strictly henselian local ring does not have no non-trivial étale extensions. In this sense the inverse function theorem is satisfied. So, for these rings infinitesimal isomorphism implies local isomorphism as in the differential case. – Leo Alonso Dec 13 '17 at 10:15
• @Arrow: I suspect that in retrospect I understand what $T_{f(x)}N\times_N M$ meant: for given $x:1\to M$ and $f:M\to N$ it is the pullback of $T_{f(x)}N \to N$ (which factors through $f(x):1\to N$) along $f$ . But now I don't understand why you claim that $T_xM\cong T_{f(x)}N\times_N M$ for any $f$ and $x$. It seems wrong for say $f:R\to 1$ and any $x:1\to R$. – Michael Bächtold Dec 13 '17 at 13:10