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.

Top is complete and cocomplete, and its underlying-set functor preserves all small limits and colimits

Statement

The category $T o p$ has all small limits and colimits. The underlying set functor $U : T o p \to S e t$ preserves every small limit and every small colimit.

Facts & Assumptions

Given: A small diagram $D : J \to T o p$ .

[L1]

The underlying Set-diagram has a limit and a colimit (Set has all small limits, realized as compatible tuples in a set-indexed product, Set has all small colimits, realized as a quotient of a set-indexed disjoint union).

[F1]

Topological spaces and continuous maps form $T o p$ (Topological spaces and continuous maps form the large locally small category $T o p$ ).

[F2]

For the initial topology of a family $(f_{i} : X \to Y_{i})$ , a function $h : Z \to X$ is continuous exactly when every $f_{i} \circ h$ is continuous; dually, for the final topology of a family $(g_{i} : Y_{i} \to X)$ , a function $h : X \to Z$ is continuous exactly when every $h \circ g_{i}$ is continuous (Characteristic properties: a map into a space with the initial topology is continuous iff every composite with the defining family is, a map out of a space with the final topology is continuous iff every composite with the defining family is, and the two topologies are respectively the coarsest and the finest making that family continuous, claims 2 and 4). The topologies themselves are constructed in The initial topology of a family of maps into spaces and the final topology of a family of maps out of spaces, and the subspace topology as the model initial topology, which states these characteristic properties are proved separately.

[F3]

Continuity means inverse images of open sets are open (Continuity of a map of topological spaces at a point and globally).

[F4]

Preservation means that the image of a limiting or colimiting cone is again limiting or colimiting (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

Proof

technique · lift the Set constructions by universal topologies

1.1

Let $(L, p_{j})$ be the Set-limit of $U D$ from [L1]. Give $L$ the initial topology induced by all $p_{j} : L \to U (D (j))$ . Then every $p_{j}$ is continuous and the Set cone equations make it a cone in $T o p$ .

L1F1F2

1.2

Let $(Q, i_{j})$ be the Set-colimit of $U D$ and give $Q$ the final topology induced by all $i_{j} : U (D (j)) \to Q$ . A function $f : Q \to X$ is continuous exactly when every $f i_{j}$ is continuous. Set-universality therefore proves existence and uniqueness of the continuous factor for every Top-cocone. Thus $Q$ is a Top-colimit.

L1F2F3

2.1

For a cone of continuous maps $f_{j} : X \to D (j)$ , Set-universality gives a unique function $f : X \to L$ with $p_{j} f = f_{j}$ . By the characteristic property in [F2], $f$ is continuous exactly because all $p_{j} f$ are continuous. Its uniqueness as a continuous map follows from uniqueness as a function. Hence this is a Top-limit.

L1F2F3step 1.1

3.1

In steps 1.1 and 1.2 the underlying sets, legs, and mediating functions are exactly the Set-limit and Set-colimit data. Applying $U$ removes only the topologies, so both canonical comparisons are identity bijections. By [F4], $U$ preserves all the small limits and colimits.

F4step 1.1step 2.1step 1.2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 65 results over 17 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

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