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

An end is the equalizer of two products, and a coend the coequalizer of two coproducts

Statement

Let $C$ be a small category (Small, locally small, and large categories) and let $T : C^{o p} \times C \to D$ be a functor. Suppose the two products

$\prod_{c \in Ob (C)} T (c, c), \prod_{(f : c \to c^{'}) \in Mor (C)} T (c, c^{'})$

exist in $D$ (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations), and write $Λ, P$ for the two morphisms between them determined by $q_{f} \circ Λ = T (1_{c}, f) \circ p_{c}$ and $q_{f} \circ P = T (f, 1_{c^{'}}) \circ p_{c^{'}}$ for $f : c \to c^{'}$ , where $p$ and $q$ are the projections of the first and second product.

Then an end is the equalizer of two products (Equalizers and coequalizers as limits and colimits of a parallel pair, The end and the coend of a functor $C^{o p} \times C \to D$ ): $T$ has an end exactly when $Λ, P$ have an equalizer, and then

$\int_{c} T (c, c) = eq (\prod_{c} T (c, c) \begin{array}{c} Λ \\ ⇉ \\ P \end{array} \prod_{f : c \to c^{'}} T (c, c^{'})) .$

Dually, if the coproducts $∐_{c} T (c, c)$ and $∐_{(f : c \to c^{'})} T (c^{'}, c)$ exist, a coend is the coequalizer of two maps between coproducts: the two morphisms $Λ^{'}, P^{'}$ determined on the $f$ -summand by $Λ^{'} \circ ȷ_{f} = ι_{c} \circ T (f, 1_{c})$ and $P^{'} \circ ȷ_{f} = ι_{c^{'}} \circ T (1_{c^{'}}, f)$ have a coequalizer exactly when $T$ has a coend, and then the coend is that coequalizer. Note that the $f$ -summand of the second coproduct is $T (c^{'}, c)$ , with the domain and codomain of $f$ interchanged.

Facts & Assumptions

Given: A small category $C$ , a functor $T$ on $C^{o p} \times C$ , and the displayed products and coproducts wherever they are assumed to exist.

[F1]

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^{'}$ ; a cowedge from $T$ to $d$ is a family $ρ_{c} : T (c, c) \to d$ with $ρ_{c} \circ T (f, 1_{c}) = ρ_{c^{'}} \circ T (1_{c^{'}}, f)$ ; a morphism of wedges is a morphism of the vertices commuting with every component (Wedges and cowedges, and the categories they form).

[F2]

A product of $(A_{i})_{i \in I}$ is an object $P$ with projections $p_{i}$ such that every family $f_{i} : X \to A_{i}$ has a unique pairing $⟨ f_{i} ⟩_{i \in I} : X \to P, p_{i} ⟨ f_{i} ⟩ = f_{i} (i \in I)$ , and dually a coproduct has injections $ι_{i}$ with unique copairings (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[F5]

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

[F3]

An equalizer of $f, g : A ⇉ B$ is a morphism $e : E \to A$ satisfying $f e = g e$ such that, whenever $h : X \to A$ satisfies $f h = g h$ , there is a unique $u : X \to E$ with $e u = h$ ; a coequalizer is the dual (Equalizers and coequalizers as limits and colimits of a parallel pair).

[F6]

A limit of $D$ is a terminal cone: explicitly, for every cone $(X, ξ)$ there exists a unique morphism $u : X \to L$ such that $λ_{j} u = ξ_{j}$ for every $j$ (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F4]

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

Because $C$ is small, $Ob (C)$ and $Mor (C)$ are sets, so the two displayed families are set-indexed and the products named in the hypothesis are products of set-indexed families; no product over a proper class is formed anywhere below. The morphisms $Λ$ and $P$ exist and are unique because a morphism into a product is determined by its components.

F1F2F5given

2.1

For an object $X$ , the pairing of [F2] is a bijection between morphisms $u : X \to \prod_{c} T (c, c)$ and families $α_{c} : X \to T (c, c)$ , given by $α_{c} = p_{c} u$ . Under it, $Λ u = P u$ holds exactly when $q_{f} Λ u = q_{f} P u$ for every $f$ , that is exactly when $T (1_{c}, f) α_{c} = T (f, 1_{c^{'}}) α_{c^{'}}$ for every $f : c \to c^{'}$ , which is the wedge equation. So the equalising morphisms $X \to \prod_{c} T (c, c)$ correspond exactly to the wedges with vertex $X$ , in both directions.

F1F2F3step 1.1

3.1

The correspondence of step 2.1 is compatible with precomposition: for $h : X^{'} \to X$ the family attached to $u h$ is $(α_{c} h)$ . So a morphism of wedges $(X, α) \to (X^{'}, α^{'})$ is exactly a morphism $h$ with $u^{'} h = u$ , and a terminal wedge is exactly a universal equalising morphism. By [F3] and [F4] that says $T$ has an end exactly when $Λ, P$ have an equalizer, and then the end is the equalizer, with $ω_{c} = p_{c} e$ ; the same statement read through [F6] identifies both with the limit of the parallel pair.

F3F4F6step 2.1

4.1

Dually, the copairing of [F2] is a bijection between morphisms $v : ∐_{c} T (c, c) \to X$ and families $ρ_{c} : T (c, c) \to X$ , and $v Λ^{'} = v P^{'}$ holds exactly when $ρ_{c} T (f, 1_{c}) = ρ_{c^{'}} T (1_{c^{'}}, f)$ for every $f : c \to c^{'}$ , which is the cowedge equation; the same compatibility with postcomposition then makes an initial cowedge exactly a coequalizer of $Λ^{'}, P^{'}$ . The indexing is written out rather than left to duality because the $f$ -summand of the second coproduct is $T (c^{'}, c)$ and not $T (c, c^{'})$ .

F4step 3.1∎

Remarks

The two index sets are the objects and the morphisms of $C$ , and they are not the objects and morphisms of $Tw (C)$ ; this formula is therefore not an instance of the general construction of a limit from products and equalizers applied to An end is a limit over the twisted arrow category, and a coend is a colimit over its opposite, and it is proved here from the wedge universal property directly.

The identity morphisms of $C$ contribute components to the second product, and they cost nothing: at $f = 1_{c}$ the equalising condition of step 2.1 reads $α_{c} = α_{c}$ . Restricting the second product to the non-identity morphisms would give the same equalizer, but the unrestricted indexing is what makes the two morphisms $Λ$ and $P$ definable by a single formula.

Depends on

Used by

Dependency tree · two levels

14 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

G. M. Kelly, Basic Concepts of Enriched Category Theory (TAC Reprints 10), (2.2) (standard reference, not scraped)
F. Loregian, (Co)end Calculus (arXiv:1501.02503v7), Remark 1.2.4 (standard reference, not scraped)