LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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 first three Stasheff identities

Statement

Let $(A, m_{n})$ be an uncurved cohomological A∞-algebra with the unsuspended convention of Uncurved cohomological A∞-algebra in the unsuspended convention. Its first three identities are

$m_{1} m_{1} = 0,$

$m_{1} m_{2} = m_{2} (m_{1} \otimes 1 + 1 \otimes m_{1}),$

and

$m_{1} m_{3} + m_{3} (m_{1} \otimes 1 \otimes 1 + 1 \otimes m_{1} \otimes 1 + 1 \otimes 1 \otimes m_{1}) + m_{2} (m_{2} \otimes 1) - m_{2} (1 \otimes m_{2}) = 0.$

In particular, $m_{1}$ is a cochain differential and a signed derivation of $m_{2}$ . The third identity explicitly gives the associator $m_{2} (m_{2} \otimes 1) - m_{2} (1 \otimes m_{2})$ as the negative of the displayed $m_{1}, m_{3}$ terms.

Facts & Assumptions

Given: An uncurved cohomological A∞-algebra $(A, m_{n})$ over a field, with the Koszul tensor convention specified in its definition.

[F1]

Uncurved cohomological A∞-algebra in the unsuspended convention: for each $n \geq 1$ , $\sum_{r + s + t = n, s \geq 1} (- 1)^{r + s t} m_{r + 1 + t} (1^{\otimes r} \otimes m_{s} \otimes 1^{\otimes t}) = 0.$

[F2]

Koszul sign rule for graded tensor products and permutations: for homogeneous maps and inputs, $(f \otimes g) (x \otimes y) = (- 1)^{∣ g ∣ ∣ x ∣} f (x) \otimes g (y)$ .

Proof

1.1givenF1

For $n = 1$ , the only triple $(r, s, t)$ is $(0, 1, 0)$ , so [F1] is exactly $m_{1} m_{1} = 0$ .

1.2F1F2algebra

For $n = 2$ , the triples are $(0, 1, 1)$ , $(1, 1, 0)$ , and $(0, 2, 0)$ ; their coefficients are $- 1, - 1, + 1$ . Hence [F1] gives $m_{1} m_{2} - m_{2} (m_{1} \otimes 1) - m_{2} (1 \otimes m_{1}) = 0$ . On homogeneous $a, b$ , [F2] makes the last term $(- 1)^{∣ a ∣} m_{2} (a, m_{1} b)$ , which is the signed derivation rule.

2.1F1algebra∎

For $n = 3$ , the triples with $s = 1$ contribute the three terms $m_{3} (m_{1} \otimes 1 \otimes 1)$ , $m_{3} (1 \otimes m_{1} \otimes 1)$ , $m_{3} (1 \otimes 1 \otimes m_{1})$ , each with sign $+ 1$ ; $s = 2$ contributes $m_{2} (m_{2} \otimes 1) - m_{2} (1 \otimes m_{2})$ ; and $s = 3$ contributes $m_{1} m_{3}$ . Their sum is the third displayed identity.

Depends on

Used by

A differential graded algebra is an A∞-algebra with no higher products Proposition

Dependency tree · two levels

6 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

Bernhard Keller, Introduction to A-infinity algebras and modules, §3.1 (standard reference, not scraped)