ExampleConstruction: Literature-sourcedVerification: 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.

Two-variable diagonal Koszul signs

Example

Assume AC. Let $k$ be a field, $R = k [x, y]$ , and let $M$ be a $k$ -central $R$ -bimodule. Order the exterior generators as $θ_{x} = θ_{1}$ and $θ_{y} = θ_{2}$ . The coefficient Koszul complex is

0 ⟶ M θ_{x} \land θ_{y} \overset{d_{2}}{\to} M θ_{x} \oplus M θ_{y} \overset{d_{1}}{\to} M ⟶ 0,

where $d_{2} (m θ_{x} \land θ_{y}) = - (y m - m y) θ_{x} + (x m - m x) θ_{y}$ and $d_{1} (a θ_{x} + b θ_{y}) = (x a - a x) + (y b - b y)$ . Under the polynomial Hochschild theorem, its homology is $H H_{∙} (R, M)$ .

Facts & Assumptions

Given: AC, a field $k$ , $R = k [x, y]$ , a $k$ -central $R$ -bimodule $M$ , and the ordered exterior generators $θ_{x}, θ_{y}$ .

[F1]

Under AC, the polynomial theorem identifies $H H_{j} (R, M)$ with the homology of the coefficient Koszul complex. Its differential deletes an increasing wedge factor with sign $(- 1)^{r - 1}$ and coefficient $x_{i} m - m x_{i}$ (Polynomial Hochschild homology from the diagonal Koszul complex).

[F2]

A $k$ -central $R$ -bimodule has commuting left and right actions and equal induced scalar actions (Enveloping algebra and the bimodule–module dictionary).

[F3]

The diagonal Koszul term has the increasing wedge basis and alternating deletion differential; if $\deg x = \deg y = 2$ , each wedge generator has internal degree $2$ (The polynomial diagonal Koszul bimodule complex).

[F4]

For the regular bimodule with $k$ in internal degree $0$ , $\deg x = \deg y = 2$ , and each exterior generator in internal degree $2$ , one has $H H_{j} (R, R) ≅ R {2 j}^{(\binom{2}{j})}$ for $0 \leq j \leq 2$ , and $H H_{j} (R, R) = 0$ for $j > 2$ (Diagonal Hochschild homology of a polynomial ring).

[F5]

AC asserts that every family of nonempty sets has a choice function (The Axiom of Choice).

Verification

technique · direct

1.1F1F3given

Specialize the diagonal deletion formula to the ordered two-variable wedge. [F1, F3, given] For $m θ_{x} \land θ_{y}$ , deleting the first factor contributes $(x m - m x) θ_{y}$ with positive sign; deleting the second contributes $- (y m - m y) θ_{x}$ . For degree one, deleting either singleton gives $d_{1} (a θ_{x} + b θ_{y}) = (x a - a x) + (y b - b y)$ . This gives exactly the two displayed maps with the stated wedge orientation.

2.1F1F2step 1.1algebra

Verify that the displayed maps compose to zero. [F1, F2, step 1.1, algebra] Set $u_{x} (m) = x m - m x$ and $u_{y} (m) = y m - m y$ . The bimodule laws in [F2] give $u_{x} u_{y} (m) = (x y) m - (x m) y - (y m) x + m (x y)$ and $u_{y} u_{x} (m) = (y x) m - (y m) x - (x m) y + m (y x)$ . Because $x y = y x$ and the left and right actions commute, these expressions are equal. Hence $d_{1} d_{2} (m θ_{x} \land θ_{y}) = - u_{x} u_{y} (m) + u_{y} u_{x} (m) = 0$ , which checks the mixed-product cancellation.

3.1F1F3F4step 1.1step 2.1algebra

Compute the regular-coefficient subcase. [F1, F4, step 1.1, step 2.1, algebra] If $M = R$ with its regular bimodule structure, commutativity gives $u_{x} (m) = u_{y} (m) = 0$ for every $m$ . Thus both maps vanish. The terms are $R$ in degree zero, $R θ_{x} \oplus R θ_{y}$ in degree one, and $R θ_{x} \land θ_{y}$ in degree two; there are no higher terms. If $\deg x = \deg y = 2$ , their internal shifts are respectively $0$ , $2$ , and $4$ . By [F4], this gives $H H_{0} (R, R) = R$ , $H H_{1} (R, R) = R {2}^{2}$ , $H H_{2} (R, R) = R {4}$ , and $H H_{j} (R, R) = 0$ for $j \geq 3$ .

4.1

Check endpoints, zero input, grading, and AC use. [F1, F2, F3, step 2.1, step 3.1, given] Degree zero is the empty wedge term $M$ , and degree two is the single top wedge $M θ_{x} \land θ_{y}$ ; the degree-two differential has zero composite with $d_{1}$ by step 2.1, and there is no degree-three term. If $M = 0$ , every term and map is zero. For the graded regular-coefficient subcase in step 3.1, use the standard grading with $\deg x = \deg y = 2$ and give each wedge generator internal degree $2$ ; the displayed maps preserve total internal degree. The general coefficient statement does not require a grading on $M$ . AC is used only to apply the polynomial Hochschild theorem and its regular-coefficient corollary; the sign and commutator calculations use no choice. This example asserts no biconditional. [F1, F2, F3, F4, F5, step 1.1, step 2.1, step 3.1, given] $□$

Source comparison

Weibel, An Introduction to Homological Algebra, Exercise 9.1.3, printed p.304/PDF p.4, asks for the general polynomial Koszul computation but does not spell out the two-variable signs. Khovanov, “Hochschild homology,” PDF p.1, lines 41–60, states the polynomial resolution and coefficient differential with exterior deletion signs. The explicit orientation, commutator cancellation, and regular-coefficient groups are calculated above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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, 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)