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

The end of a functor made mute in its contravariant variable is the ordinary limit of that functor

Statement

Let $F : C \to D$ be a functor and let $F^{'} : C^{o p} \times C \to D$ be given by $F^{'} (c_{1}, c_{2}) : = F (c_{2})$ on objects and $F^{'} (f_{1}, f_{2}) : = F (f_{2})$ on morphisms (Product category and its projection functors, Opposite category $C^{o p}$ ), so that $F^{'}$ ignores its contravariant variable.

Then the end of a functor made mute in its contravariant variable is the ordinary limit of that functor: the wedges over $F^{'}$ are exactly the cones over $F$ and the morphisms between them are the same morphisms (Wedges and cowedges, and the categories they form, Constant diagrams, cones, cocones, and their morphisms), so $F^{'}$ has an end exactly when $F$ has a limit (The end and the coend of a functor $C^{o p} \times C \to D$ , Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties) and then

$\int_{c} F^{'} (c, c) = \lim_{c \in C} F (c) .$

Dually, the cowedges under $F^{'}$ are exactly the cocones under $F$ , so $F^{'}$ has a coend exactly when $F$ has a colimit, and then $\int^{c} F^{'} (c, c) = {colim}_{c \in C} F (c)$ .

Facts & Assumptions

Given: A functor $F : C \to D$ and the assignment $F^{'}$ displayed in the Statement.

[F1]

A functor satisfies $F (1_{A}) = 1_{F A}, F (g \circ f) = F g \circ F f$ (Covariant functor, identity functor, composite functor, and contravariant functor).

[F2]

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

[F3]

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

[F4]

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

[F5]

A cone over $D : J \to C$ with apex $c$ is a family $λ_{j} : c \to D (j)$ satisfying $D (u) λ_{j} = λ_{k}$ for $u : j \to k$ , a cocone is a family $ρ_{j} : D (j) \to c$ satisfying $ρ_{k} D (u) = ρ_{j}$ , and a morphism of cones is $h : c \to c^{'}$ with $λ_{j}^{'} h = λ_{j}$ (Constant diagrams, cones, cocones, and their morphisms).

[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$ ; a colimit is an initial cocone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F7]

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

The assignment $F^{'}$ is a functor: $F^{'} (1_{c_{1}}, 1_{c_{2}}) = F (1_{c_{2}}) = 1_{F (c_{2})}$ , and a composite in $C^{o p} \times C$ has second coordinate the composite of the second coordinates, so $F^{'}$ of it is $F$ of that composite, which is the composite of the values of $F^{'}$ .

F1F2

2.1

For a family $α_{c} : X \to F^{'} (c, c) = F (c)$ the wedge equation at $f : c \to c^{'}$ reads $F^{'} (1_{c}, f) \circ α_{c} = F^{'} (f, 1_{c^{'}}) \circ α_{c^{'}}$ , that is $F (f) \circ α_{c} = α_{c^{'}}$ , which is the cone equation of [F5] verbatim; likewise the cowedge equation reads $α_{c} = α_{c^{'}} \circ F (f)$ , which is the cocone equation. The wedge and cone conditions on one family are therefore the same equation, not merely equivalent ones.

F3F4F5step 1.1

3.1

A morphism of wedges over $F^{'}$ is a morphism $h$ of $D$ with $ω_{c}^{'} h = ω_{c}$ for every $c$ , and that is exactly the defining condition of a morphism of cones over $F$ ; so the two categories have the same objects and the same morphisms, and a terminal object of one is a terminal object of the other. By [F7] and [F6], $F^{'}$ has an end exactly when $F$ has a limit, and the two are the same object with the same components.

F5F6F7step 2.1

4.1

The same argument in the dual direction gives that the cowedges under $F^{'}$ and their morphisms are the cocones under $F$ and their morphisms, so an initial object of one category is an initial object of the other, and $F^{'}$ has a coend exactly when $F$ has a colimit, with the same vertex and components.

F5F7step 2.1step 3.1∎

Remarks

This is the sense in which ends generalise limits rather than sitting beside them: a diagram indexed by $C$ becomes a two-variable functor that does not use its first variable, and its end is the limit already defined. The proof cites the published cone and limit definitions and restates neither, so no second notion of limit is introduced here.

Nothing in the argument needs $C$ to be small or $D$ to have any limits: the two universal properties are identified as conditions, and the existence of an object satisfying them is transported in both directions.

Depends on

Used by

Fubini checked by hand on a product of two walking arrows Example
FALSE: every functor preserves the ends that exist in its domain False statement

Dependency tree · two levels

12 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.2.5 (standard reference, not scraped)