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.

✓ 14 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 14 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Universal Properties, Representables and the Yoneda Lemma — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-13Open item page →

A Cartesian product represents $X \mapsto S e t (X, A) \times S e t (X, B)$

Example

For sets $A$ and $B$ , the presheaf

$F (X) = S e t (X, A) \times S e t (X, B)$

is represented by $A \times B$ . The representing natural isomorphism sends a function $f : X \to A \times B$ to its coordinate functions $(π_{A} \circ f, π_{B} \circ f)$ .

Facts & Assumptions

Given: Sets $A, B$ , the category $S e t$ , and an arbitrary set $X$ .

[F1]

A presheaf is represented by $R$ when it is naturally isomorphic to $S e t (-, R)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[F2]

Sets and functions form a locally small category whose composition and identities are ordinary function composition and identity functions (Sets and functions form the large locally small category $S e t$ ).

[F3]

The Cartesian product is $A \times B = {(a, b) : a \in A, b \in B}$ , and $(a, b) = (a^{'}, b^{'})$ holds exactly when $a = a^{'}$ and $b = b^{'}$ (The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ , $(a, b) = (c, d)$ if and only if $a = c$ and $b = d$ ). Hence $π_{A} (a, b) = a$ and $π_{B} (a, b) = b$ are well-defined functions.

[F4]

A function assigns each element of its domain exactly one element of its codomain, and two functions with the same domain and codomain are equal exactly when their values agree everywhere (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain, Functions $f$ and $g$ are equal if and only if $dom f = dom g$ and $f (x) = g (x)$ for every $x$ in that common domain).

Verification

technique · constructive

1.1

Define $Φ_{X} (f) = (π_{A} \circ f, π_{B} \circ f)$ for $f : X \to A \times B$ .

F2F3construct

1.2

For functions $g : X \to A$ and $h : X \to B$ , define $Ψ_{X} (g, h) : X \to A \times B$ by $Ψ_{X} (g, h) (x) = (g (x), h (x))$ .

F3F4construct

2.1

For every $(g, h)$ , the two projections of $Ψ_{X} (g, h)$ are $g$ and $h$ , so $Φ_{X} Ψ_{X} (g, h) = (g, h)$ .

step 1.1step 1.2F3F4

2.2

For every $f$ and $x \in X$ , $Ψ_{X} Φ_{X} (f) (x) = (π_{A} (f (x)), π_{B} (f (x))) = f (x)$ ; hence $Ψ_{X} Φ_{X} (f) = f$ .

step 1.1step 1.2F3F4

2.3

If $k : Y \to X$ , then $Φ_{Y} (f \circ k) = ((π_{A} \circ f) \circ k, (π_{B} \circ f) \circ k)$ , which is the restriction of $Φ_{X} (f)$ along $k$ in both factors. Thus $Φ$ is natural in $X$ .

step 1.1F2

3.1

Steps 2.1 and 2.2 make every $Φ_{X}$ bijective, and step 2.3 makes the family natural; by [F1], $A \times B$ represents $F$ .

step 2.1step 2.2step 2.3F1discharge-construct∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-13Open item page →

A tagged disjoint union represents $X \mapsto S e t (A, X) \times S e t (B, X)$

Example

For sets $A$ and $B$ , put

$A ⊔ B = (A \times {0}) \cup (B \times {1})$

and define $i_{A} (a) = (a, 0)$ and $i_{B} (b) = (b, 1)$ . The covariant functor

$G (X) = S e t (A, X) \times S e t (B, X)$

is represented by $A ⊔ B$ . The representing isomorphism sends $q : A ⊔ B \to X$ to $(q \circ i_{A}, q \circ i_{B})$ .

Facts & Assumptions

Given: Sets $A, B$ , the category $S e t$ , and an arbitrary set $X$ .

[F1]

A covariant set-valued functor is represented by $R$ when it is naturally isomorphic to $S e t (R, -)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[F2]

Sets and functions form a category with ordinary composition (Sets and functions form the large locally small category $S e t$ ).

[F3]

Cartesian products contain exactly the ordered pairs with entries in the two factors, and membership in a binary union is membership in at least one of its two members (The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ , The union $⋃ x$ of a set, and the binary union $a \cup b : = ⋃ {a, b}$ , $⋃ \emptyset = \emptyset$ , $⋃ {a} = a$ , $⋃ {a, b} = a \cup b$ , $⋂ {a} = a$ , and $⋂ {a, b} = a \cap b$ ).

[F4]

Ordered pairs satisfy $(a, s) = (b, t)$ if and only if $a = b$ and $s = t$ ; the natural numbers $0 = \emptyset$ and $1 = {0}$ are distinct, so the two tagged parts are disjoint (The Kuratowski ordered pair $(a, b) : = {{a}, {a, b}}$ , $(a, b) = (c, d)$ if and only if $a = c$ and $b = d$ , The natural numbers $N$ (von Neumann)).

