For central , define the Koszul complex on central ring elements using formal exterior symbols:
with zero terms outside and differential
The terms are free bimodules with the formal symbols commuting with coefficients. Centrality makes a bimodule map, and the terms in cancel in pairs because the commute. This defines the Koszul complex over a possibly noncommutative ring without using an undefined exterior algebra of arbitrary one-sided modules. In particular is a well-defined chain complex of left modules.
A regular sequence on a module means that multiplication by is injective on for each , usually with the additional convention that the final quotient is nonzero. The homology vanishing below uses only the injectivity conditions. For one element, the chain complex is , with zero first homology and zeroth homology .
For the induction let . Adjoining the last generator identifies the new Koszul complex with the mapping cone of multiplication by on . In the convention its differential is ; the identification is . The long exact sequence in homology of this mapping cone gives
The induction hypothesis is for and . Regularity makes injective. Hence the new positive homology is zero and its zeroth homology is . The augmentation to this quotient induces these homology isomorphisms, giving the quasi-isomorphism
where the right side is placed in degree zero. The results used are the long exact sequence in homology of a degreewise short exact sequence of complexes and its mapping cone form, together with the stated induction; no unmentioned acyclicity criterion is needed.
For , is a regular sequence: is a non-zero-divisor in , and multiplication by is injective in , even when is composite. The Koszul resolution of is
With and acting as zero, applying the Hom functor gives the cochain complex
Thus, more generally, the Ext groups between polynomial-ring residue modules are
and vanish in all degrees above two. For the equal-modulus case,
These are -modules through and reduction modulo . If the multiplicative self-Ext functor is desired, the Koszul self-Ext algebra is the exterior algebra on two degree-one generators over . The two contractions on the Koszul resolution lift these classes, square to zero and anticommute, so this description also holds for composite and characteristic two. For coprime , multiplication by is invertible on , so both its kernel and cokernel vanish:
For central elements, each multiplication map on the preceding quotient must be injective; a usual convention also requires the final quotient to be nonzero. The augmented Koszul complex on central ring elements tensored with is then a quasi-isomorphism to the final quotient in degree zero.