Koszul complex ($K_{\bullet }(f_1,\dots ,f_r;R)$)

The Koszul complex on $f_1,\dots ,f_r$ has term $K_i={\bigwedge }^i{R}^r$ and differential $\partial (e_{j_1}\wedge \cdots \wedge e_{j_i})={\sum }_a(-1{)}^{a-1}{f}_{j_a}{e}_{j_1}\wedge \cdots \wedge \widehat{e_{j_a}}\wedge \cdots \wedge e_{j_i}$. Its degree-zero homology is $R/(f_1,\dots ,f_r)$. For a regular sequence it is exact in positive degrees, hence a Koszul resolution of that quotient. The variables of a polynomial ring form a regular sequence, so this resolves the coefficient field in length equal to the number of variables.

The perfect exterior pairing in complementary degrees identifies the dual of a Koszul complex with its degree reversal, with suitable differential signs. For a regular sequence, its Koszul resolution consequently gives ${\mathrm{Ext}}_R^i(R/(f),R)=0$ except in degree $r$, where it is $R/(f)$.

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.

Tensor the finite free Koszul complex on $f_1,\dots ,f_r$ with the module $M$. For a regular sequence on a module, its positive Koszul homology vanishes. If the sequence is regular on $R$, this complex instead computes ${\mathrm{Tor}}^R(R/(f),M)$ for arbitrary $M$.

Koszul homology is the homology of the Koszul complex with module coefficients. Its degree-zero term is $M/(f)M$, and its positive terms record failures of regularity. Each generator acts trivially on homology by the Koszul homotopy for multiplication by a generator.

Exterior multiplication $h_j(u)=e_j\wedge u$ is a chain homotopy between multiplication by $f_j$ and zero on a Koszul complex. A linear combination of these homotopies is a contracting homotopy when the generators span the unit ideal.

For a possibly noncommutative ring and central $t_i$, the formal exterior basis gives free bimodules with differential $d(e_{i_1}\wedge \cdots \wedge e_{i_k})={\sum }_a(-1{)}^{a-1}{t}_{i_a}{e}_{i_1}\wedge \cdots \widehat{e_{i_a}}\cdots \wedge e_{i_k}$. Centrality makes this a bimodule differential. Pairwise cancellation proves $d^2=0$.