Surface regular fibres preserve normality

Given: A flat map of Noetherian rings with regular fibres, and in the application the completion map of a normal essentially finite-type local ring over a field or complete equicharacteristic base.

cor-flat-local-depth-additivity. Assume the Axiom of Choice. For a flat local homomorphism $(R,\mathfrak{m})\to (S,\mathfrak{n})$ of Noetherian local rings, $\mathrm{depth}(S)=\mathrm{depth}(R)+\mathrm{depth}(S\mathrm{/}\mathfrak{m}S)\mathrm{.}$ (Depth is additive for a flat local homomorphism)

Under AC, a commutative Noetherian ring is normal if and only if it satisfies $(R_1)$ and $(S_2)$; no domain hypothesis is required. (serre normality criterion)

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-flat-local-ascent-of-regularity. Assume the Axiom of Choice. For a flat local map $(R,\mathfrak{m})\to (S,\mathfrak{n})$ of nonzero Noetherian local rings: if $R$ and $S\mathrm{/}\mathfrak{m}S$ are regular, then $S$ is regular. Conversely, regularity of $S$ implies regularity of $R$. (flat local ascent of regularity)

lem-flat-local-depth-formula-regular-sequence-split. Assume the Axiom of Choice. Let $(R,\mathfrak{m},k)\to (S,\mathfrak{n},\mathrm{\ell })$ be a flat local homomorphism of Noetherian local rings. If $x_1,\dots ,x_r$ is an $R$-regular sequence and ${\bar{y}}_1,\dots ,{\bar{y}}_s$ is regular on the closed fibre $S\mathrm{/}\mathfrak{m}S$, then arbitrary lifts $y_j\in \mathfrak{n}$ make $x_1,\dots ,x_r,y_1,\dots ,y_s$ an $S$-regular sequence. (A flat local map splits regular sequences into base and fibre parts)

A nonzero finite module over a Noetherian local ring has depth at most its support dimension. (A finite local module has depth at most its dimension)

lem-surface-finite-type-formal-fibres. Assume AC and DC. Let $A$ be a field or a complete equicharacteristic Noetherian local ring and $B$ an essentially finite-type $A$-algebra. Every formal fibre of every local ring of $B$ is geometrically regular over its residue fraction field. (Surface finite type formal fibres)

thm-completion-of-a-noetherian-local-ring. Assume the Axiom of Choice. Let $(R,\mathfrak{m})$ be a Noetherian local ring, and let $\widehat{R}$ be its $\mathfrak{m}$-adic completion. 1. $\widehat{R}$ is a Noetherian local ring with maximal ideal $\mathfrak{m}\widehat{R}$. 2. The residue field is unchanged: $\widehat{R}\mathrm{/}\mathfrak{m}\widehat{R}\cong R\mathrm{/}\mathfrak{m}\mathrm{.}$ 3. The completion map $R\to \widehat{R}$ is faithfully flat. (Completion of a Noetherian local ring is local with the same residue field)

thm-regular-local-rings-are-domains-and-cohen-macaulay. Assume the Axiom of Choice (The Axiom of Choice). A regular local ring $R$ of dimension $d$ is a domain and Cohen–Macaulay. For every regular system $(x_1,\dots ,x_d)$, the tuple is $R$-regular and $R\mathrm{/}(x_1,\dots ,x_c)$ is regular local of dimension $d-c$ for all $0\le c\le d$. (regular local rings are domains and cohen macaulay)