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.

Coderivations of the reduced graded symmetric coalgebra are determined by corestrictions

Statement

Let $W$ and $S^{c} (W)$ be as in Reduced graded symmetric coalgebra with its shuffle coproduct. For any family of degree $+ 1$ graded-symmetric maps $q_{n} : S^{n} (W) \to W$ , $n \geq 1$ , the formula

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

defines a degree $+ 1$ coderivation of $S^{c} (W)$ . It is the unique such coderivation whose projection to $S^{1} (W) = W$ on $S^{n} (W)$ is $q_{n}$ . For $n = N$ , the final tail is empty and the term means just $q_{N} (w_{σ (1)} ⊙ \dots ⊙ w_{σ (N)})$ ; in this case $Sh (N, 0)$ contains only the identity permutation.

Here a degree-one coderivation is a linear map $Q : S^{c} (W) \to S^{c} (W)$ that satisfies

$\overset{ˉ}{Δ} Q = (Q \otimes 1 + 1 \otimes Q) \overset{ˉ}{Δ},$

where the tensor map $1 \otimes Q$ uses the Koszul sign rule. The sum defining $Q$ is finite on each input because $n \leq N$ .

Facts & Assumptions

Given: A characteristic-zero graded vector space $W$ , its reduced shuffle coalgebra, and graded-symmetric degree-one maps $q_{n} : S^{n} (W) \to W$ .

[F1]

Reduced graded symmetric coalgebra with its shuffle coproduct: the coproduct is a sum over unshuffles with Koszul signs, and its primitive subspace is $W$ by The graded shuffle coproduct is coassociative, cocommutative, and conilpotent.

[F2]

Koszul sign rule for graded tensor products and permutations: composing graded tensor maps and reordering homogeneous factors multiplies their Koszul signs.

Proof

1.1F1F2construct

The formula is well-defined on the graded-symmetric quotient: replacing a representative by an adjacent graded swap bijects the unshuffle summands, and the Koszul sign in [F2] gives the same graded-symmetric output. Each term is finite because its consumed arity is at most the input length.

1.2F1F2algebra

In $\overset{ˉ}{Δ} Q (x)$ , choose the $n$ input labels consumed by one $q_{n}$ , then split the $q_{n}$ output and the unused labels into two nonempty ordered blocks. The same terms occur in $(Q \otimes 1 + 1 \otimes Q) \overset{ˉ}{Δ} (x)$ by first splitting the original labels into those two blocks and applying $Q$ to the block containing the chosen $q_{n}$ inputs. These are the same ordered three-block decompositions; their signs agree by [F2], including the crossing sign from $1 \otimes Q$ . Thus the formula satisfies the coderivation identity.

1.3F1induction

Let $Q^{'}$ be another coderivation with the same corestrictions and put $D = Q - Q^{'}$ . We prove by induction on input length that $D = 0$ . On length one, $D$ is its zero corestriction. Assume $D = 0$ on all lengths below $N$ . For $x \in S^{N} (W)$ , every tensor factor in $\overset{ˉ}{Δ} (x)$ has length below $N$ ; the coderivation identity therefore gives $\overset{ˉ}{Δ} D (x) = 0$ . Hence $D (x)$ is primitive.

2.1F1step 1.3discharge-induction∎

By [F1], primitive elements are exactly $W$ , and the length-one projection of $D (x)$ is zero because $Q$ and $Q^{'}$ have the same corestrictions. Thus $D (x) = 0$ . This completes the induction for every finite length, so $Q = Q^{'}$ .

Depends on

Used by

Dependency tree · two levels

8 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, Proposition 10.1.20 (standard reference, not scraped)