ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-13

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.

$Z [x]$ represents the underlying-set functor on unital rings

Example

Let $U : R i n g \to S e t$ send a unital ring to its underlying set and a unit-preserving ring homomorphism to its underlying function. The ring $Z [x]$ represents $U$ . Explicitly, for every unital ring $R$ , not assumed commutative, evaluation at $r \in R$ gives the natural bijection

$R i n g (Z [x], R) \overset{≅}{\to} U (R), ϕ ⟼ ϕ (x),$

whose inverse is

$r ⟼ {ev}_{r}, {ev}_{r} (\sum_{i} a_{i} x^{i}) = \sum_{i} (a_{i} 1_{R}) r^{i} .$

Facts & Assumptions

Given: An arbitrary unital ring $R$ , an element $r \in R$ , and finitely supported integer coefficient sequences $p = (a_{i})$ and $q = (b_{j})$ .

[F1]

Unital rings and unit-preserving ring homomorphisms form the large locally small category $R i n g$ (Unital rings and unit-preserving ring homomorphisms form the large locally small category $R i n g$ ).

[F2]

For a commutative ring $A$ , $A [x]$ consists of finitely supported coefficient sequences, with coefficientwise addition and convolution $(p q)_{n} = \sum_{i + j = n} a_{i} b_{j}$ (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

[L1]

The integers form a commutative unital ring, and the operations of [F2] make $Z [x]$ a commutative unital ring whose constant-polynomial map is an injective unital homomorphism (The integers form a commutative ring, Polynomial convolution makes $R [x]$ a commutative ring containing $R$ as its constant subring).

[L2]

In any ring, $a 1_{R}$ is central and $(a 1_{R}) (b 1_{R}) = (a b) 1_{R}$ for integers $a, b$ ; more generally integer multiples distribute over addition and multiplication (Integer multiples in a ring: $(m + n) a = m a + n a$ , $m (a + b) = m a + m b$ , $(m a) b = m (a b) = a (m b)$ and $(m a) (n b) = (m n) (a b)$ for all $m, n \in Z$ and $a, b \in R$ ).

[F3]

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

[F4]

Natural powers are finite products with $r^{0} = 1_{R}$ , and the splitting law gives $r^{i + j} = r^{i} r^{j}$ (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity, Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either).

[L3]

Finite sums in a commutative monoid may be reindexed, split, and summed in either order over a finite product (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[F5]

A covariant functor is represented by $A$ when it is naturally isomorphic to the hom-functor $R i n g (A, -)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

Verification

technique · constructive

1.1

The assignment $U$ preserves identities and composition because it leaves their underlying functions unchanged, so [F1] makes it a functor $R i n g \to S e t$ .

1.2

Because $p$ has finite support, the displayed sum defining ${ev}_{r} (p)$ is finite and is independent of any larger finite support bound by adjoining zero terms. It sends $1$ to $(1 \cdot 1_{R}) r^{0} = 1_{R}$ .

F2L1L2F4construct

1.3

Coefficientwise addition, distributivity of integer multiples, and finite-sum splitting give ${ev}_{r} (p + q) = {ev}_{r} (p) + {ev}_{r} (q)$ .

F2L2L3

1.4

Conversely, let $ϕ : Z [x] \to R$ be a unital ring homomorphism and put $r = ϕ (x)$ . From $ϕ (1) = 1_{R}$ and additivity, including additive inverses, $ϕ$ sends the constant $a$ to $a 1_{R}$ for every integer $a$ ; multiplicativity gives $ϕ (x^{i}) = r^{i}$ . Additivity over the finite expression $p = \sum_{i} a_{i} x^{i}$ then gives $ϕ (p) = \sum_{i} (a_{i} 1_{R}) r^{i} = {ev}_{r} (p)$ .

L1L2F3F4

2.1

Expanding a product of the two finite evaluation sums and using [L3] gives ${ev}_{r} (p) {ev}_{r} (q) = \sum_{i, j} (a_{i} 1_{R}) r^{i} (b_{j} 1_{R}) r^{j} .$ Since $b_{j} 1_{R}$ is central by [L2], each summand is $((a_{i} b_{j}) 1_{R}) r^{i} r^{j} = ((a_{i} b_{j}) 1_{R}) r^{i + j}$ by [F4].

step 1.2L2F4L3

2.2

The polynomial $x$ has only coefficient $1$ at index $1$ , so ${ev}_{r} (x) = r$ . Hence evaluation at $x$ after $r \mapsto {ev}_{r}$ recovers $r$ .

step 1.2F2F4

3.1

Reindex the last finite sum by $n = i + j$ and regroup its fibres. By [F2] and [L3] the inner coefficient sum is $(p q)_{n}$ , so the result is ${ev}_{r} (p q)$ . Together with steps 1.2 and 1.3, [F3] makes ${ev}_{r} : Z [x] \to R$ a unital ring homomorphism, without any commutativity hypothesis on $R$ .

step 1.2step 1.3step 2.1F2F3L3

4.1

Steps 2.2 and 1.4 make $ϕ \mapsto ϕ (x)$ and $r \mapsto {ev}_{r}$ inverse bijections. If $h : R \to S$ is a unital ring homomorphism, then $h \circ {ev}_{r}$ and ${ev}_{h (r)}$ have the same value $h (r)$ at $x$ , so step 1.4 makes them equal; the bijection is natural in $R$ .

step 3.1step 2.2step 1.4F3

5.1

By [F5], $Z [x]$ represents $U$ . The proof includes the zero ring: when $0_{R} = 1_{R}$ , its underlying set and the hom-set from $Z [x]$ are both singletons, and the same formulas apply.

step 1.1step 4.1F5discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

60 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

Emily Riehl, Category Theory in Context, Example 2.4.12(vi) (standard reference, not scraped)

Z[x]Z[x] represents the underlying-set functor on unital rings