Koszul acyclicity criterion in a Noetherian local ring (source code)

= Koszul acyclicity criterion in a Noetherian local ring
{c}

Let $(R,\mathfrak m)$ be a <Noetherian local ring>, let $M$ be nonzero and finitely generated, and let every $f_i$ lie in $\mathfrak m$. Then positive <Koszul homology> vanishes exactly when $f$ is a <regular sequence on a module> $M$. The <mapping cone> exact sequence proves the forward implication by induction; surjectivity of the last generator on earlier homology and the <Nakayama lemma> prove the converse.