TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

For a small source category, the set of natural transformations is an end of the hom-bifunctor of the values

Statement

Let $C$ be small and $D$ locally small (Small, locally small, and large categories), and let $F, G : C \to D$ be functors. Write $H : C^{o p} \times C \to S e t$ for the functor $H (a, b) : = D (F a, G b)$ , whose action on a morphism $(g, h)$ of the product category sends $u$ to $G h \circ u \circ F g$ (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category, The hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a bifunctor, Sets and functions form the large locally small category $S e t$ ).

Then $Nat (F, G)$ is a set, and the set of natural transformations is an end of the hom-bifunctor of the values (The end and the coend of a functor $C^{o p} \times C \to D$ ): the evaluation family ${ev}_{c} (α) = α_{c}$ is a terminal wedge over $H$ , so

$Nat (F, G) = \int_{c} D (F c, G c) .$

Facts & Assumptions

Given: A small category $C$ , a locally small category $D$ , and functors $F, G : C \to D$ .

[F6]

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

[F7]

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$ ).

[F5]

The functor category $[C, D]$ has functors $C \to D$ as objects and natural transformations as morphisms (Functor category $[C, D]$ ).

[L2]

If $C$ is small and $D$ is locally small, then $[C, D]$ is locally small (If $C$ is small and $D$ is locally small then $[C, D]$ is locally small; if both are small it is small).

[L1]

For every locally small category $C$ , the hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a functor (The hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a bifunctor).

[F3]

The hom-assignment sends $(a, b)$ to $C (a, b)$ , and a morphism of the product category consisting of $h : a^{'} \to a$ and $u : b \to b^{'}$ acts by $C (h, u) : C (a, b) ⟶ C (a^{'}, b^{'}), f ⟼ u \circ f \circ h$ (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category).

[F4]

A natural transformation $α : F \Rightarrow G$ is a family $α_{A} : F A \to G A$ such that every $f : A \to B$ satisfies the naturality equation $G f \circ α_{A} = α_{B} \circ F f$ (Natural transformation and its components).

[F2]

A wedge from $d$ to $T$ is a dinatural transformation from a constant functor to $T$ : 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^{'}$ (Wedges and cowedges, and the categories they form).

[F1]

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$ ).

Proof

technique · direct

1.1F3F5F6F7L1L2given

Local smallness of $D$ makes every $D (F a, G b)$ a set, so by [L1] and [F3] the assignment $H$ is a functor into $S e t$ , being the hom-bifunctor of $D$ composed with $F$ in the contravariant slot and $G$ in the covariant one. Smallness of $C$ together with local smallness of $D$ makes $[C, D]$ locally small by [L2], so $Nat (F, G)$ , which is a hom-collection of that category by [F5], is a set. The two hypotheses buy different things and neither is redundant.

2.1F2F3F4step 1.1

A family $ϕ_{c} : Y \to D (F c, G c)$ satisfies the wedge equation at $f : c \to c^{'}$ exactly when, for every $y \in Y$ , $G f \circ ϕ_{c} (y) = ϕ_{c^{'}} (y) \circ F f$ : the two sides of the wedge equation are $H (1_{c}, f) \circ ϕ_{c}$ and $H (f, 1_{c^{'}}) \circ ϕ_{c^{'}}$ , and by [F3] the first sends $y$ to $G f \circ ϕ_{c} (y)$ and the second sends $y$ to $ϕ_{c^{'}} (y) \circ F f$ . By [F4] that is exactly the condition that for each $y$ the family $(ϕ_{c} (y))_{c}$ is a natural transformation $F \Rightarrow G$ , and the equivalence holds in both directions.

3.1F1F2step 2.1

The evaluation family ${ev}_{c} : Nat (F, G) \to D (F c, G c)$ , $α \mapsto α_{c}$ , is a wedge, since for $α$ natural the condition of step 2.1 is its naturality equation. Given any wedge $ϕ$ with vertex $Y$ , the function $y \mapsto (ϕ_{c} (y))_{c}$ lands in $Nat (F, G)$ by step 2.1 and satisfies ${ev}_{c} \circ u = ϕ_{c}$ for every $c$ ; and any $u$ with that property has $u (y)_{c} = ϕ_{c} (y)$ for every $c$ , so it is that function. Hence the evaluation wedge is terminal.

4.1F1step 3.1∎

By [F1] a terminal wedge is an end, so $Nat (F, G)$ with the evaluation family is an end of $H$ , which is the displayed equality.

Remarks

The two size hypotheses do different work in this sufficient construction. Local smallness of $D$ makes the integrand $S e t$ -valued, and smallness of $C$ guarantees that the collection of natural transformations is a set. Smallness is not necessary for every particular pair of functors: over a large source the natural transformations can still happen to form a set. No such large-source case is asserted by this theorem.

Identity morphisms of $C$ impose nothing: at $f = 1_{c}$ the condition of step 2.1 reads $ϕ_{c} (y) = ϕ_{c} (y)$ . If $C$ is discrete the wedge condition is vacuous and the end is the product of the sets $D (F c, G c)$ , which is also what an unconstrained family is.

Depends on

Used by

Dependency tree · two levels

23 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), Theorem 1.4.1 (standard reference, not scraped)
B. Richter, From Categories to Homotopy Theory (author's draft), Example 4.4.5 (standard reference, not scraped)