TheoremStatement: Literature-sourcedProof: AI-generatedprecheck 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 co-Yoneda isomorphisms: a set-valued functor is a coend against a representable

Statement

Let $C$ be locally small (Small, locally small, and large categories) and let $a$ be an object of $C$ . A set-valued functor is a coend against a representable (The end and the coend of a functor $C^{o p} \times C \to D$ , The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding):

Covariant coend form. For $F : C \to S e t$ , let $T (c_{1}, c_{2}) : = C (c_{1}, a) \times F (c_{2})$ (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category, The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ , Sets and functions form the large locally small category $S e t$ ), a functor $C^{o p} \times C \to S e t$ . Then $T$ has a coend and

$\int^{c} C (c, a) \times F (c) ≅ F (a),$

the initial cowedge being $ρ_{c} (g, y) = F (g) (y)$ for $g : c \to a$ and $y \in F (c)$ .

Contravariant coend form. For a presheaf $P : C^{o p} \to S e t$ (Opposite category $C^{o p}$ ), let $T^{'} (c_{1}, c_{2}) : = C (a, c_{2}) \times P (c_{1})$ . Then $T^{'}$ has a coend and

$\int^{c} C (a, c) \times P (c) ≅ P (a),$

the initial cowedge being $ρ_{c}^{'} (g, y) = P (g) (y)$ for $g : a \to c$ and $y \in P (c)$ .

End forms. If in addition $C$ is small, the two dual formulas $\int_{c} S e t (C (a, c), F c) ≅ F (a)$ and $\int_{c} S e t (C (c, a), P c) ≅ P (a)$ hold; these are The end of the function-set functor on a representable is evaluation and are not reproved here.

Facts & Assumptions

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

[F6]

A category is locally small when every $C (A, B)$ is a set (Small, locally small, and large categories).

[F5]

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

[F4]

The elements of $A \times B$ are exactly the ordered pairs $(a, b)$ with $a \in A$ and $b \in B$ : Thus $z \in A \times B$ holds if and only if $z = (a, b)$ for some $a \in A$ and some $b \in 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)}$ ).

[F1]

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

[F7]

A functor satisfies $F (1_{A}) = 1_{F A}, F (g \circ f) = F g \circ F f$ ; a contravariant functor is a functor on the opposite category, so it reverses composites (Covariant functor, identity functor, composite functor, and contravariant functor).

[F2]

