CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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 colimit of a set-valued functor is the set of connected components of its category of elements

Statement

Let $J$ be a small category (Small, locally small, and large categories) and let $D : J \to S e t$ be a functor (Sets and functions form the large locally small category $S e t$ ). Let $\int D$ be its category of elements (The category of elements of a covariant functor or a presheaf) and let $π_{0} (\int D)$ be the quotient of its set of objects by the least equivalence relation (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ) containing every pair $(a, b)$ for which there is a morphism $a \to b$ ; two objects lie in the same class exactly when they are joined by a finite zigzag of morphisms, which is the connectedness condition of Isomorphism, groupoid, and connected category.

Then

${colim}_{j \in J} D (j) = π_{0} (\int D)$

(Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties), the colimiting cocone sending $x \in D (j)$ to the class of the object $(j, x)$ .

Facts & Assumptions

Given: A small category $J$ and a functor $D : J \to S e t$ .

[F5]

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

[F6]

Sets as objects and functions as morphisms form a large locally small category $S e t$ (Sets and functions form the large locally small category $S e t$ ).

[F1]

The category of elements $\int G$ of a functor $G : C \to S e t$ has objects $(c, x)$ with $c \in C$ and $x \in G (c)$ ; and a morphism $(c, x) \to (d, y)$ given by a morphism $f : c \to d$ in $C$ satisfying $G (f) (x) = y$ (The category of elements of a covariant functor or a presheaf).

[L1]

Every small diagram $D : J \to S e t$ has a colimit; it is the quotient of the tagged union $S = {(j, x) : x \in D (j)}$ by the least equivalence relation containing $(j, x) \sim (k, D (u) (x))$ for $u : j \to k$ (Set has all small colimits, realized as a quotient of a set-indexed disjoint union).

[F2]

A binary relation on a set is an equivalence relation when it is reflexive, symmetric and transitive; the quotient set is the set of its classes (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ).

[F3]

A category is connected when it is nonempty and any two objects can be joined by a finite zigzag of morphisms, with successive arrows allowed to point in either direction (Isomorphism, groupoid, and connected category).

[F4]

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

Proof

technique · direct

1.1F1F5F6L1

By [F1] the objects of $\int D$ are exactly the pairs $(j, x)$ with $x \in D (j)$ , which is exactly the tagged union named in [L1]; and a morphism $(j, x) \to (k, y)$ of $\int D$ exists precisely when some $u : j \to k$ has $D (u) (x) = y$ , that is, precisely for the pairs that generate the equivalence relation of [L1].

2.1F2F3step 1.1

The least equivalence relation containing the generating pairs of [L1] is therefore the least equivalence relation on the objects of $\int D$ containing every pair joined by a morphism, and by [F2] its classes are the classes defining $π_{0} (\int D)$ . Two objects lie in one class exactly when a finite chain of generating pairs, each used in either direction, joins them, which is the finite-zigzag condition of [F3].

3.1F4L1step 2.1∎

By [L1] the colimit of $D$ is the quotient of the tagged union by that relation, with cocone components sending $x \in D (j)$ to the class of $(j, x)$ ; by step 2.1 that quotient is $π_{0} (\int D)$ , and by [F4] the universal property of the colimit is the one asserted. If $J$ is empty, or every $D (j)$ is empty, both sides are the empty set.

Remarks

Nothing about the category of elements is used beyond its objects and the existence of its morphisms: the identification is between the generating pairs of the published $S e t$ -colimit construction and the morphisms of $\int D$ , and everything else is the same quotient read twice.

The empty case is not an exception. A category with no objects has no connected components, and a diagram of empty sets has the empty set as its colimit, so both sides are empty; connectedness requires nonemptiness, but a set of components does not.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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), (3.35) (standard reference, not scraped)