TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

A representation is equivalently a universal element with a unique factorisation property

Statement

Let $C$ be locally small.

A pair $(R, u)$ with $u \in F (R)$ is universal for a functor $F : C \to S e t$ if and only if, for every object $c$ and every $x \in F (c)$ , there is a unique morphism $f : R \to c$ such that $F (f) (u) = x$ .
A pair $(R, u)$ with $u \in P (R)$ is universal for a presheaf $P : C^{o p} \to S e t$ if and only if, for every object $c$ and every $x \in P (c)$ , there is a unique morphism $f : c \to R$ such that $P (f) (u) = x$ .

Every representation $θ$ determines its universal element by $u = θ_{R} (1_{R})$ , and the universal element recovers $θ$ by the formulas in the statement. These correspondences are the Yoneda correspondences and are natural in the representing object and the set-valued functor.

Facts & Assumptions

Given: A locally small category $C$ , an object $R$ , and either a functor $F : C \to S e t$ with $u \in F (R)$ or a presheaf $P$ with $u \in P (R)$ .

[L1]

Evaluation at $1_{R}$ is a bijection $Nat (C (R, -), F) ≅ F (R)$ whose inverse sends $u$ to $f \mapsto F (f) (u)$ (Evaluation at the identity gives $Nat (C (a, -), F) ≅ F (a)$ and proves that the natural-transformation collection is a set).

[L2]

This covariant evaluation bijection is natural in both the representing object and the target functor (The Yoneda bijection $Nat (C (a, -), F) ≅ F (a)$ is natural in both $a$ and $F$ ).

[L3]

Dually, evaluation gives $Nat (C (-, R), P) ≅ P (R)$ naturally in $R$ and $P$ , with inverse $u \mapsto (f \mapsto P (f) (u))$ (For a presheaf $P$ , $Nat (C (-, a), P) ≅ P (a)$ naturally in $a$ and $P$ ).

[F1]

A universal element is an element whose Yoneda-associated natural transformation is a natural isomorphism (Universal elements of covariant functors and presheaves).

Proof

technique · direct

1.1

By [L1], any natural transformation $θ : C (R, -) \Rightarrow F$ satisfies $θ_{c} (f) = F (f) (θ_{R} (1_{R}))$ ; thus a representation determines $u = θ_{R} (1_{R})$ and is exactly the family $θ^{u}$ .

L1F1

1.2

By [L3], the same argument for a presheaf identifies its representing transformation with $f \mapsto P (f) (u)$ ; componentwise bijectivity is exactly the stated existence and uniqueness of $f : c \to R$ .

L3F1

2.1

The family $θ^{u}$ is a natural isomorphism if and only if each function $θ_{c}^{u} : f \mapsto F (f) (u)$ is bijective, which is equivalent to the existence and uniqueness of $f : R \to c$ for every $x \in F (c)$ .

step 1.1F1

3.1

The naturality assertions for the two correspondences are [L2] and [L3], so steps 1.1--2.1 prove both equivalences and the final assertion.

step 1.1step 2.1step 1.2L2L3∎

Depends on

Used by

Cited to discharge well-definedness by Universal elements of covariant functors and presheaves.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 21 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Emily Riehl, Category Theory in Context, Definition 2.3.3 (standard reference, not scraped)
Tom Leinster, Basic Category Theory, Corollaries 4.3.2 and 4.3.3 (standard reference, not scraped)