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.

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 · two levels

28 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, Proposition 3.6.2 (standard reference, not scraped)