Koszul resolution

For a regular sequence $f_1,\dots ,f_r$ in a commutative ring $R$, its Koszul complex is the finite free projective resolution of $R/(f_1,\dots ,f_r)$ with terms ${\bigwedge }^j{R}^r$ and boundary map contracting by $(f_1,\dots ,f_r)$. Exactness follows by induction: append $f_r$ using the mapping cone for multiplication by $f_r$, which is injective on the preceding quotient. For a polynomial ring viewed as a bimodule, use the regular sequence $X_{i,\ell }-X_{i,r}$ in the enveloping algebra.