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 two-sided bar complex is a projective $A^{e}$ -resolution

Statement

Assume the Axiom of Choice (AC). Let $k$ be a field and $A$ a unital associative $k$ -algebra. The augmented two-sided bar complex $\dots ⟶ {Bar}_{1} (A) ⟶ {Bar}_{0} (A) \overset{ε}{\to} A$ is a projective resolution of $A$ both as a right and as a left $A^{e} = A \otimes_{k} A^{o p}$ -module. The contraction below is $k$ -linear; it is not asserted to be $A^{e}$ -linear.

Facts & Assumptions

Given: AC, a field $k$ , and a unital associative $k$ -algebra $A$ .

[F1]

The bar terms, adjacent-multiplication differential, and multiplication augmentation are as defined in The augmented two-sided bar complex.

[F2]

Each bar term has the separate outer left and right $A^{e}$ -actions specified in The augmented two-sided bar complex.

[F3]

The maps are linear for both outer actions and satisfy $d_{n - 1} d_{n} = 0$ and $ε d_{1} = 0$ (The bar boundary squares to zero and is augmented).

[F4]

The regular bimodule $A$ has the left and right $A^{e}$ -actions specified by the enveloping-algebra dictionary (Enveloping algebra and the bimodule–module dictionary).

[F5]

Under AC every vector space has a basis (Every vector space has a basis).

[F6]

The elementary tensors of two bases form a basis of their tensor product (The elementary tensors of two bases form the product basis of the tensor product).

[F7]

Tensor products commute with arbitrary direct sums in either variable (Tensor products commute with arbitrary direct sums).

[F8]

$k \otimes_{k} V ≅ V ≅ V \otimes_{k} k$ (The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ ).

[F9]

A module with a basis indexed by $X$ is isomorphic to the free module $R^{(X)}$ (The free module on a set and its standard basis).

[F10]

Under AC every free module is projective (Free modules are projective, with the exact choice boundary).

[F11]

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

[F12]

A right $E$ -module is regarded as a left $E^{o p}$ -module by $r^{o p} m : = m r$ ; conversely a left $E^{o p}$ -module gives a right $E$ -module (Unital left and right modules over a ring; unqualified module means left module, The opposite ring $R^{o p}$ ).

[F13]

For every ring $E$ , the category of left $E$ -modules is abelian (Modules over a ring form an abelian category).

[F14]

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

[F15]

A multilinear prescription on finitely many tensor factors induces a linear map from their tensor product (Finite iterated tensor products represent multilinear maps independently of parenthesization).

[F16]

Kernels and images of module homomorphisms are the usual kernel and image submodules (Module homomorphism and isomorphism, kernel, image and cokernel).

Proof

technique · direct

1.1F1F8F15givenalgebra

Define $h_{- 1} : A \to {Bar}_{0} (A)$ by $h_{- 1} (a) = 1 \otimes a$ , and for $n \geq 0$ define $h_{n} (a_{0} \otimes \dots \otimes a_{n + 1}) = 1 \otimes a_{0} \otimes \dots \otimes a_{n + 1} .$ The formulas are $k$ -multilinear, so [F15] makes them well-defined $k$ -linear maps. In $d_{n + 1} h_{n}$ , the first face is the identity term $a_{0} \otimes \dots \otimes a_{n + 1}$ . Every later face, with index $r \geq 1$ , is $- h_{n - 1}$ applied to the face of index $r - 1$ in $d_{n}$ , since $(- 1)^{r} = - (- 1)^{r - 1}$ . For $n = 0$ , this gives $d_{1} h_{0} (a_{0} \otimes a_{1}) = a_{0} \otimes a_{1} - 1 \otimes a_{0} a_{1}$ , while $h_{- 1} ε (a_{0} \otimes a_{1}) = 1 \otimes a_{0} a_{1}$ . For $n = 1$ , $d_{2} h_{1} (a_{0} \otimes a_{1} \otimes a_{2}) = a_{0} \otimes a_{1} \otimes a_{2} - 1 \otimes a_{0} a_{1} \otimes a_{2} + 1 \otimes a_{0} \otimes a_{1} a_{2}$ , and $h_{0} d_{1} (a_{0} \otimes a_{1} \otimes a_{2}) = 1 \otimes a_{0} a_{1} \otimes a_{2} - 1 \otimes a_{0} \otimes a_{1} a_{2}$ . In general the same opposite-sign pairing yields $d_{n + 1} h_{n} + h_{n - 1} d_{n} = 1 (n \geq 0),$ where $d_{0} : = ε$ , and $ε h_{- 1} = 1_{A}$ . If $A = k$ , [F8] identifies every bar term with $k$ and every face with the identity, so $d_{n} = (\sum_{r = 0}^{n} (- 1)^{r}) 1_{k}$ is zero for odd $n$ and the identity for even $n$ .

