regular element reduction preserves minimal 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.

finite local modules admit minimal free resolutions: Every finite module $M$ over a nonzero Noetherian local ring $(R,\mathfrak{m},k)$ has an augmented resolution $\cdots \to F_1\to F_0\to M\to 0$ by finite-rank free modules, with $d_i(F_i)\subseteq \mathfrak{m}{F}_{i-1}$ for $i>0$. Such a resolution is called minimal; it need not be bounded. This extends the bounded terminology without changing it.

projective dimension from last nonzero betti number: For a nonzero finite module $M$ over a nonzero Noetherian local ring, ${\mathrm{pd}}_{R}M=\sup \{i\ge 0:{\beta }_i^R(M)\mathrm{\ne }0\}$, allowing infinity. For each integer $q\ge 0$, ${\mathrm{pd}}_{R}M\le q$ if and only if ${\mathrm{Tor}}_{q+1}^R(k,M)=0$.

The balanced Tor bifunctor: For a right $R$-module $N$, a left $R$-module $M$, and $i\ge 0$, define ${\mathrm{Tor}}_i^R(N,M)$ to be either $H_i(N{\otimes }_R{P}_{\bullet })$ for a projective resolution of $M$ or $H_i(Q_{\bullet }{\otimes }_{R}M)$ for a projective resolution of $N$, identified by the preceding natural balance isomorphism. On maps it uses the homology maps induced by comparison maps; coherence makes this a well-defined covariant bifunctor.

Tor is symmetric over a commutative ring: If $R$ is commutative and $M,N$ are $R$-modules, then ${\mathrm{Tor}}_i^R(M,N)\cong {\mathrm{Tor}}_i^R(N,M)$ naturally.

Assuming the Axiom of Choice, Nakayama's lemma: Assume the Axiom of Choice. Let $R$ be a commutative ring, let $I⊴R$ satisfy $I\subseteq J(R)$, and let $M$ be a finitely generated left $R$-module. If $IM=M$, then $M=0$.