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

A coend is a colimit weighted by the hom-bifunctor, and an end a limit weighted by it

Statement

Let $C$ be small (Small, locally small, and large categories), let $M$ be locally small and let $T : C^{o p} \times C \to M$ be a functor. Take the index category to be $J : = C^{o p} \times C$ (Product category and its projection functors, Opposite category $C^{o p}$ ) and $T$ itself as the diagram.

Coend clause. Let $W : J^{o p} \to S e t$ be the weight $W (a, b) : = C (b, a)$ , that is the hom-bifunctor (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) composed with the interchange of the two slots, which is what makes it a functor on $J^{o p}$ and not on $J$ . Then the cowedges under $T$ with vertex $m$ are exactly the natural transformations $W \Rightarrow M (T -, m)$ , naturally in $m$ , so $T$ has a coend exactly when $W ⋆ T$ exists (The end and the coend of a functor $C^{o p} \times C \to D$ , Set-weighted limits and colimits) and then

$\int^{c} T (c, c) = W ⋆ T .$

End clause. Let $W^{'} : J \to S e t$ be the hom-bifunctor itself, $W^{'} (a, b) = C (a, b)$ . Then the wedges over $T$ with vertex $m$ are exactly the natural transformations $W^{'} \Rightarrow M (m, T -)$ , naturally in $m$ , so $T$ has an end exactly when ${W^{'}, T}$ exists and then $\int_{c} T (c, c) = {W^{'}, T}$ .

Facts & Assumptions

Given: A small category $C$ , a locally small category $M$ and a functor $T$ on $C^{o p} \times C$ with values in $M$ .

[F7]

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

[F5]

The product category has morphisms $(f, g) : (C, D) \to (C^{'}, D^{'})$ , componentwise identities, and componentwise composition $(f^{'}, g^{'}) \circ (f, g) = (f^{'} \circ f, g^{'} \circ g)$ (Product category and its projection functors).

[F6]

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

[F4]

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

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

[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^{'}}$ ; a cowedge is a family $ρ_{c} : T (c, c) \to d$ with $ρ_{c} \circ T (f, 1_{c}) = ρ_{c^{'}} \circ T (1_{c^{'}}, f)$ (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$ ).

[F1]

A weighted limit ${W, F}$ is an object that represents the functor sending an object to the set of natural transformations from the weight, and a weighted colimit $W ⋆ F$ is characterised by $M (W ⋆ F, m) ≅ [J^{o p}, S e t] (W, M (F -, m))$ naturally in $m$ (Set-weighted limits and colimits).

[F8]

A representation of a functor is an object together with a natural isomorphism from the corresponding hom-functor; The pair $(R, θ)$ is a representation of $F$ , and $R$ is a representing object (Presheaves, covariantly and contravariantly representable functors, and representations).

Proof

technique · direct

1.1

The index category $J$ is small with $C$ , and $J^{o p}$ is $C \times C^{o p}$ by [F6]. The assignment $W (a, b) = C (b, a)$ is the functor of [L1] composed with the interchange of the two slots, which is an isomorphism $C \times C^{o p} \to C^{o p} \times C$ , so $W$ is a functor on $J^{o p}$ ; the interchange is what the variance requires, and writing the hom-bifunctor on $J$ instead would give the weight of the end clause, not of the coend clause. A morphism $(a, b) \to (a^{'}, b^{'})$ of $J^{o p}$ is a pair $(u, v)$ with $u : a \to a^{'}$ and $v : b^{'} \to b$ in $C$ , and $W$ sends $g \in C (b, a)$ to $u \circ g \circ v$ by [F4].

F4F5F6F7L1

2.1

For the coend clause, send a cowedge $ρ$ with vertex $m$ to the family $α_{(a, b)} (g) : = ρ_{b} \circ T (g, 1_{b})$ for $g \in C (b, a)$ , which equals $ρ_{a} \circ T (1_{a}, g)$ by the cowedge equation of [F2] at $g : b \to a$ . It is natural: for $(u, v)$ as in step 1.1, both $α_{(a^{'}, b^{'})} (u g v)$ and $α_{(a, b)} (g) \circ T (u, v)$ reduce, by the factorisations of $T$ supplied by [F5] and the cowedge equation at $u : a \to a^{'}$ , to $ρ_{a^{'}} \circ T (1_{a^{'}}, u \circ g \circ v)$ . Conversely a natural $α$ gives $ρ_{c} : = α_{(c, c)} (1_{c})$ , whose cowedge equation at $f : c \to c^{'}$ is naturality of $α$ at $(f, 1_{c})$ read against naturality at $(1_{c^{'}}, f)$ , both of which compute $α_{(c^{'}, c)} (f)$ . The two assignments are mutually inverse, since $α_{(c, c)} (1_{c}) = ρ_{c}$ and naturality recovers $α_{(a, b)} (g)$ from $α_{(b, b)} (1_{b})$ .

F2F4F5step 1.1

2.2

For the end clause, send a wedge $ω$ with vertex $m$ to $α_{(a, b)} (g) : = T (1_{a}, g) \circ ω_{a}$ for $g \in C (a, b)$ , which equals $T (g, 1_{b}) \circ ω_{b}$ by the wedge equation of [F2] at $g : a \to b$ . A morphism $(a, b) \to (a^{'}, b^{'})$ of $J$ is a pair $(u, v)$ with $u : a^{'} \to a$ and $v : b \to b^{'}$ , and both $α_{(a^{'}, b^{'})} (v g u)$ and $T (u, v) \circ α_{(a, b)} (g)$ reduce, by the same factorisations and the wedge equation at $u : a^{'} \to a$ , to $T (1_{a^{'}}, v \circ g \circ u) \circ ω_{a^{'}}$ . Conversely a natural $α$ gives $ω_{c} : = α_{(c, c)} (1_{c})$ , and naturality at $(1_{c}, f)$ and at $(f, 1_{c^{'}})$ gives the two sides of the wedge equation.

F2F4F5step 1.1

3.1

Both correspondences are natural in $m$ : postcomposing a cowedge with $h : m \to m^{'}$ postcomposes every $α_{(a, b)} (g)$ with $h$ , and precomposing a wedge with $h : m^{'} \to m$ precomposes every $α_{(a, b)} (g)$ with $h$ . So by [F1] and [F8] an initial cowedge under $T$ is exactly a representing object for $m \mapsto [J^{o p}, S e t] (W, M (T -, m))$ and a terminal wedge exactly a representing object for $m \mapsto [J, S e t] (W^{'}, M (m, T -))$ ; by [F3] the coend of $T$ exists exactly when $W ⋆ T$ does and the end exactly when ${W^{'}, T}$ does, with equality in each case.

F1F3F8step 2.1step 2.2∎

Remarks

The variance of the weight is fixed before any computation and is the point at which the statement can go wrong. A weight for a colimit over $J$ is a presheaf on $J$ , so it is a functor on $C \times C^{o p}$ , and the hom-bifunctor becomes one only after its two slots are interchanged. The weight for the end clause is the hom-bifunctor with no interchange at all.

Together with An end is a limit over the twisted arrow category, and a coend is a colimit over its opposite this closes the loop between the two descriptions of a coend. One presents it as an ordinary colimit over a larger index category; the other presents it as a weighted colimit over the original index category, with the hom-bifunctor carrying the information that the larger index category encoded. The category of elements of the weight is what turns one into the other, by A weighted limit is an ordinary limit over the category of elements of the weight, and a weighted colimit an ordinary colimit over it.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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

E. Riehl, Categorical Homotopy Theory, Example 7.2.9 (standard reference, not scraped)