Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13‡ rests on unproved material (inherited)
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.

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

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:

  1. all finite limits exist if and only if finite products and equalizers exist, equivalently if and only if a terminal object and pullbacks exist;
  2. all nonempty finite limits exist if and only if binary products and equalizers exist, equivalently if and only if binary products and pullbacks exist;
  3. 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→B×B back along the diagonal B→B×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.

F2
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→B×B along the diagonal B→B×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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 19 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources