TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The diagonal Koszul complex is a finite free resolution of R

Statement

Let $k$ be a field, $R = k [x_{1}, \dots, x_{n}]$ for $n \geq 0$ , and $S = R^{e} = R \otimes_{k} R^{o p}$ . Regard $R$ as the regular $S$ -module through the enveloping-algebra dictionary, and let $u_{i} = x_{i} \otimes 1 - 1 \otimes x_{i}$ . The augmented Koszul complex

$K (u_{1}, \dots, u_{n}; S) \overset{μ}{\to} R$

is a finite free, hence projective, resolution of $R$ over $S$ . Its degree- $j$ term is free of rank $(\binom{n}{j})$ for $0 \leq j \leq n$ , and is zero for $j > n$ . When $n = 0$ , this is the identity resolution $k \overset{i d}{\to} k$ .

Facts & Assumptions

Given: A field $k$ , the polynomial algebra $R = k [x_{1}, \dots, x_{n}]$ , $S = R^{e}$ , the diagonal differences $u_{i}$ , the Koszul complex $K (u_{1}, \dots, u_{n}; S)$ , and its multiplication augmentation $μ$ .

[F1]

The regular bimodule $R$ is the left $R^{e}$ -module with action $(a \otimes b^{o p}) r = a r b$ (Enveloping algebra and the bimodule–module dictionary).

[F2]

The ordered sequence $(u_{1}, \dots, u_{n})$ is regular on $S$ , and multiplication induces $S / (u_{1}, \dots, u_{n}) S ≅ R$ (Polynomial diagonal differences form a regular sequence).

[F3]

Every finite $M$ -regular sequence has zero positive-degree Koszul homology (Regular Sequences Give Acyclic Koszul Complexes).

[F4]

The zeroth Koszul homology is the quotient by the sequence (Basic Koszul Homology).

[F5]

The diagonal Koszul degree- $j$ term is free on its increasing wedge symbols and there are no terms above degree $n$ (The polynomial diagonal Koszul bimodule complex).

[F6]

The increasing wedges indexed by $j$ -element subsets form a basis of the $j$ th exterior power, and that power is zero for $j > n$ (Exterior Algebra Basis Monomials).

[F7]

A free module with a finite basis is projective using only finite choice; the empty basis gives the zero projective module (Free modules are projective, with the exact choice boundary).

[F8]

The category of left $S$ -modules is abelian (Modules over a ring form an abelian category).

[F9]

A projective resolution in an abelian category is an exact augmented complex whose terms are projective (Projective resolutions in an abelian category).

Proof

technique · direct

1.1F1F2givenalgebra

By [F1], $R$ has the regular left $S$ -module structure $(a \otimes b^{o p}) r = a r b$ . The multiplication map $μ : S \to R$ is $S$ -linear: on $s = a \otimes b^{o p}$ and $t = c \otimes d^{o p}$ , $μ (s t) = a c d b = a (c d) b = s \cdot μ (t)$ by associativity. Pure tensors span $S$ , so this equality extends to arbitrary $s, t$ . By [F2], the induced quotient map $S / (u_{1}, \dots, u_{n}) S \to R$ is an isomorphism and is exactly $μ$ . The Koszul differential and $μ$ are module-linear maps, so both send zero to zero.

1.2F5F6givenalgebra

By [F5] and [F6], for $0 \leq j \leq n$ the increasing wedges indexed by $j$ -element subsets form a finite $S$ -basis of $K_{j}$ , with $(\binom{n}{j})$ basis elements, and $K_{j} = 0$ for $j > n$ . If $n = 0$ , the only basis symbol is the empty wedge, $S = R = k$ , and the augmentation is the identity.

2.1F2F3F4step 1.1given

Since $S$ is a commutative ring and $(u_{1}, \dots, u_{n})$ is $S$ -regular by [F2], apply [F3] with coefficient module $S$ to get $H_{j} (K (u_{1}, \dots, u_{n}; S)) = 0$ for every $j > 0$ . By [F4], $H_{0} (K (u_{1}, \dots, u_{n}; S)) = S / (u_{1}, \dots, u_{n}) S$ , which [F2] identifies with $R$ by the augmentation from 1.1. Thus the augmented complex is exact in positive degrees and at $K_{0}$ and $R$ .

2.2F7step 1.2givenalgebra

The basis in each nonzero degree is finite and explicitly enumerated by the lexicographic order on increasing subsets of ${1, \dots, n}$ . By [F7] each $K_{j}$ is projective as an $S$ -module; this uses only finite choice, not AC. The zero terms above degree $n$ are projective as well.

3.1step 2.1step 1.2step 2.2F8F9∎

The augmentation is an exact augmented chain complex by 2.1, all its terms are projective by 2.2, and $S - M o d$ is abelian by [F8]. Therefore [F9] makes it a projective resolution. Step 1.2 gives the claimed finite free ranks and length, including the $n = 0$ identity case. No form of AC is used.

Depends on

Used by

Polynomial Hochschild homology from the diagonal Koszul complex Theorem

Dependency tree · two levels

36 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Charles A. Weibel, An Introduction to Homological Algebra, Chapter 9: Hochschild and Cyclic Homology, Exercise 9.1.3 (standard reference, not scraped)
Mikhail Khovanov, Triply-graded link homology and Hochschild homology of Soergel bimodules, Hochschild homology section (standard reference, not scraped)
The Stacks Project, Section 15.31: Koszul regular sequences, Lemma 15.31.2 (standard reference, not scraped)