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.

One-variable twisted bimodule Hochschild calculation

Example

Assume AC. Let $R = Q [x]$ and let $M = R$ as a left $R$ -module with right action $m \cdot x = - x m$ , extended to all polynomials by $m \cdot f (x) : = m f (- x)$ . Then

H H_{0} (R, M) ≅ Q, H H_{1} (R, M) = 0, H H_{j} (R, M) = 0 (j \geq 2) .

Facts & Assumptions

Given: AC, $R = Q [x]$ , the usual left $R$ -module $M = R$ , and the right action $m \cdot f (x) = m f (- x)$ .

[F1]

Under AC, for a $k$ -central $R$ -bimodule $M$ , Hochschild homology is isomorphic to the homology of the coefficient Koszul complex, whose one-variable differential is $m θ_{1} \mapsto x m - m x$ (Polynomial Hochschild homology from the diagonal Koszul complex).

[F2]

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

[F3]

The assumed Axiom of Choice is the choice-function principle (The Axiom of Choice); it licenses the AC-qualified polynomial Hochschild theorem used at step 2.1.

Verification

technique · direct

1.1F2givenalgebra

Verify the twisted right action and the bimodule hypotheses. [F2, given] Define $σ (f (x)) = f (- x)$ . Since $σ (f g) = σ (f) σ (g)$ , $σ (1) = 1$ , and $σ^{2} = id$ , it is a unital ring automorphism of $R$ . Put $m \cdot f = m σ (f)$ . Then $m \cdot 1 = m$ and $(m \cdot f) \cdot g = m σ (f) σ (g) = m σ (f g) = m \cdot (f g)$ , so this is a unital right action. In particular $m \cdot x = - m x = - x m$ . For $r, f \in R$ , $r (m \cdot f) = r m σ (f) = (r m) \cdot f$ , using commutativity of $R$ ; hence the left and right actions commute. Since $σ (q) = q$ for $q \in Q$ , the two scalar actions agree. Thus $M$ is a $Q$ -central $R$ -bimodule, as required by [F1].

2.1F1F3step 1.1algebra

Write the one-variable coefficient complex and compute its map. [F1, F2, step 1.1, algebra] Under the AC premise [F3], [F1] computes $H H_{∙} (R, M)$ by the two-term complex $M θ_{1} \overset{d}{\to} M$ . Its differential is $d (m θ_{1}) = x m - m \cdot x = x m - (- x m) = 2 x m$ . There are no terms above degree one.

3.1F1step 2.1algebra

Compute the kernel and cokernel of multiplication by $2 x$ . [F1, step 2.1, algebra] If $0 \neq f (x) = a_{d} x^{d} + \dots$ with $a_{d} \neq 0$ , then $2 x f (x)$ has leading coefficient $2 a_{d} \neq 0$ in $Q$ , so $d$ is injective. Because $2$ is a unit, its image is $2 x Q [x] = x Q [x]$ . Evaluation at zero $ε : Q [x] \to Q$ is surjective and has kernel $x Q [x]$ : a polynomial with zero constant coefficient is divisible by $x$ . Thus $coker d ≅ Q$ and $\ker d = 0$ , giving $H H_{0} (R, M) ≅ Q$ and $H H_{1} (R, M) = 0$ . The terms above degree one vanish, so $H H_{j} (R, M) = 0$ for $j \geq 2$ .

4.1

Check grading, endpoints, and the exact AC use. [F1, F2, step 2.1, step 3.1, given] If $\deg_{i n t} x = 2$ , then $f (x) \mapsto f (- x)$ preserves degree, and the Koszul generator $θ_{1}$ has internal degree $2$ ; hence the degree-one term is the corresponding shift of $M$ and $d$ has internal degree zero. Degree zero is the cokernel computed in step 3.1; degree one is the kernel, with no incoming term from degree two; all higher terms are zero. AC is used only to apply the polynomial Hochschild theorem in step 2.1. The action, leading-term injectivity, and evaluation quotient are explicit and use no choice. The example is a computation, not an equivalence. [F1, F2, step 1.1, step 2.1, step 3.1, algebra] $□$

Source comparison

Weibel, An Introduction to Homological Algebra, §9.1.3 and Exercise 9.1.3, printed pp.302–304/PDF pp.2–4, gives the enveloping/bar framework and poses the polynomial Koszul computation as an exercise, but does not treat this twist. Khovanov, “Hochschild homology,” PDF p.1, lines 41–60, describes the polynomial Koszul complex and the coefficient maps $x_{i} m - m x_{i}$ . The automorphism twist and its kernel/cokernel calculation are proved explicitly above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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, §9.1.3 and 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)