TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11

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 $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism

Statement

Let $R, S$ be commutative rings, let $φ ⁣ : R \to S$ be a unital ring homomorphism, and let $s \in S$ . There is a unique unital ring homomorphism

${ev}_{φ, s} ⁣ : R [x] \to S$

that extends $φ$ on constant polynomials and sends $x$ to $s$ . It is given by ${ev}_{φ, s} (\sum_{i} a_{i} x^{i}) = \sum_{i} φ (a_{i}) s^{i}$ .

Facts & Assumptions

Given: Commutative rings $R, S$ , a unital ring homomorphism $φ ⁣ : R \to S$ , and an element $s \in S$ .

[L1]

Evaluation is the finite sum $f_{φ} (s) = \sum_{i} φ (a_{i}) s^{i}$ (Evaluation and roots of a polynomial in a commutative target ring).

[L2]

Polynomial convolution makes $R [x]$ a commutative ring with constant embedding $c ⁣ : R \to R [x]$ (Polynomial convolution makes $R [x]$ a commutative ring containing $R$ as its constant subring).

[L3]

Finitely supported sequences and trimmed coefficient lists have the same coefficients and operations (Finitely supported coefficient sequences and trimmed finite coefficient lists define the same formal polynomials).

[L4]

A ring homomorphism preserves addition, multiplication, and one (Ring homomorphism: additive, multiplicative, and required to send $1$ to $1$ ).

[L5]

Finite sums may be reindexed and iterated over finite products (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

Proof

technique · direct

1.1givenL1L2L4L5algebra

The formula in [L1] preserves sums term by term, sends $1$ to $1$ , and sends a convolution product to $\sum_{i, j} φ (a_{i}) φ (b_{j}) s^{i + j} = (\sum_{i} φ (a_{i}) s^{i}) (\sum_{j} φ (b_{j}) s^{j})$ by [L5]; thus [L4] makes it a unital ring homomorphism, and [L2] shows that it extends $φ$ and sends $x$ to $s$ .

2.1step 1.1L2L3L4∎

If $ψ ⁣ : R [x] \to S$ is another such homomorphism, [L3] writes every polynomial as a finite sum $\sum_{i} c (a_{i}) x^{i}$ , so [L4] forces $ψ (f) = \sum_{i} φ (a_{i}) s^{i}$ ; hence $ψ = {ev}_{φ, s}$ and uniqueness holds.

Depends on

Dependency tree · 2 levels

Sources

James McKernan, MIT 18.703 Lecture 21, Lemma 21.3

Universal property of R[x]R[x]: a coefficient homomorphism and the image of xx determine a unique ring homomorphism