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.

Hochschild homology of the ground field

Statement

Let $k$ be a field and give $A = k$ its regular $k$ -bimodule. Then

$H H_{0} (k, k) ≅ k, H H_{j} (k, k) = 0 (j > 0) .$

Facts & Assumptions

Given: A field $k$ , considered as a unital associative algebra over itself and with its regular bimodule.

[F1]

The Hochschild chain terms are $C_{0} (A, M) = M$ and $C_{n} (A, M) = M \otimes_{k} A^{\otimes_{k} n}$ for $n \geq 1$ (Hochschild chains and Hochschild homology with coefficients).

[F2]

On $m \otimes a_{1} \otimes \dots \otimes a_{n}$ , the faces are the first action $(m a_{1}) \otimes a_{2} \otimes \dots \otimes a_{n}$ , the internal products $m \otimes a_{1} \otimes \dots \otimes (a_{i} a_{i + 1}) \otimes \dots \otimes a_{n}$ , and the last cyclic action $(a_{n} m) \otimes a_{1} \otimes \dots \otimes a_{n - 1}$ (Hochschild chains and Hochschild homology with coefficients).

[F3]

Set $b_{0} = 0$ ; for $n \geq 1$ , the Hochschild boundary is $b_{n} = \sum_{i = 0}^{n} (- 1)^{i} δ_{i}^{(n)}$ (Hochschild chains and Hochschild homology with coefficients).

[F4]

Hochschild homology is $H H_{n} (A, M) = H_{n} (C_{∙} (A, M))$ (Hochschild chains and Hochschild homology with coefficients).

[F5]

There is a canonical isomorphism $H H_{0} (A, M) ≅ M / {span}_{k} {a m - m a : a \in A, m \in M}$ (Degree-zero Hochschild homology is bimodule coinvariants).

[F6]

For zero variables, the diagonal Koszul sequence and exterior generators are empty, $R = k$ , $R^{e} = k$ , and the complex is $k$ in degree zero with identity augmentation (The polynomial diagonal Koszul bimodule complex).

[F7]

A finite parenthesized tensor product represents multilinear maps, and different parenthesizations are related by canonical isomorphisms preserving pure tensors (Finite iterated tensor products represent multilinear maps independently of parenthesization).

[F8]

The maps $k \otimes_{k} V \to V$ and $V \otimes_{k} k \to V$ given by scalar actions are isomorphisms (The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ ).

Proof

technique · direct

1.1F1F7F8givenalgebra

For $n \geq 1$ , write a pure tensor in $C_{n} (k, k)$ as $c_{0} \otimes \dots \otimes c_{n}$ . The multilinear product map $ϕ_{n} (c_{0} \otimes \dots \otimes c_{n}) = c_{0} \dots c_{n}$ is well-defined by [F7] and is an isomorphism by repeated application of the tensor-unit maps [F8]; its inverse sends $c$ to $c \otimes 1 \otimes \dots \otimes 1$ . Indeed, the balancing relations let each scalar factor move to the first slot, so the composite with $ϕ_{n}$ is the identity in either order. For $n = 0$ , use the identity $C_{0} (k, k) = k$ . Thus identify every chain group with $k$ .

2.1F2F3step 1.1givenalgebra

Under these identifications every face $δ_{i}^{(n)}$ preserves the product of the scalar entries: the first and last formulas in [F2] use the regular scalar actions, while each internal formula multiplies two scalars. Hence each face is ${id}_{k}$ , so by [F3], $b_{n} = \sum_{i = 0}^{n} (- 1)^{i} {id}_{k}$ ; pairing consecutive terms gives $b_{n} = 0$ for odd $n$ and $b_{n} = {id}_{k}$ for even $n \geq 2$ . Also $b_{0} = 0$ . In particular, $b_{1} = 0$ and $b_{2} = {id}_{k}$ .

3.1F1F3F4F5step 2.1givenalgebra

Since $C_{0} (k, k) = k$ and $b_{0} = b_{1} = 0$ , the degree-zero homology is $k$ . Equivalently, [F5] gives the quotient by the span of $a b - b a$ , which is zero because $k$ is commutative. If $j > 0$ is even, then $b_{j} = {id}_{k}$ , so the cycle group is zero. If $j$ is odd, then $b_{j} = 0$ and $b_{j + 1} = {id}_{k}$ , so every cycle is a boundary. By [F4], these are exactly $H H_{0} (k, k) ≅ k$ and $H H_{j} (k, k) = 0$ for $j > 0$ .

4.1F1F2F3F6step 2.1step 3.1givenalgebra∎

Let $K$ be the diagonal Koszul complex for the zero-variable polynomial ring $R = k$ . By [F6], $K$ is $k$ in degree zero and zero in positive degrees, with identity augmentation. The maps $p : C_{∙} (k, k) \to K$ and $i : K \to C_{∙} (k, k)$ are identity in degree zero and zero in positive degrees for $p$ , and the degree-zero identity inclusion for $i$ . Define $h_{n} : C_{n} (k, k) \to C_{n + 1} (k, k)$ to be the identity under [F1]'s scalar identifications when $n$ is odd and zero when $n$ is even; put $h_{- 1} = 0$ . For $n = 0$ , $b_{1} h_{0} + h_{- 1} b_{0} = 0 = id - i p$ . For $n > 0$ , the parity formulas in step 2.1 give $b_{n + 1} h_{n} + h_{n - 1} b_{n} = {id}_{C_{n}}$ . Thus $h$ is a chain homotopy from ${id}_{C_{∙}}$ to $i p$ , and $C_{∙} (k, k)$ is chain-homotopy equivalent to the empty diagonal Koszul complex. Its homology matches the calculation in step 3.1. This direct comparison uses no general AC-bearing polynomial comparison theorem and no choice.

Source notes

Weibel, An Introduction to Homological Algebra, §9.1.1, printed p. 300/PDF p. 0, lines 6–19, gives the unnormalized Hochschild chain and face conventions and the degree-zero coinvariant formula. It does not perform the alternating sum calculation for $A = k$ ; the scalar identifications, parity calculation, and chain homotopy above are supplied directly here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

33 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.1 (standard reference, not scraped)