Surface complete equicharacteristic formal fibres

Given: A complete equicharacteristic Noetherian local ring $A$ and primes $\mathfrak{q}\subseteq \mathfrak{p}$ of $A$.

cor-complete-local-domain-finite-over-a-regular-power-series-ring. Assume the Axiom of Choice. Let $(A,\mathfrak{m})$ be a complete equicharacteristic Noetherian local domain of dimension $d$. Then there exists a coefficient field $k\subseteq A$ and an injective local homomorphism $k\mathrm{⟦}{X}_1,\dots ,X_d\mathrm{⟧}\hookrightarrow A$ whose image is a regular complete local subring over which $A$ is module-finite. (A complete local domain is finite over a regular power-series ring)

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-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-generic-power-series-formal-fibres. Assume AC. For $A=k[\text{\hspace{0.17em}⁣}[X_1,\dots ,X_n]\text{\hspace{0.17em}⁣}][Y_1,\dots ,Y_m]$ and $K=\mathrm{Frac}A$, every completed local generic fibre $\widehat{A_{\mathfrak{p}}}{\otimes }_{A}K$ is geometrically regular over $K$. (Surface generic power series formal fibres)