finite residue field projective dimension forces depth equals dimension

Given: The objects and hypotheses in the statement. We work with the Axiom of Choice; cited dependent-choice and resolution-existence hypotheses are retained.

auslander buchsbaum formula: For a nonzero finite module $M$ of finite projective dimension over a nonzero Noetherian local ring $R$, ${\mathrm{pd}}_{R}M+{\mathrm{depth}}_{R}M=\mathrm{depth}R$. Consequently such an $M$ with $\mathrm{depth}M=\mathrm{depth}R$ is free.

positive depth ring has regular minimal generator: If a nonzero Noetherian local ring $(R,\mathfrak{m},k)$ has positive depth, then some $x\in \mathfrak{m}\setminus {\mathfrak{m}}^2$ is a nonzerodivisor. The residue field need not be infinite.

residue field splits off reduced maximal ideal: Let $(R,\mathfrak{m},k)$ be nonzero Noetherian local and $x\in \mathfrak{m}\setminus {\mathfrak{m}}^2$ a nonzerodivisor. Over $S=R\mathrm{/}(x)$ the sequence $0\to (x)\mathrm{/}(x\mathfrak{m})\to \mathfrak{m}\mathrm{/}x\mathfrak{m}\to \mathfrak{m}\mathrm{/}(x)\to 0$ splits, and $(x)\mathrm{/}(x\mathfrak{m})\cong k$. Consequently finite ${\mathrm{pd}}_{R}k$ implies finite ${\mathrm{pd}}_{S}k$.

quotient and lifting regularity across a regular element: Let $(R,\mathfrak{m})$ be nonzero Noetherian local. If $x\in \mathfrak{m}$ is a nonzerodivisor and $R\mathrm{/}(x)$ is regular, then $R$ is regular and $x\mathrm{\notin }{\mathfrak{m}}^2$. For every nonzerodivisor $x\in \mathfrak{m}$, $\dim (R\mathrm{/}(x))=\dim R-1$. If $R$ is regular and $0\mathrm{\ne }x\in \mathfrak{m}$, then $R\mathrm{/}(x)$ is regular if and only if $x\mathrm{\notin }{\mathfrak{m}}^2$.

regular local rings are domains and cohen macaulay: 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$.

Depth drops by one after quotienting by a regular element: Let $R$ be Noetherian, let $M$ be finite, let $I$ lie in the Jacobson radical, and let $x\in I$ be $M$-regular. Then ${\mathrm{depth}}_I(M\mathrm{/}xM)={\mathrm{depth}}_I(M)-1.$