[F5]

Two functions with the same domain and codomain are equal exactly when their values agree everywhere (Functions $f$ and $g$ are equal if and only if $dom f = dom g$ and $f (x) = g (x)$ for every $x$ in that common domain).

Verification

technique · constructive

1.1

Define $Φ_{X} (q) = (q \circ i_{A}, q \circ i_{B})$ for $q : A ⊔ B \to X$ .

F2construct

1.2

For $(g, h) \in G (X)$ define $[g, h] : A ⊔ B \to X$ by $[g, h] (a, 0) = g (a)$ and $[g, h] (b, 1) = h (b)$ . Every element has one of these forms by [F3], and the forms cannot overlap by [F4], so this is a function.

F3F4construct

2.1

Restricting $[g, h]$ along $i_{A}$ and $i_{B}$ gives $g$ and $h$ , so $Φ_{X} ([g, h]) = (g, h)$ .

step 1.1step 1.2

2.2

Every $z \in A ⊔ B$ is in exactly one tagged part; there $[q \circ i_{A}, q \circ i_{B}] (z) = q (z)$ . Thus $[q \circ i_{A}, q \circ i_{B}] = q$ by [F5].

step 1.1step 1.2F3F4F5

2.3

If $k : X \to Y$ , then $Φ_{Y} (k \circ q) = (k \circ q \circ i_{A}, k \circ q \circ i_{B})$ , obtained by applying $G (k)$ to $Φ_{X} (q)$ . Hence $Φ$ is natural.

step 1.1F2

3.1

Steps 2.1--2.3 give a natural isomorphism $S e t (A ⊔ B, -) ≅ G$ , so [F1] proves the claim, including $A = \emptyset$ or $B = \emptyset$ .

step 2.1step 2.2step 2.3F1discharge-construct∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The function set $B^{A}$ represents $X \mapsto S e t (X \times A, B)$

Example

For sets $A$ and $B$ , let $B^{A}$ be the set of functions $A \to B$ . The presheaf

$H (X) = S e t (X \times A, B)$

is represented by $B^{A}$ . Its representing natural isomorphism is currying:

$S e t (X, B^{A}) ⟶ S e t (X \times A, B), g ⟼ ((x, a) \mapsto g (x) (a)) .$

Facts & Assumptions

Given: Sets $A, B$ , the category $S e t$ , and an arbitrary set $X$ .

[F1]

A presheaf is represented by $R$ when it is naturally isomorphic to $S e t (-, R)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[F2]

Sets and functions form a category under ordinary composition (Sets and functions form the large locally small category $S e t$ ).

[F3]

The function set $B^{A}$ consists of all functions from $A$ to $B$ (The set $B^{A}$ of all functions $A \to B$ ).

[F4]

The product $X \times A$ consists of the pairs $(x, a)$ with $x \in X$ and $a \in A$ (The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ ).

[F5]

A function assigns exactly one value to each domain element, and two functions with the same domain and codomain are equal exactly when their values agree everywhere (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain, Functions $f$ and $g$ are equal if and only if $dom f = dom g$ and $f (x) = g (x)$ for every $x$ in that common domain).

Verification

technique · constructive

1.1

For $g : X \to B^{A}$ , define $Φ_{X} (g) : X \times A \to B$ by $Φ_{X} (g) (x, a) = g (x) (a)$ .

F3F4construct

1.2

For $f : X \times A \to B$ , define $Ψ_{X} (f) : X \to B^{A}$ by $Ψ_{X} (f) (x) (a) = f (x, a)$ .

F3F4construct

2.1

For all $(x, a)$ , $Φ_{X} Ψ_{X} (f) (x, a) = f (x, a)$ , and for all $x, a$ , $Ψ_{X} Φ_{X} (g) (x) (a) = g (x) (a)$ ; [F5] makes $Φ_{X}$ and $Ψ_{X}$ inverse functions.

step 1.1step 1.2F3F4F5

2.2

If $k : Y \to X$ , then $Φ_{Y} (g \circ k) (y, a) = g (k (y)) (a) = Φ_{X} (g) (k (y), a)$ , which is precomposition of $Φ_{X} (g)$ by $k \times 1_{A}$ . Thus $Φ$ is natural in $X$ .

step 1.1F2F4

3.1

By steps 2.1 and 2.2, $Φ$ is a natural isomorphism $S e t (-, B^{A}) ≅ H$ ; [F1] gives the representation, also when $A$ , $B$ , or $X$ is empty.

step 2.1step 2.2F1discharge-construct∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The free word monoid on $X$ represents $M \mapsto S e t (X, U (M))$

Example

Let $X^{*}$ be the set of finite words in the alphabet $X$ , including the empty word $ε$ . Concatenation and $ε$ make $X^{*}$ a monoid, and the one-letter map $j : X \to X^{*}$ makes it the free word monoid on $X$ .

