Surface generic power series formal fibres

Given: The ring $A=k[\text{\hspace{0.17em}⁣}[X_1,\dots ,X_n]\text{\hspace{0.17em}⁣}][Y_1,\dots ,Y_m]$ with fraction field $K$ and a prime $\mathfrak{p}\in \mathrm{Spec}A$.

def-axiom-of-choice. The Axiom of Choice (AC) is the following statement. > Every family of nonempty sets has a choice function > (def-choice-function). Written out: for every set $\mathcal{F}$ all of whose members are nonempty, there exists a function $g$ with domain $\mathcal{F}$ satisfying $g(S)\in S$ for all $S\in \mathcal{F}$. (The Axiom of Choice)

def-dependent-choice. Let $X$ be a set and let $R\subseteq X\times X$ be a binary relation on $X$. Call $R$ entire on $X$ when $\text{for every }x\in X\text{ there is }y\in X\text{ with }xRy\mathrm{.}$ The Axiom of Dependent Choice, written $\mathrm{D}\mathrm{C}$, is the following statement. (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain)

lem-surface-derivations-and-regular-hypersurfaces. Assume AC. Derivations of Noetherian rings extend uniquely through localization and adic completion. If $T$ is regular Noetherian, $D:T\to T$ a derivation and $D(f)$ a unit, then $T[z]\mathrm{/}(z^r-f)$ is regular for every $r\ge 1$. (Surface derivations and regular hypersurfaces)

lem-surface-finite-completion-factors. Assume AC. For a finite map $R\to S$ of Noetherian rings and $\mathfrak{p}\in \mathrm{Spec}R$, $\widehat{R_{\mathfrak{p}}}{\otimes }_{R}S\cong {\prod }_{\mathfrak{q}\cap R=\mathfrak{p}}\widehat{S_{\mathfrak{q}}}$. The finitely many factors use their maximal-adic completions. Thus formal fibres for finite extensions are factors of residue-field base changes of the original formal fibres. (Surface finite completion factors)

lem-surface-geometric-regularity-field-test-and-generic-spread. Assume AC. For a Noetherian $k$-algebra $T$, call $T$ geometrically regular if $T{\otimes }_{k}E$ is regular for every finitely generated field extension $E\mathrm{/}k$. It suffices to test finite purely inseparable $E\mathrm{/}k$. Geometric regularity is stable under finitely generated field extension. (Surface geometric regularity field test and generic spread)

lem-surface-non-pth-power-detected-by-derivation. Assume AC. Let $B$ be a domain of characteristic $p>0$ finite type over a complete equicharacteristic Noetherian local ring, and let $f\in B$ not be a $p$th power in $\mathrm{Frac}B$. There is a derivation $D:B\to B$ with $D(f)\mathrm{\ne }0$. (Surface non pth power detected by derivation)

thm-completion-preserves-regular-local-rings. Assume the Axiom of Choice (The Axiom of Choice). A nonzero Noetherian local ring $R$ is regular if and only if its maximal-adic completion $\widehat{R}$ is regular. (completion preserves regular local rings)