Smooth morphisms via local standard smooth presentations

Assume the Axiom of Choice (The Axiom of Choice). Let $k$ be a field and $f:X\to Y$ a morphism of finite-type $k$-schemes. The morphism $f$ is smooth if every point $x\in X$ has affine neighborhoods $x\in V=\mathrm{Spec}B$ and $f(x)\in U=\mathrm{Spec}A$, with $f(V)\subseteq U$, for which the induced map $A\to B$ is standard smooth at the prime corresponding to $x$ (Standard smooth presentations and locally standard smooth maps). Thus the condition is imposed at every source point, including nonclosed points; it is local on the source and target. In this condition, standard smoothness at a prime means that after a further principal shrinking around that prime the ring map has a standard smooth presentation.

The pointwise and global equivalences in Locally standard smooth iff flat with geometrically regular fibres identify standard smoothness for finite-presentation affine charts with flatness and geometrically regular scheme-theoretic fibres. Applied after the local shrinkings above, this gives the corresponding local criterion for $f$. The local-presentation clause itself is choice-free; AC is assumed here for that proved equivalence, through the cited theorem.