If $M o n$ denotes the locally small category of monoids and unital monoid homomorphisms and $U : M o n \to S e t$ forgets the monoid structure, then $X^{*}$ represents

$M ⟼ S e t (X, U (M)) .$

The representing bijection sends $ϕ : X^{*} \to M$ to $U (ϕ) \circ j$ .

Facts & Assumptions

Given: A set $X$ ; finite words have a length, the empty word has length zero, every nonempty word is uniquely a shorter word followed by one letter, and concatenation joins the two finite lists.

[F1]

A monoid has an associative product and a two-sided identity (Semigroup and monoid).

[F2]

A monoid homomorphism preserves products and the identity; identity maps and composites are monoid homomorphisms (Monoid homomorphism and group homomorphism).

[F3]

A category has associative composition and identity morphisms; it is locally small when each hom-collection is a set (Category, object, morphism, domain, codomain, identity, composition, and hom-collection, Small, locally small, and large categories).

[F4]

A functor preserves identities and composition, and the functions between two fixed sets form a set (Covariant functor, identity functor, composite functor, and contravariant functor, The set $B^{A}$ of all functions $A \to B$ ).

[F5]

The finite product in a monoid has empty value $e$ and appending one factor multiplies it on the right; its splitting law identifies the product along a concatenated list with the product of the first list followed by the product of the second (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).

[F6]

A property of all finite lengths follows from the zero case and the step obtained by appending one letter (The principle of mathematical induction).

[F7]

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

Verification

technique · constructive

1.1

Concatenation is associative because joining three finite lists gives the same word in either bracketing, and the empty word is a two-sided identity; hence [F1] makes $X^{*}$ a monoid.

givenF1

1.2

Monoids and their unital homomorphisms form a category by [F2] and the function laws. Its hom-collection from $M$ to $N$ is a subclass of the set of functions $U (M) \to U (N)$ , so it is a set and the category is locally small by [F3] and [F4].

F2F3F4

1.3

Given $f : X \to U (M)$ and a word $w = x_{0} \dots x_{n - 1}$ , define $\hat{f} (w) = \prod_{i < n} f (x_{i})$ . In particular, $\hat{f} (ε) = e_{M}$ and $\hat{f} (j (x)) = f (x)$ .

F5construct

2.1

Sending a monoid to its underlying set and a homomorphism to its underlying function preserves identities and composition, so it defines the functor $U$ . Postcomposition therefore makes $M \mapsto S e t (X, U (M))$ a functor.

step 1.2F2F4

2.2

The splitting law in [F5] gives $\hat{f} (w v) = \hat{f} (w) \hat{f} (v)$ for all words $w, v$ ; together with the empty-word equation, this makes $\hat{f} : X^{*} \to M$ a unital monoid homomorphism extending $f$ .

step 1.3F2F5

3.1

If $q : X^{*} \to M$ is a unital monoid homomorphism with $q j = f$ , then $q (ε) = e_{M} = \hat{f} (ε)$ . If $q (w) = \hat{f} (w)$ , then $q (w j (x)) = q (w) f (x) = \hat{f} (w j (x))$ ; induction [F6] proves $q = \hat{f}$ .

step 1.3step 2.2F2F6

4.1

Thus restriction along $j$ and $f \mapsto \hat{f}$ are inverse bijections $M o n (X^{*}, M) ≅ S e t (X, U (M))$ . If $r : M \to N$ is a monoid homomorphism, then both $r \circ \hat{f}$ and $\hat{U (r) \circ f}$ extend $U (r) \circ f$ , so uniqueness in step 3.1 makes them equal; the bijection is natural in $M$ .

step 2.2step 3.1F2

5.1

By [F7], $X^{*}$ is the claimed representing object. The construction also covers $X = \emptyset$ : then $X^{*} = {ε}$ , and there is exactly one unital homomorphism from it to every monoid.

step 2.1step 4.1F7discharge-construct∎

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The free group on $X$ represents $G \mapsto S e t (X, U (G))$

Example

Let $(F (X), i)$ be a free group on a set $X$ , and let $U : G r p \to S e t$ be the underlying-set functor. Then $F (X)$ represents the functor

$G ⟼ S e t (X, U (G)) .$

The representing natural isomorphism is

$G r p (F (X), G) ⟶ S e t (X, U (G)), ϕ ⟼ U (ϕ) \circ i .$

For a singleton $X = {x}$ , the reduced-word model $F (X)$ is infinite cyclic, generated by the one-letter word $x$ .

Facts & Assumptions

Given: A set $X$ , a free group $(F (X), i)$ , and a group $G$ .

[F1]