1.2F1F2F5F6F7F8F9F11F12F15givenalgebra

By the assumed AC [F11] and the basis theorem [F5], choose a $k$ -basis $B$ of $A$ . For every $n \geq 1$ , [F6] applied inductively gives the basis of $A^{\otimes_{k} n}$ consisting of tensors $b_{1} \otimes \dots \otimes b_{n}$ with $b_{i} \in B$ . For $n = 0$ , use the basis ${1_{k}}$ of $A^{\otimes_{k} 0} = k$ . Let $B_{n}$ denote these basis index sets. Using [F7]–[F9], $A^{\otimes_{k} n} \otimes_{k} A^{e} ≅ ⨁_{B_{n}} (k \otimes_{k} A^{e}) ≅ (A^{e})^{(B_{n})}$ as right $A^{e}$ -modules, where the canonical map on pure tensors is $((a_{1} \otimes \dots \otimes a_{n}) \otimes (a \otimes b^{o p})) ⟼ b \otimes a_{1} \otimes \dots \otimes a_{n} \otimes a .$ For $n = 0$ , it sends $1_{k} \otimes (a \otimes b^{o p})$ to $b \otimes a$ . The inverse extracts the middle tensor and the two outer factors; multilinearity makes both maps well-defined by [F15]. By [F2], multiplication by $c \otimes d^{o p}$ sends the outer factors to $d b$ and $a c$ on each side, so this isomorphism respects the right action. By [F12], this right free module is a free left $(A^{e})^{o p}$ -module.

2.1step 1.2F1F2F6F7F8F9F15givenalgebra

Similarly, $A^{e} \otimes_{k} A^{\otimes_{k} n} ≅ ⨁_{B_{n}} (A^{e} \otimes_{k} k) ≅ (A^{e})^{(B_{n})}$ as left $A^{e}$ -modules, by the map $((a \otimes b^{o p}) \otimes (a_{1} \otimes \dots \otimes a_{n})) ⟼ a \otimes a_{1} \otimes \dots \otimes a_{n} \otimes b .$ For $n = 0$ , it sends $(a \otimes b^{o p}) \otimes 1_{k}$ to $a \otimes b$ . The inverse extracts the two outer factors and the middle tensor. Left multiplication by $c \otimes d^{o p}$ sends those outer factors to $c a$ and $b d$ on both sides, by [F2], and [F15] makes the maps well-defined. Thus, using the separate outer actions in [F1]–[F2] and the basis in step 1.2, every bar term is free on both sides.

2.2step 1.1F3F4F12F16givenalgebra

If $z \in \ker ε$ , step 1.1 gives $z = d_{1} h_{0} (z)$ . If $n \geq 1$ and $z \in \ker d_{n}$ , it gives $z = d_{n + 1} h_{n} (z)$ . Conversely, each image lies in the next kernel by [F3]. Also $ε h_{- 1} = 1_{A}$ , so $ε$ is onto. The augmented bar complex is therefore exact as a complex of $k$ -vector spaces. Since each differential and the augmentation are $A^{e}$ -linear by [F3] and the target actions are those of [F4], these elementwise kernel-image equalities are exactness in both module categories by [F12] and [F16]. The contraction need not be $A^{e}$ -linear.

3.1step 1.2step 2.1F10F11F12given

By the assumed AC [F11], each free module in steps 1.2 and 2.1 is projective by [F10], applying that theorem to the ring $A^{e}$ for left modules and $(A^{e})^{o p}$ for right modules via [F12]. Therefore every bar term is projective in both module categories.

4.1

By [F13], the left $A^{e}$ -module category and the left $(A^{e})^{o p}$ -module category are abelian; by [F12] the latter is the right $A^{e}$ -module category. Steps 2.2 and 3.1 give exactness and termwise projectivity in each category. Thus [F14] makes $Bar (A) \to A$ a projective resolution on both sides. AC is used to obtain a basis of $A$ and for projectivity of free modules with arbitrary basis; the contracting homotopy and exactness calculation are choice-free. [step 2.2, step 3.1, F11, F12, F13, F14, given] $□$

Depends on

Used by

Dependency tree · two levels

51 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, §9.1.3–9.1.5 (standard reference, not scraped)
Mikhail Khovanov, Triply-graded link homology and Hochschild homology of Soergel bimodules, Hochschild homology section (standard reference, not scraped)

The two-sided bar complex is a projective AeAe-resolution