TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13

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.

Set has all small colimits, realized as a quotient of a set-indexed disjoint union

Statement

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)) (u : j \to k) .$

Facts & Assumptions

Given: A small diagram $D : J \to S e t$ .

[F1]

Smallness makes the object and morphism collections sets, and cocompleteness means existence of all small colimits (Finite, small, and large limits and colimits; complete and cocomplete categories).

[F2]

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

[F3]

An equivalence relation is reflexive, symmetric, and transitive (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ).

[L1]

A function on a set factors uniquely through its quotient precisely when it is constant on equivalence classes (Let $\sim$ be an equivalence relation on $A$ with quotient map $π : A \to A / \sim$ , and let $f : A \to B$ . There is a function $g : A / \sim \to B$ with $g \circ π = f$ if and only if $a \sim a^{'}$ implies $f (a) = f (a^{'})$ ; and such a $g$ is then unique).

[F4]

A colimit has a unique mediating morphism to every cocone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

Proof

technique · construction

1.1

By [F1], $S$ is a set. Intersecting all equivalence relations on $S$ that contain the displayed pairs gives the least such relation $\sim$ ; let $Q = S / \sim$ .

F1F3

2.1

Define $ρ_{j} : D (j) \to Q$ by $ρ_{j} (x) = [j, x]$ . Each generating relation gives $ρ_{k} D (u) = ρ_{j}$ , so $ρ$ is a cocone.

step 1.1

2.2

For a cocone $ξ_{j} : D (j) \to X$ , define $h : S \to X$ by $h (j, x) = ξ_{j} (x)$ . The cocone equations make $h$ equal on every generating pair, hence on the equivalence relation they generate.

givenstep 1.1

2.3

If $J$ is empty, then $S = Q = \emptyset$ ; the empty set has one function to every set, so the same construction is the initial-set colimit.

F2step 1.1

3.1

By [L1], there is a unique $\overset{ˉ}{h} : Q \to X$ with $\overset{ˉ}{h} [j, x] = ξ_{j} (x)$ , equivalently $\overset{ˉ}{h} ρ_{j} = ξ_{j}$ for every $j$ . Any map with these equations has the same composite with the quotient map and therefore equals $\overset{ˉ}{h}$ .

L1step 2.2

4.1

By [F4], the cocone is colimiting. Since $D$ was arbitrary, $S e t$ is cocomplete.

F1F4step 2.1step 3.1step 2.3∎

Depends on

Used by

Dependency tree · two levels

22 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

E. Riehl, Category Theory in Context, Proposition 3.6.1 (standard reference, not scraped)