TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Universal property of the symmetric algebra

Statement

If $A$ is a commutative unital $k$ -algebra, every linear map $f : V \to A$ extends uniquely to a unital algebra homomorphism $\tilde{f} : S (V) \to A$ .

Facts & Assumptions

Given: A vector space $V$ , a commutative unital $k$ -algebra $A$ , and a linear map $f : V \to A$ .

[L1]

The tensor-algebra universal property extends $f$ uniquely to a unital algebra map $\hat{f} : T (V) \to A$ (Universal property of the tensor algebra).

[L2]

A ring homomorphism killing an ideal factors uniquely through the quotient (A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring).

[L3]

$S (V) = T (V) / J$ , where $J$ is generated by commutativity relators (Symmetric algebra of a vector space).

Proof

technique · direct

1.1

Apply [L1] to obtain $\hat{f}$ . For every generator of $J$ , commutativity of $A$ gives $\hat{f} (v \otimes w - w \otimes v) = f (v) f (w) - f (w) f (v) = 0$ , so $J \subseteq \ker \hat{f}$ .

L1L3algebra

2.1

By [L2], $\hat{f}$ factors through a unique unital algebra map $\tilde{f} : S (V) \to A$ , and its restriction to the image of $V$ is $f$ .

step 1.1L2

3.1

If $G : S (V) \to A$ is another such map, its composite with $T (V) ↠ S (V)$ is a unital algebra extension of $f$ , hence equals $\hat{f}$ by [L1]. Surjectivity of the quotient map gives $G = \tilde{f}$ .

step 2.1L1L3algebra

4.1

Therefore $\tilde{f}$ exists uniquely, with no basis or finite-dimensional hypothesis on $V$ .

step 2.1step 3.1∎

Depends on

Used by

PBW symbol map from the symmetric algebra Definition
Ordered monomial basis of a symmetric algebra Lemma

Dependency tree · two levels

16 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

Etingof, MIT 18.745 notes, §13.1, printed pp. 74–75 (standard reference, not scraped)