A cowedge from $T$ to $d$ is a dinatural transformation from $T$ to a constant functor: a family $ρ_{c} : T (c, c) \to d$ with $ρ_{c} \circ T (f, 1_{c}) = ρ_{c^{'}} \circ T (1_{c^{'}}, f)$ for every $f : c \to c^{'}$ (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, so a coend is a cowedge through which every cowedge factors by exactly one morphism (The end and the coend of a functor $C^{o p} \times C \to D$ ).

[L1]

For small $C$ , the end of the function-set functor on a representable is evaluation: $\int_{c} S e t (C (a, c), F c) ≅ F (a)$ and $\int_{c} S e t (C (c, a), P c) ≅ P (a)$ (The end of the function-set functor on a representable is evaluation).

Proof

technique · direct

1.1F1F4F5F6F7

Both integrands are functors on $C^{o p} \times C$ with values in $S e t$ , local smallness making each hom-collection a set. In $T$ the slot $c_{1}$ is contravariant because $C (-, a)$ is, and $c_{2}$ is covariant because $F$ is; explicitly $T (f, 1_{c}) (g, y) = (g \circ f, y)$ and $T (1_{c^{'}}, f) (g, y) = (g, F (f) (y))$ for $f : c \to c^{'}$ , $g \in C (c^{'}, a)$ and $y \in F (c)$ . In $T^{'}$ the slot $c_{1}$ is contravariant because $P$ is and $c_{2}$ is covariant because $C (a, -)$ is; explicitly $T^{'} (f, 1_{c}) (g, y) = (g, P (f) (y))$ and $T^{'} (1_{c^{'}}, f) (g, y) = (f \circ g, y)$ for $g \in C (a, c)$ and $y \in P (c^{'})$ .

2.1F2F4F7step 1.1

The family $ρ_{c} (g, y) = F (g) (y)$ is a cowedge from $T$ to $F (a)$ : on an element $(g, y)$ of $T (c^{'}, c) = C (c^{'}, a) \times F (c)$ the left side gives $ρ_{c} (g f, y) = F (g f) (y)$ and the right side gives $ρ_{c^{'}} (g, F (f) y) = F (g) (F (f) (y))$ , and these agree by functoriality of $F$ .

2.2F2F4F7step 1.1

The family $ρ_{c}^{'} (g, y) = P (g) (y)$ is a cowedge from $T^{'}$ to $P (a)$ : on an element $(g, y)$ of $T^{'} (c^{'}, c) = C (a, c) \times P (c^{'})$ the left side gives $ρ_{c}^{'} (g, P (f) y) = P (g) (P (f) (y))$ and the right side gives $ρ_{c^{'}}^{'} (f g, y) = P (f g) (y)$ , and these agree because $P$ reverses composites.

3.1F2F3F4step 2.1

The cowedge of step 2.1 is initial. Let $λ_{c} : C (c, a) \times F (c) \to X$ be any cowedge and put $u (z) : = λ_{a} (1_{a}, z)$ for $z \in F (a)$ . Applying the cowedge equation of $λ$ at the morphism $g : c \to a$ to the element $(1_{a}, y)$ of $T (a, c) = C (a, a) \times F (c)$ gives $λ_{c} (1_{a} \circ g, y) = λ_{a} (1_{a}, F (g) (y))$ , that is $λ_{c} (g, y) = u (F (g) (y)) = u (ρ_{c} (g, y))$ , so $u ρ_{c} = λ_{c}$ for every $c$ . Any $u^{'}$ with $u^{'} ρ_{c} = λ_{c}$ satisfies $u^{'} (z) = u^{'} (ρ_{a} (1_{a}, z)) = λ_{a} (1_{a}, z) = u (z)$ , so $u$ is unique.

3.2F2F3F4step 2.2

The cowedge of step 2.2 is initial by the same computation in the other variance. Let $λ_{c}^{'} : C (a, c) \times P (c) \to X$ be a cowedge and put $u (z) : = λ_{a}^{'} (1_{a}, z)$ for $z \in P (a)$ . The cowedge equation of $λ^{'}$ at $g : a \to c$ applied to $(1_{a}, y)$ in $T^{'} (c, a) = C (a, a) \times P (c)$ gives $λ_{a}^{'} (1_{a}, P (g) (y)) = λ_{c}^{'} (g \circ 1_{a}, y)$ , that is $λ_{c}^{'} (g, y) = u (ρ_{c}^{'} (g, y))$ ; and $u^{'} (z) = u^{'} (ρ_{a}^{'} (1_{a}, z)) = λ_{a}^{'} (1_{a}, z)$ forces uniqueness.

4.1F3L1step 3.1step 3.2∎

By [F3] an initial cowedge is a coend, so steps 3.1 and 3.2 give the two displayed coend isomorphisms, with the stated initial cowedges. The two end forms are [L1] and are quoted, not reproved; they carry the extra hypothesis that $C$ be small, which the coend forms do not need.

Remarks

Every class in the coend has a representative in the summand at $a$ with first coordinate $1_{a}$ : the cowedge equation applied to $(1_{a}, y)$ moves $(g, y)$ to $(1_{a}, F (g) y)$ , which is why the counit at $a$ suffices to define the inverse morphism in steps 3.1 and 3.2. That is the content of the formula, and it is what makes the coend collapse to a single value.

The coend forms need only local smallness, since they are proved from the universal property of a coend directly and never form a product or a quotient over the objects of $C$ . The end forms need $C$ small, because they pass through the set of natural transformations.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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), Proposition 2.2.1 (standard reference, not scraped)