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 reduced graded symmetric coalgebra is cofree conilpotent cocommutative

Statement

Let $W$ be a graded vector space over a characteristic-zero field and let $S^{c} (W)$ be the reduced graded symmetric coalgebra of Reduced graded symmetric coalgebra with its shuffle coproduct. Let $C$ be any graded $k$ -vector space with a degree-zero reduced coproduct ${\overset{ˉ}{Δ}}_{C} : C \to C \otimes_{k} C$ that is coassociative and graded-cocommutative (invariant under the graded flip), with no counit. Assume that for every $c \in C$ some iterated reduced coproduct of $c$ is zero; such a coalgebra is called conilpotent here. A coalgebra morphism is a degree-zero linear map commuting with the reduced coproduct. For any degree-zero linear map $ϕ : C \to W$ , there is a unique degree-zero coalgebra morphism $G : C \to S^{c} (W)$ whose length-one projection is $ϕ$ . Explicitly, let $ρ_{n} : W^{\otimes n} \to S^{n} (W)$ be the quotient map, put ${\overset{ˉ}{Δ}}_{C}^{(0)} = {id}_{C}$ , and define iterates recursively by ${\overset{ˉ}{Δ}}_{C}^{(n)} = ({\overset{ˉ}{Δ}}_{C}^{(n - 1)} \otimes 1) {\overset{ˉ}{Δ}}_{C}$ ; coassociativity makes the parenthesization immaterial. Then

$G (c) = \sum_{n \geq 1} \frac{1}{n!} ρ_{n} ⁣ (ϕ^{\otimes n} {\overset{ˉ}{Δ}}_{C}^{(n - 1)} (c)) .$

The sum is finite for each $c$ by conilpotence. In particular, the graded symmetric coalgebra is the reduced cofree conilpotent cocommutative coalgebra on $W$ .

Facts & Assumptions

Given: A conilpotent graded cocommutative noncounital coalgebra $C$ , a graded vector space $W$ over a characteristic-zero field, and a degree-zero linear map $ϕ : C \to W$ .

[F1]

Reduced graded symmetric coalgebra with its shuffle coproduct: $S^{c} (W)$ is the direct sum of the positive graded symmetric powers with the reduced shuffle coproduct.

[F2]

The graded shuffle coproduct is coassociative, cocommutative, and conilpotent: $S^{c} (W)$ is coassociative and cocommutative, and its primitive subspace is $W$ .

[F3]

Field, The characteristic of a ring: the least $n \geq 1$ with $n \cdot 1_{R} = 0$ when one exists, and $0$ otherwise, and Every field is a commutative ring with $1 \neq 0$ ; it is an integral domain, and it is a commutative division ring: the ground field has characteristic zero, so every $n!$ is nonzero and invertible.

[F4]

Koszul sign rule for graded tensor products and permutations: graded permutations and tensor maps use the displayed Koszul signs.

Proof

1.1givenF1construct

For fixed $c \in C$ , conilpotence makes ${\overset{ˉ}{Δ}}_{C}^{(n - 1)} (c) = 0$ for all sufficiently large $n$ , so the displayed sum defines an element of the direct sum $S^{c} (W)$ . Its length-one projection is the $n = 1$ term $ϕ (c)$ ; every $n > 1$ term has length $n$ and projects to zero.

1.2F1F2F4algebra

To check the coalgebra-map identity, fix $n = p + q$ in the formula for $G (c)$ and put $D_{n} = {\overset{ˉ}{Δ}}_{C}^{(n - 1)} (c)$ . Coassociativity and cocommutativity imply that $D_{n}$ is invariant under graded permutations of its $n$ outputs: adjacent swaps follow by applying coassociativity to isolate two adjacent outputs and then using cocommutativity on that pair. Applying the shuffle coproduct to the length- $n$ symmetric class sums over the $(\binom{n}{p})$ choices of the $p$ labels in the first block. Since $D_{n}$ is graded-symmetric, these choices give the same projected class, with the Koszul signs prescribed by [F4]. Their total coefficient is $(\binom{n}{p}) / n! = 1 / (p! q!)$ . On the other side, $(G \otimes G) {\overset{ˉ}{Δ}}_{C} (c)$ has the same grouped iterated coproduct by coassociativity, and its length- $(p, q)$ coefficient is also $1 / (p! q!)$ . Thus the two sides agree in every length and $\overset{ˉ}{Δ} G = (G \otimes G) {\overset{ˉ}{Δ}}_{C}$ .

1.3F1F2algebra

Suppose $G^{'}$ is another coalgebra morphism with $π_{1} G^{'} = ϕ$ . Applying the iterated coproduct into $n$ factors and then $π_{1}^{\otimes n}$ gives $π_{1}^{\otimes n} {\overset{ˉ}{Δ}}_{S^{c} (W)}^{(n - 1)} G^{'} (c) = ϕ^{\otimes n} {\overset{ˉ}{Δ}}_{C}^{(n - 1)} (c) .$ Only the length- $n$ component of $G^{'} (c)$ can survive on the left: a shorter length cannot split into $n$ positive factors, while a longer length leaves some factor of length greater than one, killed by $π_{1}$ . This length behavior follows directly from the coproduct in [F1].

2.1F1F2F3F4step 1.3∎

For a length- $n$ element, the left side of step 1.3 is the sum over all $n!$ permutations in the iterated unshuffle coproduct. Applying $ρ_{n}$ to that tensor sum yields $n!$ times the length- $n$ component, because all permuted factors represent the same graded-symmetric class with their Koszul signs canceled by the quotient relation. Hence that component is forced to be $\frac{1}{n!} ρ_{n} ⁣ (ϕ^{\otimes n} {\overset{ˉ}{Δ}}_{C}^{(n - 1)} (c)),$ which is the length- $n$ component in the displayed formula for $G$ . Since this holds for every $n$ , $G^{'} = G$ .

Depends on

Used by

Shifted coalgebra definition of an L∞-algebra Definition

Cited to discharge well-definedness by Reduced graded symmetric coalgebra with its shuffle coproduct.

Dependency tree · two levels

25 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, §§2–3 (standard reference, not scraped)
Jean-Louis Loday and Bruno Vallette, Algebraic Operads, Proposition 10.1.20 (standard reference, not scraped)