Formal power series preserve regular local rings (source code)

= Formal power series preserve regular local rings
{title2=$\dim A[[x]]=\dim A+1$}

Let $(A,\mathfrak m)$ be a <regular local ring> of <Krull dimension> $d$. Its <formal power series ring> $B=A[[x]]$ is <Noetherian> and local, with <maximal ideal> $I=\mathfrak mB+(x)$ and <embedding dimension> $d+1$. Since $I$ is generated by $d+1$ elements, the <Krull height theorem> gives $\dim B\leq d+1$. For the reverse inequality choose a strict prime chain $\mathfrak p_0\subsetneq\cdots\subsetneq\mathfrak p_d=\mathfrak m$ in $A$. Finite generation of each $\mathfrak p_i$ gives $B/\mathfrak p_iB\cong(A/\mathfrak p_i)[[x]]$, an <integral domain>, so each extended <ideal> is prime. The inclusions remain strict by contraction to $A$, and $\mathfrak mB\subsetneq I$ adds one more step since $x\notin\mathfrak mB$. This proves $\dim B=d+1$, equal to its <embedding dimension>, and hence regularity.