TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

The end of the function-set functor on a representable is evaluation

Statement

Let $C$ be small (Small, locally small, and large categories) and let $a$ be an object of $C$ . Write $S e t (X, Y)$ for the hom-set of $S e t$ , which is the set $Y^{X}$ of functions $X \to Y$ (Sets and functions form the large locally small category $S e t$ , The set $B^{A}$ of all functions $A \to B$ ).

Covariant case. For $F : C \to S e t$ , let $H (c_{1}, c_{2}) : = S e t (C (a, c_{1}), F c_{2})$ , a functor $C^{o p} \times C \to S e t$ (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category). Then

$\int_{c} S e t (C (a, c), F c) ≅ F (a) .$

Contravariant case. For a presheaf $P : C^{o p} \to S e t$ (Opposite category $C^{o p}$ ), let $H^{'} (c_{1}, c_{2}) : = S e t (C (c_{2}, a), P c_{1})$ , again a functor $C^{o p} \times C \to S e t$ . Then

$\int_{c} S e t (C (c, a), P c) ≅ P (a) .$

So the end of the function-set functor on a representable is evaluation (The end and the coend of a functor $C^{o p} \times C \to D$ ), the isomorphism sending a family to its value at the identity of $a$ .

Facts & Assumptions

Given: A small category $C$ , an object $a$ of $C$ , a functor $F : C \to S e t$ and a presheaf $P : C^{o p} \to S e t$ .

[F5]

A category is small when both $Ob (C)$ and $Mor (C)$ are sets; a small category is locally small (Small, locally small, and large categories).

[F4]

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

[F2]

The functions $A \to B$ form the set $B^{A}$ , and Thus $f \in B^{A}$ holds if and only if $f : A \to B$ . (The set $B^{A}$ of all functions $A \to B$ ).

[F1]

The covariant hom-assignment $C (a, -)$ sends $b$ to $C (a, b)$ and $u : b \to c$ to $u_{*} : C (a, b) ⟶ C (a, c), f ⟼ u \circ f$ , while the contravariant hom-assignment $C (-, a)$ sends $u$ to precomposition (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category).

[F6]

The opposite category has the same objects and reverses every morphism: $C^{o p} (A, B) = C (B, A)$ (Opposite category $C^{o p}$ ).

[F7]

A wedge from $d$ to $T$ is a family $ω_{c} : d \to T (c, c)$ with $T (1_{c}, f) \circ ω_{c} = T (f, 1_{c^{'}}) \circ ω_{c^{'}}$ for every $f : c \to c^{'}$ , and a morphism of wedges is a morphism of the vertices commuting with every component (Wedges and cowedges, and the categories they form).

[F3]

An end of $T$ is a terminal object of the category of wedges over $T$ and a coend an initial object of the category of cowedges under $T$ ; in short, an end is a terminal wedge and a coend an initial cowedge (The end and the coend of a functor $C^{o p} \times C \to D$ ).

[L1]

For a small source category and a locally small target, the set of natural transformations is an end of the hom-bifunctor of the values: $Nat (F, G) = \int_{c} D (F c, G c)$ , with the integrand $(c_{1}, c_{2}) \mapsto D (F c_{1}, G c_{2})$ (For a small source category, the set of natural transformations is an end of the hom-bifunctor of the values).

[L2]

For locally small $C$ the evaluation maps $E_{a, F} : Nat (C (a, -), F) \overset{≅}{\to} F (a)$ are bijections natural in both variables, given by $α \mapsto α_{a} (1_{a})$ (The Yoneda bijection $Nat (C (a, -), F) ≅ F (a)$ is natural in both $a$ and $F$ ).

[L3]

For locally small $C$ , an object $a$ and a presheaf $P$ , evaluation at the identity gives a bijection $E_{P}^{a} : Nat (C (-, a), P) \overset{≅}{\to} P (a), E_{P}^{a} (α) = α_{a} (1_{a})$ (For a presheaf $P$ , $Nat (C (-, a), P) ≅ P (a)$ naturally in $a$ and $P$ ).

Proof

technique · direct

1.1

The variance of each integrand is fixed before anything is computed. In $H$ the representable sits inside the first argument of a function set, and $S e t (-, Y)$ reverses that argument, so $c_{1} \mapsto S e t (C (a, c_{1}), Y)$ is contravariant while $c_{2} \mapsto F c_{2}$ is covariant; hence $H$ is a functor on $C^{o p} \times C$ of the shape $(c_{1}, c_{2}) \mapsto S e t (A c_{1}, B c_{2})$ with $A = C (a, -)$ and $B = F$ both covariant on $C$ . In $H^{'}$ the same two reversals apply to $C (-, a)$ and to $P$ , and both are contravariant on $C$ , so $H^{'}$ has the shape $(c_{1}, c_{2}) \mapsto S e t (A^{'} c_{2}, B^{'} c_{1})$ with $A^{'} = C (-, a)$ and $B^{'} = P$ functors on $C^{o p}$ .

F1F2F4F5

1.2

An end over $C^{o p}$ of a functor $T$ on $(C^{o p})^{o p} \times C^{o p}$ is an end over $C$ of the functor with its two slots exchanged. Indeed, writing $T^{'} (x, y) : = T (y, x)$ , a morphism $f : c \to c^{'}$ of $C^{o p}$ is a morphism $f : c^{'} \to c$ of $C$ , and the wedge equation $T (1_{c}, f) ω_{c} = T (f, 1_{c^{'}}) ω_{c^{'}}$ becomes $T^{'} (f, 1_{c}) ω_{c} = T^{'} (1_{c^{'}}, f) ω_{c^{'}}$ , which is the wedge equation for $T^{'}$ at that morphism of $C$ . The two wedge categories therefore have the same objects and the same morphisms.

F6F7

2.1

For the covariant case, $H$ has the shape required by [L1] with source $C$ and target $S e t$ , which is locally small by [F4], so $\int_{c} S e t (C (a, c), F c) = Nat (C (a, -), F)$ . By [L2] evaluation at the identity is a bijection from that set to $F (a)$ .

F3L1L2step 1.1

3.1

For the contravariant case, step 1.2 rewrites $\int_{c} S e t (C (c, a), P c)$ as the end over $C^{o p}$ of $(x, y) \mapsto S e t (A^{'} x, B^{'} y)$ , and $C^{o p}$ is small with $C$ , so [L1] applied with source $C^{o p}$ gives $Nat (C (-, a), P)$ , the natural transformations being taken between presheaves. By [L3], evaluation at the identity is a bijection from that set to $P (a)$ . The contravariant published corollary is used here rather than the covariant statement read in an opposite category.

F3F5L1L3step 1.1step 1.2step 2.1∎

Remarks

Both displays are ends of a function-set functor, and in each the representable occupies the argument that the function set reverses. Writing either display with the representable in the other slot changes the variance of the integrand and gives a different functor, so the two cases are stated and proved separately rather than by symmetry.

The isomorphism is evaluation at $1_{a}$ in both cases, which is where the object $a$ enters: the component of the wedge at $c = a$ is the only one that sees the identity, and it is what the published Yoneda bijection inverts.

Depends on

Used by

The co-Yoneda isomorphisms: a set-valued functor is a coend against a representable Theorem

Dependency tree · two levels

27 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

F. Loregian, (Co)end Calculus (arXiv:1501.02503v7), §2.2 (standard reference, not scraped)