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

A natural transformation of functors induces a unique morphism of their ends and of their coends

Statement

Let $P, P^{'} : C^{o p} \times C \to D$ be functors and let $η : P \Rightarrow P^{'}$ be a natural transformation (Natural transformation and its components); a wedge is a dinatural transformation from a constant functor (Dinatural transformation between functors on $C^{o p} \times C$ ).

If $P$ and $P^{'}$ have ends $(e, ω)$ and $(e^{'}, ω^{'})$ (The end and the coend of a functor $C^{o p} \times C \to D$ ), then a natural transformation induces a unique morphism of ends: there is exactly one morphism $\int η : e \to e^{'}$ satisfying

$ω_{c}^{'} \circ \int η = η_{c, c} \circ ω_{c} for every object c .$

If $P$ and $P^{'}$ have coends $(q, ρ)$ and $(q^{'}, ρ^{'})$ , there is exactly one morphism $\int^{η} : q \to q^{'}$ satisfying $\int^{η} \circ ρ_{c} = ρ_{c}^{'} \circ η_{c, c}$ for every $c$ .

Moreover $\int 1_{P} = 1_{e}$ , and $\int (η^{'} \circ η) = \int η^{'} \circ \int η$ whenever $η : P \Rightarrow P^{'}$ and $η^{'} : P^{'} \Rightarrow P^{''}$ are natural and all three ends exist.

Facts & Assumptions

Given: Functors $P, P^{'} : C^{o p} \times C \to D$ , a natural transformation $η : P \Rightarrow P^{'}$ , and ends and coends of $P$ and of $P^{'}$ where these are asserted to exist.

[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, and the universal property says that every wedge factors through the end by exactly one morphism (The end and the coend of a functor $C^{o p} \times C \to D$ ).

[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^{'}$ ; dually 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)$ (Wedges and cowedges, and the categories they form).

[F3]

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

[F4]

A dinatural transformation $α : P \to Q$ is a family $α_{c} : P (c, c) \to Q (c, c)$ such that every $f : c \to c^{'}$ satisfies $Q (1_{c}, f) \circ α_{c} \circ P (f, 1_{c}) = Q (f, 1_{c^{'}}) \circ α_{c^{'}} \circ P (1_{c^{'}}, f)$ , the equation displayed by the hexagon (Dinatural transformation between functors on $C^{o p} \times C$ ).

Proof

technique · direct

1.1

The family $η_{c, c} \circ ω_{c} : e \to P^{'} (c, c)$ is a wedge from $e$ to $P^{'}$ : naturality of $η$ at $(1_{c}, f) : (c, c) \to (c, c^{'})$ gives $P^{'} (1_{c}, f) \circ η_{c, c} = η_{c, c^{'}} \circ P (1_{c}, f)$ , naturality at $(f, 1_{c^{'}}) : (c^{'}, c^{'}) \to (c, c^{'})$ gives $P^{'} (f, 1_{c^{'}}) \circ η_{c^{'}, c^{'}} = η_{c, c^{'}} \circ P (f, 1_{c^{'}})$ , and the wedge equation for $ω$ gives $P (1_{c}, f) \circ ω_{c} = P (f, 1_{c^{'}}) \circ ω_{c^{'}}$ , so both sides of the wedge equation for $η_{c, c} \circ ω_{c}$ equal $η_{c, c^{'}}$ composed with that common morphism.

F2F3F4

2.1

Since $(e^{'}, ω^{'})$ is a terminal wedge, the wedge of step 1.1 factors through it by exactly one morphism, which is the asserted $\int η : e \to e^{'}$ with $ω_{c}^{'} \circ \int η = η_{c, c} \circ ω_{c}$ for every $c$ .

F1step 1.1

3.1

Taking $P^{'} = P$ , $η = 1_{P}$ and $(e^{'}, ω^{'}) = (e, ω)$ , the identity of $e$ satisfies the defining equation of step 2.1, and that equation has exactly one solution, so $\int 1_{P} = 1_{e}$ .

F1step 2.1

3.2

For $η : P \Rightarrow P^{'}$ and $η^{'} : P^{'} \Rightarrow P^{''}$ with all three ends present, both $\int η^{'} \circ \int η$ and $\int (η^{'} \circ η)$ satisfy $ω_{c}^{''} \circ (-) = η_{c, c}^{'} \circ η_{c, c} \circ ω_{c}$ , and that equation has exactly one solution, so the two agree.

F1step 2.1

4.1

For coends, the family $ρ_{c}^{'} \circ η_{c, c} : P (c, c) \to q^{'}$ is a cowedge under $P$ : naturality of $η$ at $(f, 1_{c}) : (c^{'}, c) \to (c, c)$ and at $(1_{c^{'}}, f) : (c^{'}, c) \to (c^{'}, c^{'})$ rewrites both sides of its cowedge equation as $ρ_{c}^{'} \circ P^{'} (f, 1_{c}) \circ η_{c^{'}, c}$ and $ρ_{c^{'}}^{'} \circ P^{'} (1_{c^{'}}, f) \circ η_{c^{'}, c}$ , which agree by the cowedge equation for $ρ^{'}$ ; initiality of $(q, ρ)$ then gives exactly one $\int^{η} : q \to q^{'}$ with $\int^{η} \circ ρ_{c} = ρ_{c}^{'} \circ η_{c, c}$ . The induced morphism runs from the coend of $P$ to the coend of $P^{'}$ , in the same direction as $η$ , and the argument is written out here rather than left to duality because the universal property used is initiality rather than terminality.

F1step 1.1step 2.1∎

Remarks

The two functor laws in steps 3.1 and 3.2 are proved from uniqueness alone and use nothing about $η$ beyond its defining equation. So on any full subcategory of functors all of whose objects have a chosen end, the assignment $P \mapsto e$ with $η \mapsto \int η$ is a functor; making that statement precise for a family of parameters, where the choice has to be made for every parameter value at once, is A chosen family of ends is the object part of exactly one functor making the counit natural in the parameters.

Depends on

Used by

A chosen family of ends is the object part of exactly one functor making the counit natural in the parameters Theorem

Dependency tree · two levels

10 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), Remark 1.1.7 (standard reference, not scraped)
G. M. Kelly, Basic Concepts of Enriched Category Theory (TAC Reprints 10), §2.1 (standard reference, not scraped)