ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck 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.

The one-point space represents the underlying-set functor on $T o p$

Example

Let $1 = {*}$ carry its unique topology ${\emptyset, 1}$ . The one-point space represents the underlying-set functor $U : T o p \to S e t$ through the natural bijection

$T o p (1, X) \overset{≅}{\to} U (X), f ⟼ f (*) .$

Facts & Assumptions

Given: The singleton space $1 = {*}$ and an arbitrary topological space $X$ .

[F1]

A topology contains the empty set and the whole underlying set (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[F2]

A function is continuous when it is continuous at every point, equivalently when inverse images of open sets are open (Continuity of a map of topological spaces at a point and globally, For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ , clause (b)).

[F3]

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

[F4]

A covariant set-valued functor is represented by $R$ when it is naturally isomorphic to the hom-functor $T o p (R, -)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[F5]

A function assigns exactly one value to each domain element, and two functions with the same domain and codomain are equal exactly when their values agree everywhere (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain, Functions $f$ and $g$ are equal if and only if $dom f = dom g$ and $f (x) = g (x)$ for every $x$ in that common domain).

Verification

technique · constructive

1.1

For every point $x \in X$ , define $f_{x} : 1 \to X$ by $f_{x} (*) = x$ . For every open $V \subseteq X$ , the inverse image $f_{x}^{- 1} [V]$ is $1$ if $x \in V$ and $\emptyset$ otherwise; [F1] and [F2] make $f_{x}$ continuous.

F1F2construct

2.1

Every function $f : 1 \to X$ equals $f_{f (*)}$ by [F5], and $f_{x} (*) = x$ . Thus $f \mapsto f (*)$ and $x \mapsto f_{x}$ are inverse bijections.

step 1.1F5

3.1

If $g : X \to Y$ is continuous, then $(g \circ f) (*) = g (f (*))$ , so the bijections in step 2.1 commute with the hom-functor action and the underlying function $U (g)$ . They are natural in $X$ , and $U$ is a functor because [F3] uses ordinary function composition.

step 2.1F3

4.1

By [F4], the singleton space represents $U$ . When $X = \emptyset$ , both $T o p (1, X)$ and $U (X)$ are empty, so the same bijection includes that boundary case.

step 3.1F4discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

Emily Riehl, Category Theory in Context, Example 2.1.5(ii) (standard reference, not scraped)

The one-point space represents the underlying-set functor on TopTop