regular local residue field koszul resolution

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

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$.

Koszul Complex Resolves A Regular Quotient: If $M$ is finite free and $\mathbf{x}$ is $M$-regular, then $K(\mathbf{x};M)$ is a finite free resolution of $M\mathrm{/}(\mathbf{x})M$.

minimal free resolution differentials land in maximal ideal: For an augmented degreewise finite free resolution over a nonzero Noetherian local ring $(R,\mathfrak{m})$, minimality means that every positive differential matrix has entries in $\mathfrak{m}$. Equivalently no positive differential admits a unit pivot, or a nonzero two-term identity direct summand. A unit pivot can be cancelled without changing the resolved module.