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:
- What's the categorical property of algebraic closedness that gives the first equivalence above?
- 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...