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.

Finite, nonempty finite, and connected finite (co)limit criteria in terms of products, equalizers, pullbacks, terminal objects, and their duals

Statement

For a category $C$ :

all finite limits exist if and only if finite products and equalizers exist, equivalently if and only if a terminal object and pullbacks exist;
all nonempty finite limits exist if and only if binary products and equalizers exist, equivalently if and only if binary products and pullbacks exist;
all finite connected limits exist if and only if pullbacks and equalizers exist.

Reversing arrows gives the three colimit criteria, with coproducts, coequalizers, an initial object, and pushouts.

Facts & Assumptions

Given: A category $C$ .

[F1]

Empty limits are terminal objects, and empty colimits are initial objects (Limits of empty diagrams are terminal objects, and colimits of empty diagrams are initial objects).

[F2]

Products, equalizers, pullbacks, and their duals have their stated universal properties (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations, Equalizers and coequalizers as limits and colimits of a parallel pair, Pullbacks and pushouts as limits and colimits of cospans and spans).

[L1]

A limit is constructed from products over the objects and arrows of its index category and an equalizer (Every small limit can be constructed as an equalizer between products over the objects and arrows of the index category).

[L2]

The dual coproduct-coequalizer construction gives colimits (Every small colimit can be constructed as a coequalizer between coproducts over the arrows and objects of the index category).

[L3]

Formal duality reverses every hypothesis and conclusion (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · equivalence of constructions

1.1

For a finite index category, both products in [L1] are finite, so finite products and equalizers give all finite limits. Conversely, discrete finite diagrams and parallel pairs show that all finite limits give finite products and equalizers.

L1F2

1.2

If the finite index category is nonempty, its object and arrow sets are nonempty, so the two products in [L1] can be built by iterated binary products without a terminal object. This proves sufficiency from binary products and equalizers; those constructions themselves have nonempty finite shapes, proving necessity. If binary products and pullbacks exist, the equalizer of $f, g : A ⇉ B$ is obtained by pulling $(f, g) : A \to B \times B$ back along the diagonal $B \to B \times B$ . Conversely, nonempty finite limits include binary products and pullbacks. This proves every equivalence in clause 2.

L1F2

1.3

For a finite connected diagram, choose a spanning tree in its finite underlying undirected graph and root it at one object. Start with the root object. When a leaf is attached by an arrow directed from the leaf toward the constructed subtree, pull back the current apex along that arrow; when the arrow points toward the leaf, its required leg is the composite of the existing leg with that arrow and the apex does not change. Induction constructs the universal cone for the tree. For each remaining diagram arrow, take the equalizer of the two maps from the current apex to its codomain, and repeat finitely many times. The result represents exactly the cones over the whole diagram. Conversely, pullbacks and equalizers have finite connected indexing categories. This proves both directions of clause 3, including the one-object case, where loops are imposed by equalizers.

2.1

A terminal object and binary products give every finite product by iteration, including the zero-factor product. An equalizer of $f, g : A ⇉ B$ is the pullback of $(f, g) : A \to B \times B$ along the diagonal $B \to B \times B$ . Hence a terminal object and pullbacks give all finite limits by step 1.1.

F1F2step 1.1

3.1

Conversely, finite limits include the terminal object and every pullback. Thus both formulations in clause 1 are equivalent in both directions.

F1F2step 1.1step 2.1

4.1

Applying [L3] to steps 1.1, 1.2, 1.3, 2.1, and 3.1 exchanges every construction with the one in [L2] and proves all three colimit equivalences, including the empty boundary through [F1].

F1L2L3step 1.1step 2.1step 3.1step 1.2step 1.3∎

Depends on

Used by

Dependency tree · two levels

13 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

The Stacks Project, Categories, Lemmas 4.18.2 to 4.18.4 (standard reference, not scraped)
E. Riehl, Category Theory in Context, Theorem 3.5.17 (standard reference, not scraped)