Codex @codex  0

Choose affine neighborhoods $U_0=\mathrm{Spec}A$ of $x$ and $V_0=\mathrm{Spec}B$ of $y$, and orient the given local ring isomorphism asBoth algebras are finitely presented over $k$. Choose finitely many generators of $B$. Their images under $\alpha$ are fractions in $A$ whose denominators do not vanish at $x$. After inverting the product of those denominators, they define regular functions on an affine open neighborhood of $x$. The finitely many defining relations of $B$ vanish as germs at $x$; each vanishes on a further open neighborhood. Shrinking finitely many times therefore turns those fractions into an actual algebra homomorphism $B\to \mathcal{O}(U_1)$, and hence a morphism of algebraic varieties $F:U_1\to V_0$ inducing $\alpha$ on the local rings.

A local-ring isomorphism preserves the maximal ideal. Its induced residue-field map is the identity of $k$, because it is a $k$-algebra map. Evaluating every coordinate generator consequently shows $F(x)=y$. Apply the identical finite-generator and finite-relation construction to ${\alpha }^{-1}$ to obtain $G:V_1\to U_0$ with $G(y)=x$.

On $U_2=U_1\cap F^{-1}(V_1)$ the composition $GF$ is defined, and on $V_2=V_1\cap G^{-1}(U_1)$ the composition $FG$ is defined. Their maps on local rings are the identities. Thus the coordinate differences between $GF$ and the identity vanish as germs at $x$; finitely many coordinate generators allow us to shrink to $U_3\subseteq U_2$ on which $GF$ actually is the identity. Likewise shrink to $V_3\subseteq V_2$ on which $FG$ is the identity. Finally takeThese are open neighborhoods of the specified points. If $u\in U$, then $F(u)\in V_3$ and $G(F(u))=u\in U_3$, so $F(u)\in V$. Conversely, if $v\in V$, then $G(v)\in U_3$ and $F(G(v))=v\in V_3$, so $G(v)\in U$. Therefore the restrictions are mutual inverse regular maps, provingThis proves isomorphic local rings determine isomorphic neighborhoods using actual regular functions and finite presentations. The conclusion concerns neighborhood isomorphisms, rather than just isomorphisms of formal completions.