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 limits, realized as compatible tuples in a set-indexed product

Statement

Every small diagram $D : J \to S e t$ has a limit. It is the set

$L = {(x_{j})_{j \in Ob J} \in \prod_{j} D (j) : D (u) (x_{j}) = x_{k} for every u : j \to k}$

with its coordinate projections.

Facts & Assumptions

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

[F1]

A small category has sets of objects and morphisms, and completeness means existence of limits for all small diagrams (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]

The product of a set-indexed family consists of functions choosing one element from each member (The product $\prod_{i \in I} A_{i} : = {f : I \to ⋃_{i \in I} A_{i} ∣ f (i) \in A_{i} for every i \in I}$ ).

[F4]

A limit requires a unique mediating morphism from every cone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

Proof

technique · construction

1.1F1F2F3

By [F1] and [F3], the displayed product and its subset $L$ are sets. For each $j$ , let $p_{j} : L \to D (j)$ be the coordinate function. The defining equalities give $D (u) p_{j} = p_{k}$ , so $(L, p)$ is a cone.

1.2F3

If $Ob J$ is empty, the product is the singleton containing the empty function and all compatibility conditions are vacuous. Thus the construction still gives the terminal set.

1.3F2given

Let $(X, ξ_{j})$ be any cone. Define $h : X \to \prod_{j} D (j)$ by $h (x)_{j} = ξ_{j} (x)$ . The cone equations imply $h (x) \in L$ , so $h$ corestricts to a function $\overset{ˉ}{h} : X \to L$ satisfying $p_{j} \overset{ˉ}{h} = ξ_{j}$ .

2.1step 1.2step 1.3

If $g : X \to L$ has the same composites, then for every $x$ and $j$ , $g (x)_{j} = p_{j} g (x) = ξ_{j} (x) = p_{j} \overset{ˉ}{h} (x)$ . Equality of functions gives $g = \overset{ˉ}{h}$ . This remains true for the empty index, where there is one function to the singleton.

3.1F1F4step 1.1step 1.3step 2.1∎

By [F4], steps 1.1, 1.3, and 2.1 prove that $(L, p)$ is a limit, with step 1.2 covering the empty boundary. Since $D$ was an arbitrary small diagram, $S e t$ is complete.

Depends on

Used by

Dependency tree · two levels

15 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, Theorem 3.2.4 (standard reference, not scraped)