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.

Every small limit can be constructed as an equalizer between products over the objects and arrows of the index category

Statement

Let $D : J \to C$ be small. If the products

$P = \prod_{j \in Ob J} D (j), Q = \prod_{u : j \to k} D (k)$

and the equalizer of the maps $s, t : P ⇉ Q$ defined by $q_{u} s = D (u) p_{j}$ and $q_{u} t = p_{k}$ exist, then that equalizer is a limit of $D$ .

Facts & Assumptions

Given: The displayed products and an equalizer $e : L \to P$ of $s, t$ .

[F1]

A product represents families of arrows into its factors (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[F2]

An equalizer represents arrows on which its parallel pair agrees (Equalizers and coequalizers as limits and colimits of a parallel pair).

[F3]

A small diagram has sets of objects and arrows (Finite, small, and large limits and colimits; complete and cocomplete categories).

[F4]

A limit represents cones by unique mediating arrows (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

Proof

technique · construction

1.1F1F3

By [F3] the two displayed families are set-indexed. By [F1], the stated coordinate equations define unique maps $s, t : P \to Q$ .

2.1F2step 1.1

Put $λ_{j} = p_{j} e$ . Since $s e = t e$ , equality of the $u$ -coordinates says $D (u) λ_{j} = λ_{k}$ for every $u : j \to k$ . Thus $λ$ is a cone.

2.2F1givenstep 1.1

Given a cone $ξ_{j} : X \to D (j)$ , [F1] supplies a unique $a : X \to P$ with $p_{j} a = ξ_{j}$ . Its cone equations imply $q_{u} s a = D (u) ξ_{j} = ξ_{k} = q_{u} t a$ for all $u$ , so product uniqueness gives $s a = t a$ .

3.1F2step 2.1step 2.2

By [F2], $a$ factors uniquely as $a = e h$ with $h : X \to L$ . Then $λ_{j} h = p_{j} e h = ξ_{j}$ , so $h$ is a cone morphism.

4.1F1F2step 3.1

If $h^{'}$ has the same leg equations, product uniqueness gives $e h^{'} = a = e h$ ; equalizer uniqueness gives $h^{'} = h$ .

5.1F1F2F4step 2.1step 3.1step 4.1∎

Steps 2.1, 2.2, 3.1, and 4.1 are exactly [F4], so $(L, λ)$ is a limit. If $J$ is empty, both products are terminal objects, $s = t$ , and their equalizer is isomorphic to the terminal object, so the construction still applies.

Depends on

Dependency tree · 2 levels

Sources

E. Riehl, Category Theory in Context, Theorem 3.5.11 and Remark 3.2.13