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.

Square-zero coderivations are equivalent to the shifted higher Jacobi identities

Statement

Let $Q$ be the degree-one coderivation of Shifted coalgebra definition of an L∞-algebra, with corestrictions $q_{i} : S^{i} (W) \to W$ . For each $n \geq 1$ , define

$J_{n} (w_{1}, \dots, w_{n}) = \sum_{i = 1}^{n} \sum_{σ \in Sh (i, n - i)} ϵ (σ; w_{1}, \dots, w_{n}) q_{n - i + 1} ⁣ (q_{i} (w_{σ (1)} ⊙ \dots ⊙ w_{σ (i)}) ⊙ w_{σ (i + 1)} ⊙ \dots ⊙ w_{σ (n)}),$

where $Sh (n, 0)$ contains only the identity and an empty tail after $q_{i}$ is omitted. Then $Q^{2} = 0$ if and only if $J_{n} (w_{1}, \dots, w_{n}) = 0$ for every $n$ and all homogeneous $w_{j} \in W$ . These are the shifted higher Jacobi identities; for $n = 1$ the identity is $q_{1}^{2} = 0$ .

Facts & Assumptions

Given: A reduced graded symmetric coalgebra $S^{c} (W)$ , a degree-one coderivation $Q$ , and its corestrictions $q_{n}$ .

[F1]

Shifted coalgebra definition of an L∞-algebra: $Q$ has degree $+ 1$ and satisfies the coderivation equation with the graded tensor convention.

[F2]

Coderivations of the reduced graded symmetric coalgebra are determined by corestrictions: a coderivation is uniquely determined by its corestrictions.

[F3]

The graded shuffle coproduct is coassociative, cocommutative, and conilpotent: the only primitive elements of $S^{c} (W)$ are the length-one elements $W$ .

[F4]

Koszul sign rule for graded tensor products and permutations: moving homogeneous factors past one another contributes the displayed Koszul signs.

Proof

1.1F1F4algebra

The square $Q^{2}$ is a coderivation of degree $2$ . Indeed, applying the coderivation equation twice gives $\overset{ˉ}{Δ} Q^{2} = (Q \otimes 1 + 1 \otimes Q)^{2} \overset{ˉ}{Δ} = (Q^{2} \otimes 1 + 1 \otimes Q^{2}) \overset{ˉ}{Δ},$ because the two cross terms are $Q \otimes Q$ and $- Q \otimes Q$ by [F4].

1.2F1F2F4algebra

On an input of symmetric length $n$ , the projection $π_{1} Q^{2}$ can be nonzero only when the first application of $Q$ consumes $i$ inputs by $q_{i}$ and the second consumes the resulting $q_{i}$ output together with all $n - i$ unused inputs by $q_{n - i + 1}$ . The first application ranges over exactly the $(i, n - i)$ -unshuffles; its coefficient is $ϵ (σ; w_{1}, \dots, w_{n})$ , and the second unshuffle has only one term because it must consume every remaining factor. Thus $(π_{1} Q^{2}) ∣_{S^{n} (W)} = J_{n}$ .

2.1step 1.2algebra

If $Q^{2} = 0$ , then every projection $π_{1} Q^{2} ∣_{S^{n} (W)}$ is zero, so step 1.2 gives $J_{n} = 0$ for all $n$ .

2.2step 1.1step 1.2F3induction

Conversely, suppose $J_{n} = 0$ for every $n$ . By step 1.2, every corestriction of the coderivation $Q^{2}$ is zero. We show by induction on input length that $Q^{2} = 0$ . On length one it is zero by its corestriction. If it vanishes on all smaller lengths, its coderivation equation makes the reduced coproduct of $Q^{2} (x)$ zero for an input $x$ of the next length. By [F3], $Q^{2} (x)$ is then in $W$ , and its zero corestriction forces $Q^{2} (x) = 0$ .

3.1step 2.2discharge-induction∎

The induction covers every finite symmetric length, which exhausts the direct sum $S^{c} (W)$ . Hence $Q^{2} = 0$ , proving the converse.

Depends on

Used by

Cited to discharge well-definedness by Shifted coalgebra definition of an L∞-algebra.

Dependency tree · two levels

11 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

Tom Lada and Jim Stasheff, Introduction to sh Lie algebras for physicists, sh Lie Structures (standard reference, not scraped)
Jean-Louis Loday and Bruno Vallette, Algebraic Operads, §§10.1.12–10.1.20 (standard reference, not scraped)