The free-group universal property gives, for every function $f : X \to U (G)$ , a unique group homomorphism $\hat{f} : F (X) \to G$ with $\hat{f} \circ i = f$ (Free group on a set of generators).

[L1]

Reduced words form a free group, with generators the one-letter positive words; reduced words are unique normal forms (Reduced words form the free group on an alphabet).

[L2]

Any two free groups on $X$ have a unique isomorphism carrying one generator map to the other (Free groups on the same set are uniquely isomorphic compatibly with their generators).

[F2]

Groups and group homomorphisms form the large locally small category $G r p$ (Groups and group homomorphisms form the large locally small category $G r p$ ).

[F3]

A group is cyclic when it is generated by one element, meaning every element lies in the subgroup generated by that element (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

[F4]

A covariant set-valued functor represented by $R$ is naturally isomorphic to the hom-functor $C (R, -)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

Verification

technique · direct

1.1

By [F1], restriction along $i$ is a bijection $G r p (F (X), G) \to S e t (X, U (G))$ , with inverse $f \mapsto \hat{f}$ .

1.2

Now let $X = {x}$ . By [L1], every reduced word is either empty, a string of $n \geq 1$ copies of $x$ , or a string of $n \geq 1$ copies of $x^{- 1}$ : a reduced word containing both signs would have an adjacent sign change and hence a cancellable pair. Thus every element is an integer power of $x$ , so [F3] makes $F (X)$ cyclic.

L1F3

2.1

If $r : G \to H$ is a group homomorphism, then $r \circ \hat{f}$ and $\hat{U (r) \circ f}$ are homomorphisms $F (X) \to H$ with the same restriction to $X$ ; uniqueness in [F1] makes them equal. Thus the bijections of step 1.1 are natural in $G$ .

step 1.1F1F2

3.1

Steps 1.1 and 2.1, together with [F4], show that $F (X)$ represents the stated functor. By [L2], changing the chosen free-group model changes this representation by the unique generator-compatible isomorphism.

step 1.1step 2.1L2F4

4.1

The positive words $x, x x, x x x, \dots$ have different finite lengths and are distinct reduced normal forms by [L1], so $F (X)$ has infinitely many elements. Hence the singleton free group is infinite cyclic.

step 1.2L1∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-13Open item page →

$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∎

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-08-13Open item page →

The one-point space represents the underlying-set functor on $T o p$

Example

Let $1 = {*}$ carry its unique topology ${\emptyset, 1}$ . The one-point space represents the underlying-set functor $U : T o p \to S e t$ through the natural bijection

$T o p (1, X) \overset{≅}{\to} U (X), f ⟼ f (*) .$

Facts & Assumptions

Given: The singleton space $1 = {*}$ and an arbitrary topological space $X$ .

[F1]

A topology contains the empty set and the whole underlying set (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[F2]

A function is continuous when it is continuous at every point, equivalently when inverse images of open sets are open (Continuity of a map of topological spaces at a point and globally, For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ , clause (b)).

[F3]

Topological spaces and continuous maps form the large locally small category $T o p$ (Topological spaces and continuous maps form the large locally small category $T o p$ ).

[F4]

A covariant set-valued functor is represented by $R$ when it is naturally isomorphic to the hom-functor $T o p (R, -)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[F5]

Verification

technique · constructive

1.1

For every point $x \in X$ , define $f_{x} : 1 \to X$ by $f_{x} (*) = x$ . For every open $V \subseteq X$ , the inverse image $f_{x}^{- 1} [V]$ is $1$ if $x \in V$ and $\emptyset$ otherwise; [F1] and [F2] make $f_{x}$ continuous.

F1F2construct

2.1

Every function $f : 1 \to X$ equals $f_{f (*)}$ by [F5], and $f_{x} (*) = x$ . Thus $f \mapsto f (*)$ and $x \mapsto f_{x}$ are inverse bijections.

step 1.1F5

3.1

If $g : X \to Y$ is continuous, then $(g \circ f) (*) = g (f (*))$ , so the bijections in step 2.1 commute with the hom-functor action and the underlying function $U (g)$ . They are natural in $X$ , and $U$ is a functor because [F3] uses ordinary function composition.

step 2.1F3

4.1

By [F4], the singleton space represents $U$ . When $X = \emptyset$ , both $T o p (1, X)$ and $U (X)$ are empty, so the same bijection includes that boundary case.

step 3.1F4discharge-construct∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-13Open item page →

A representable presheaf on a poset is the indicator of a principal down-set

Example

Let $(P, \leq)$ be a partially ordered set, viewed as a category, and fix $p \in P$ . The representable presheaf $P (-, p)$ has the object values

$P (q, p) = {\begin{cases} {*}, & q \leq p, \\ \emptyset, & q ≰ p . \end{cases}$

Consequently its nonempty support is the principal down-set $↓ p = {q \in P : q \leq p}$ .

Facts & Assumptions

Given: A partially ordered set $(P, \leq)$ and an element $p \in P$ .

[F1]

Every partial order is a preorder, and a preorder is reflexive and transitive (Preorder and monotone map).

[L1]

A preorder determines a category with at most one morphism between any two objects, and functors between such categories are exactly the monotone maps (A preorder is a category with at most one morphism between any two objects, and its functors are exactly monotone maps). In that category the morphism $q \to r$ is present exactly when $q \leq r$ , which is how this example reads every hom-set below.

[F2]

The presheaf represented by $p$ is the contravariant hom-functor $P (-, p)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[F3]

There is exactly one function with empty domain, and a function is determined by its values (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain).

Verification

technique · direct

1.1

By [L1], the hom-set $P (q, p)$ has one element when $q \leq p$ and no elements when $q ≰ p$ , proving the displayed object table.

2.1

If $r \leq q$ , presheaf restriction along the unique arrow $r \to q$ maps the unique member of $P (q, p)$ to the composite $r \to q \to p$ , the unique member of $P (r, p)$ . Whenever the source is empty, there is instead the unique empty function of [F3]. These are all possible restriction maps.

step 1.1F1L1F2F3

2.2

The object value is nonempty exactly when $q \leq p$ , so its support is precisely $↓ p$ . Reflexivity gives $p \in ↓ p$ , and transitivity makes the support downward closed.

step 1.1F1

3.1

Steps 1.1 and 2.1 compute the entire representable presheaf, including every empty value and restriction map, and step 2.2 identifies its support.

step 1.1step 2.1step 2.2∎

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The functor $D (X) = X ⊔ X$ on $S e t$ is not covariantly representable

Statement refuted

The endofunctor $D : S e t \to S e t$ defined by

$D (X) = (X \times {0}) \cup (X \times {1}), D (f) (x, s) = (f (x), s),$

is covariantly representable.

Facts & Assumptions

Given: The category $S e t$ and the tagged doubling assignment $D$ in the statement.

[F1]

Sets and functions form the locally small category $S e t$ , and a functor must preserve identities and composition (Sets and functions form the large locally small category $S e t$ , Covariant functor, identity functor, composite functor, and contravariant functor).

[F2]

The Cartesian product consists of its ordered pairs, and binary union contains exactly the elements in either of its two members (The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ , The union $⋃ x$ of a set, and the binary union $a \cup b : = ⋃ {a, b}$ , $⋃ \emptyset = \emptyset$ , $⋃ {a} = a$ , $⋃ {a, b} = a \cup b$ , $⋂ {a} = a$ , and $⋂ {a, b} = a \cap b$ ).

[F3]

Ordered pairs satisfy $(x, s) = (y, t)$ if and only if $x = y$ and $s = t$ ; the naturals $0$ and $1$ are distinct (The Kuratowski ordered pair $(a, b) : = {{a}, {a, b}}$ , $(a, b) = (c, d)$ if and only if $a = c$ and $b = d$ , The natural numbers $N$ (von Neumann)).

[F4]

The functions $R \to 1$ form the set $1^{R}$ , and a function assigns exactly one value to each element of its domain. Hence for every set $R$ , including $R = \emptyset$ , there is exactly one function $R \to 1$ (The set $B^{A}$ of all functions $A \to B$ , A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain).

[F5]

Representability by $R$ would give bijections $S e t (R, X) ≅ D (X)$ for every set $X$ , and a bijection must be both injective and surjective (Presheaves, covariantly and contravariantly representable functors, and representations, Injection, surjection, bijection).

Counterexample

technique · contradiction

1.1

The formula for $D (f)$ is a function by [F2] and [F3]. It preserves the tag and applies $f$ to the first coordinate, so $D (1_{X}) = 1_{D (X)}$ and $D (g \circ f) = D (g) \circ D (f)$ ; by [F1], $D$ is an endofunctor.

F1F2F3

1.2

By [F4], $S e t (R, 1)$ is a singleton for every $R$ , including $R = \emptyset$ .

1.3

By [F2] and [F3], $D (1) = {(*, 0), (*, 1)}$ and its two displayed elements are distinct, so it has exactly two elements.

F2F3

2.1

Suppose $D$ were represented by a set $R$ . The component at the singleton $1 = {*}$ would be a bijection $S e t (R, 1) ≅ D (1)$ by [F5].

step 1.1F5assume-contra

3.1

No function from a singleton onto a two-element set is surjective, contradicting the bijection in step 2.1.

step 2.1step 1.2step 1.3F5

4.1

Therefore $D$ is a well-defined functor but is not covariantly representable.

step 1.1step 3.1discharge-contradiction∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-13Open item page →

Two singleton sets give canonically isomorphic representations of the identity functor on $S e t$

Example

For distinct sets $s_{0}$ and $s_{1}$ , the singleton sets $S_{0} = {s_{0}}$ and $S_{1} = {s_{1}}$ both represent the identity functor on $S e t$ . Their universal elements are $s_{0} \in S_{0}$ and $s_{1} \in S_{1}$ , and the unique function

$i : S_{0} ⟶ S_{1}, i (s_{0}) = s_{1},$

is the canonical isomorphism of these representations.

Facts & Assumptions

Given: The category $S e t$ , the singletons $S_{0}, S_{1}$ , and its identity functor.

[F1]

Sets and functions form a category under ordinary identity functions and composition (Sets and functions form the large locally small category $S e t$ ).

[F2]

A covariant representation of $F$ is a natural isomorphism $S e t (R, -) ≅ F$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[L1]

Two covariant universal elements for the same functor have a unique isomorphism $i$ satisfying $F (i) (u) = u^{'}$ (Representing objects are unique up to a unique isomorphism compatible with their universal elements).

[F3]

Verification

technique · constructive

1.1

For $k \in {0, 1}$ and every set $X$ , define $E_{X}^{k} : S e t (S_{k}, X) \to X$ by $E_{X}^{k} (f) = f (s_{k})$ . Its inverse sends $x \in X$ to the function $S_{k} \to X$ with value $x$ at $s_{k}$ .

F3construct

2.1

The two formulas in step 1.1 are inverse by [F3]. If $g : X \to Y$ , then $E_{Y}^{k} (g \circ f) = g (E_{X}^{k} (f))$ , so the bijections are natural by [F1].

step 1.1F1F3

3.1

By [F2], both $S_{0}$ and $S_{1}$ represent the identity functor; their universal elements are the values of the identity functions, namely $s_{0}$ and $s_{1}$ . The conclusion remains valid at $X = \emptyset$ , where both sides of each component bijection are empty.

step 1.1step 2.1F2

4.1

The function $i : S_{0} \to S_{1}$ with $i (s_{0}) = s_{1}$ carries the first universal element to the second. By [L1], it is the unique compatible isomorphism; explicitly its inverse is the unique map $S_{1} \to S_{0}$ .

step 3.1L1F3

5.1

Thus the word canonical refers to compatibility with the chosen universal points, not merely to the fact that the underlying singleton sets happen to be isomorphic.

step 4.1discharge-construct∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-13Open item page →

The Yoneda embedding of the walking-arrow category computed objectwise

Example

Let $W$ be the walking-arrow category $0 \overset{u}{\to} 1$ . Its only morphisms are $1_{0}, u, 1_{1}$ . The Yoneda embedding $y : W \to [W^{o p}, S e t]$ has the table

$\begin{array}{cccc} 0 & 1 & u^{o p} : 1 \to 0 \\ y (0) = W (-, 0) & {1_{0}} & \emptyset & \emptyset \to {1_{0}} \\ y (1) = W (-, 1) & {u} & {1_{1}} & 1_{1} \mapsto u \end{array}$

and $y (u) : y (0) \Rightarrow y (1)$ has components $1_{0} \mapsto u$ at $0$ and the empty function at $1$ .

Facts & Assumptions

Given: The category $W$ with the two objects and three morphisms displayed above.

[F1]

A category has identity morphisms, associative composition, and the two identity laws (Category, object, morphism, domain, codomain, identity, composition, and hom-collection).

[F2]

For a small category, the Yoneda functor sends $a$ to $W (-, a)$ and $h : a \to b$ to postcomposition $W (-, h)$ (The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding).

[L1]

The Yoneda functor is fully faithful: postcomposition gives a bijection $W (a, b) ≅ Nat (y (a), y (b))$ (The Yoneda functor is fully faithful, and it is a full embedding when its object map is injective).

[F3]

A function gives one value for each domain element; no function has a nonempty domain and empty codomain, while there is exactly one empty function (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain).

Verification

technique · direct

1.1

The hom-sets are $W (0, 0) = {1_{0}}$ , $W (0, 1) = {u}$ , $W (1, 1) = {1_{1}}$ , and $W (1, 0) = \emptyset$ . These are exactly the four object values in the displayed table.

given

2.1

A presheaf represented by $a$ acts on $u^{o p} : 1 \to 0$ by precomposition with $u$ . For $a = 0$ this is the empty function $\emptyset \to {1_{0}}$ ; for $a = 1$ it sends $1_{1}$ to $1_{1} \circ u = u$ by [F1].

step 1.1F1F2F3

2.2

By [F2], $y (u)$ is postcomposition with $u$ . At $0$ it sends $1_{0}$ to $u \circ 1_{0} = u$ , and at $1$ it is the unique empty function. This proves the asserted component table, including the empty hom-set.

step 1.1F1F2F3

3.1

There is one natural transformation $y (0) \Rightarrow y (0)$ and one $y (0) \Rightarrow y (1)$ , namely the identity and $y (u)$ . There is no transformation $y (1) \Rightarrow y (0)$ because its component at $1$ would be a function ${1_{1}} \to \emptyset$ , forbidden by [F3].

step 1.1step 2.1step 2.2F3

4.1

A transformation $y (1) \Rightarrow y (1)$ has forced singleton-to-singleton components, and the naturality square commutes by [F1], so it is the identity. Hence the four natural-transformation sets have the same empty-or-singleton table as the four hom-sets, exactly as [L1] asserts.

step 1.1step 2.1step 3.1F1L1

5.1

Composition in the image has only the identity composites and $y (u)$ composed with an identity; by [F1] and step 2.2 these reproduce the composition of $1_{0}, u, 1_{1}$ in $W$ .

step 2.2step 4.1F1∎

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-13Open item page →

For a monoid action, Yoneda says that an equivariant map from the regular action is determined by the identity element

Example

Let $M$ be a monoid with identity $e$ , viewed as the one-object category $B M$ . A functor $F : B M \to S e t$ is a set $X = F (*)$ with a left $M$ -action. The representable $B M (*, -)$ is the left regular action of $M$ on itself, and Yoneda becomes the bijection

${ϕ : M \to X ∣ ϕ is M -equivariant} \overset{≅}{\to} X, ϕ ⟼ ϕ (e),$

with inverse $x \mapsto (m \mapsto m \cdot x)$ .

Facts & Assumptions

Given: A monoid $(M, \cdot, e)$ , its one-object category $B M$ , and a functor $F : B M \to S e t$ .

[F1]

A monoid has associative multiplication and a two-sided identity (Semigroup and monoid).

[L1]

Every monoid is a one-object category (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible). This example fixes the resulting data explicitly: $B M (*, *) = M$ , and composition is taken to be $n \circ m = n m$ , the convention that makes the represented functor a left action.

[F2]

Sets and functions form the category $S e t$ (Sets and functions form the large locally small category $S e t$ ).

[L2]

Evaluation at the identity is a bijection $Nat (B M (*, -), F) \to F (*)$ whose inverse sends $x$ to the natural transformation with component $m \mapsto F (m) (x)$ (Evaluation at the identity gives $Nat (C (a, -), F) ≅ F (a)$ and proves that the natural-transformation collection is a set), and it is natural in the represented object and in the target functor (The Yoneda bijection $Nat (C (a, -), F) ≅ F (a)$ is natural in both $a$ and $F$ ).

[F3]

A natural transformation has components commuting with the action of every source morphism (Natural transformation and its components).

Verification

technique · constructive

1.1

Put $m \cdot x = F (m) (x)$ . Functoriality and [L1] give $e \cdot x = x$ and $(n m) \cdot x = n \cdot (m \cdot x)$ , so this is a left action.

givenL1F1F2

1.2

The covariant representable $B M (*, -)$ has value $M$ and sends $n$ to postcomposition $m \mapsto n \circ m = n m$ , so it is the left regular action.

2.1

A natural transformation $B M (*, -) \Rightarrow F$ is a function $ϕ : M \to X$ satisfying $ϕ (n m) = n \cdot ϕ (m)$ for all $m, n$ , exactly equivariance for the two left actions.

step 1.1step 1.2F3

3.1

If $ϕ$ is equivariant, then $ϕ (m) = ϕ (m e) = m \cdot ϕ (e)$ . Conversely, for $x \in X$ , the function $ϕ_{x} (m) = m \cdot x$ satisfies $ϕ_{x} (n m) = (n m) \cdot x = n \cdot ϕ_{x} (m)$ by step 1.1 and has $ϕ_{x} (e) = x$ .

step 1.1step 2.1F1construct

4.1

Step 3.1 proves directly that evaluation at $e$ and $x \mapsto ϕ_{x}$ are inverse. These are precisely the formulas in [L2], whose target-functor naturality says that the bijection commutes with every equivariant map of $M$ -sets.

step 3.1L2discharge-construct∎

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-13Open item page →

The Yoneda lemma requires its category to be small

Statement

False claim: the Yoneda lemma can be stated and proved only when its category is small.

Facts & Assumptions

Given: The false claim above and the category $S e t$ .

[L1]

For every locally small category $C$ , object $a$ , and functor $F : C \to S e t$ , evaluation at the identity is a bijection $Nat (C (a, -), F) ≅ F (a)$ , with an explicit inverse; smallness is not a hypothesis (Evaluation at the identity gives $Nat (C (a, -), F) ≅ F (a)$ and proves that the natural-transformation collection is a set).

[L2]

The same bijection is natural in both $a$ and $F$ for every locally small $C$ , without forming a functor category on a large source (The Yoneda bijection $Nat (C (a, -), F) ≅ F (a)$ is natural in both $a$ and $F$ ).

[L3]

The category $S e t$ is large and locally small (Sets and functions form the large locally small category $S e t$ ).

[F1]

A category is small when its objects and morphisms form sets, locally small when each hom-collection is a set, and large when it is not small (Small, locally small, and large categories).

Refutation

technique · direct

1.1

By [L3] and [F1], $S e t$ is a locally small category that is not small.

L3F1

2.1

Apply [L1] and [L2] to $C = S e t$ , any set $a$ , and any functor $F : S e t \to S e t$ . The Yoneda bijection exists and has both naturalities despite the category being large.

step 1.1L1L2

3.1

Thus local smallness, which makes each hom-collection a set, suffices for the pointwise Yoneda lemma; the large locally small category $S e t$ refutes the asserted need for smallness.

step 1.1step 2.1∎

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-13Open item page →

Non-isomorphic objects can have naturally isomorphic representable presheaves

Statement

False claim: in a locally small category, two non-isomorphic objects can have naturally isomorphic representable presheaves $C (-, a) ≅ C (-, b)$ .

Facts & Assumptions

Given: A locally small category $C$ and the false claim above.

[L1]

Objects $a$ and $b$ are isomorphic if and only if the representable presheaves $C (-, a)$ and $C (-, b)$ are naturally isomorphic (Objects $a$ and $b$ are isomorphic exactly when $C (-, a)$ and $C (-, b)$ are naturally isomorphic).

[L2]

The Yoneda hom-map $C (a, b) \to Nat (C (-, a), C (-, b))$ is a bijection and respects identities and composition (The Yoneda functor is fully faithful, and it is a full embedding when its object map is injective).

Refutation

technique · contradiction

1.1

Suppose there were non-isomorphic objects $a, b$ and a natural isomorphism $α : C (-, a) \overset{≅}{\Rightarrow} C (-, b)$ .

assume-contra

2.1

By [L2], $α$ and its natural inverse lift uniquely to morphisms $f : a \to b$ and $g : b \to a$ . Because the Yoneda map respects identities and composition and is injective, the two equations $α^{- 1} α = 1$ and $α α^{- 1} = 1$ imply $g f = 1_{a}$ and $f g = 1_{b}$ .

step 1.1L2

3.1

Thus $a$ and $b$ are isomorphic, also the reverse implication of [L1], contradicting the choice in step 1.1.

step 1.1step 2.1L1

4.1

No such pair of non-isomorphic objects exists, so the claim is false.

step 3.1discharge-contradiction∎

Universal Properties, Representables and the Yoneda Lemma — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A Cartesian product represents X↦Set(X,A)×Set(X,B)X↦Set(X,A)×Set(X,B)

Example

Facts & Assumptions

Verification

A tagged disjoint union represents X↦Set(A,X)×Set(B,X)X↦Set(A,X)×Set(B,X)

Example

Facts & Assumptions

Verification

The function set BABA represents X↦Set(X×A,B)X↦Set(X×A,B)

Example

Facts & Assumptions

Verification

The free word monoid on XX represents M↦Set(X,U(M))M↦Set(X,U(M))

Example

Facts & Assumptions

Verification

The free group on XX represents G↦Set(X,U(G))G↦Set(X,U(G))

Example

Facts & Assumptions

Verification

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

Example

Facts & Assumptions

Verification

The one-point space represents the underlying-set functor on TopTop

Example

Facts & Assumptions

Verification

A representable presheaf on a poset is the indicator of a principal down-set

Example

Facts & Assumptions

Verification

The functor D(X)=X⊔XD(X)=X⊔X on SetSet is not covariantly representable

Statement refuted

Facts & Assumptions

Counterexample

Two singleton sets give canonically isomorphic representations of the identity functor on SetSet

Example

Facts & Assumptions

Verification

The Yoneda embedding of the walking-arrow category computed objectwise

Example

Facts & Assumptions

Verification

For a monoid action, Yoneda says that an equivariant map from the regular action is determined by the identity element

Example

Facts & Assumptions

Verification

The Yoneda lemma requires its category to be small

Statement

Facts & Assumptions

Refutation

Non-isomorphic objects can have naturally isomorphic representable presheaves

Statement

Facts & Assumptions

Refutation

Sources

A Cartesian product represents $X \mapsto S e t (X, A) \times S e t (X, B)$

A tagged disjoint union represents $X \mapsto S e t (A, X) \times S e t (B, X)$

The function set $B^{A}$ represents $X \mapsto S e t (X \times A, B)$

The free word monoid on $X$ represents $M \mapsto S e t (X, U (M))$

The free group on $X$ represents $G \mapsto S e t (X, U (G))$

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

The one-point space represents the underlying-set functor on $T o p$

The functor $D (X) = X ⊔ X$ on $S e t$ is not covariantly representable

Two singleton sets give canonically isomorphic representations of the identity functor on $S e t$