CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26‡ rests on unproved material (inherited)

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.

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Ends exist over a small index category in a complete target, and coends in a cocomplete one

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.

If $D$ is complete, then $T$ has an end. If $D$ is cocomplete, then $T$ has a coend (Finite, small, and large limits and colimits; complete and cocomplete categories, The end and the coend of a functor $C^{o p} \times C \to D$ ).

These conditions are sufficient and are not asserted to be necessary: the definition of an end asks only that a terminal wedge exist, and a particular functor on a large $C$ , or into a target that is not complete, may still have one.

Facts & Assumptions

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

[F1]

The objects of $Tw (C)$ are the morphisms of $C$ , and a morphism $f \to g$ is a pair $(a, b)$ of morphisms of $C$ with $b f a = g$ (The twisted arrow category and its projection to $C^{o p} \times C$ ).

[F2]

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

[L1]

The wedges over $T$ are the cones over $T π$ , so an end is the limit over the twisted arrow category, and a coend is a colimit over $Tw (C)^{o p}$ of the integrand read with domain and codomain swapped (An end is a limit over the twisted arrow category, and a coend is a colimit over its opposite).

[F3]

A category is complete when it has all small limits and cocomplete when it has all small colimits, a diagram being small when its indexing category is small; Completeness and cocompleteness do not assert the existence of limits or colimits of large diagrams (Finite, small, and large limits and colimits; complete and cocomplete categories).

Proof

technique · direct

1.1

$Tw (C)$ is small. Its objects are the morphisms of $C$ , which form a set because $C$ is small. A morphism of $Tw (C)$ carries its domain $f$ , its codomain $g$ and the pair $(a, b)$ , so the collection of all of them is a subclass of the fourfold product $Mor (C) \times Mor (C) \times Mor (C) \times Mor (C)$ , cut out by the equation $b f a = g$ ; a subclass of a set is a set, and no choice is used to form it.

F1F2given

2.1

The diagram $T π$ is therefore a small diagram in $D$ , so completeness of $D$ supplies a limit for it, and by [L1] that limit is an end of $T$ .

L1F3step 1.1

3.1

The opposite of a small category is small, since it has the same objects and the same morphisms, so $T π^{s w}$ is a small diagram as well and cocompleteness of $D$ supplies a colimit for it, which by [L1] is a coend of $T$ .

L1F3step 1.1∎

Remarks

The smallness count is carried out rather than asserted because it is where a size hypothesis could quietly be dropped: it is the morphisms of $Tw (C)$ , not only its objects, that have to form a set before $T π$ counts as a small diagram, and that in turn needs $Mor (C)$ to be a set rather than merely each hom-set to be one. A locally small but large $C$ is not enough.

Sufficiency is all that is claimed. That the hypotheses cannot simply be dropped is FALSE: every functor on $C^{o p} \times C$ has an end, which exhibits a small index category and a target that is not complete in which an end fails to exist.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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

B. Richter, From Categories to Homotopy Theory (author's draft), Proposition 4.5.3 (standard reference, not scraped)