PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-16

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.

Under the ultrafilter lemma and dependent choice, compact Hausdorff spaces satisfy the explicit SAFT hypotheses for their inclusion into topological spaces

Statement

Assume the ultrafilter lemma and dependent choice. The category $C o m p H a u s$ is complete and locally small, has the coseparating object $[0, 1]$ , and has a supplied well-powering by closed subspace inclusions. Its full inclusion $I : C o m p H a u s ↪ T o p$ preserves all small limits. Hence it satisfies the supplied-well-powering branch of the special adjoint functor theorem.

Facts & Assumptions

Given: The ultrafilter lemma and dependent choice.

[L1]

Under the ultrafilter lemma, arbitrary products of compact Hausdorff spaces are compact (Assuming the ultrafilter lemma, an arbitrary product of compact Hausdorff spaces is compact).

[L2]

The category $T o p$ has all small limits, computed on underlying sets (Top is complete and cocomplete, and its underlying-set functor preserves all small limits and colimits).

[L3]

A closed subspace of a compact space is compact, and a compact Hausdorff space is normal and $T_{1}$ (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact, A compact Hausdorff space is regular and normal, hence $T_{3}$ and $T_{4}$ ).

[L4]

If $f : X \to Y$ is continuous and $K \subseteq X$ is compact then $f [K]$ is a compact subset of $Y$ ; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

[L5]

Under dependent choice, $[0, 1]$ is coseparating in $C o m p H a u s$ (Under dependent choice, the unit interval is a coseparating object in compact Hausdorff spaces).

[L6]

A supplied well-powering gives, as data for every object $C$ at once, a set $M_{C}$ of monomorphisms into $C$ containing a representative of every subobject class of $C$ (Well-powered and co-well-powered categories, and supplied well-powerings).

[L7]

For a small diagram $D$ , if the products $P = \prod_{j} D (j)$ and $Q = \prod_{u : j \to k} D (k)$ and the equalizer of the two induced maps $s, t : P ⇉ Q$ exist, then that equalizer is a limit of $D$ (Every small limit can be constructed as an equalizer between products over the objects and arrows of the index category).

[L8]

In a Hausdorff space every compact subset is closed (In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones).

Proof

technique · direct

1.1L1L2L3L7

By [L7] a small limit is the equalizer of two maps between two products, so it is constructed from a product and an equalizer. By [L1] the required compact-Hausdorff product is compact, and the equalizer of $s, t : P ⇉ Q$ is ${p \in P : s (p) = t (p)}$ , which is the preimage of the diagonal of $Q$ under the continuous map $(s, t)$ and so is closed because a space is Hausdorff exactly when its diagonal is closed; [L3] makes it compact, while subspaces of Hausdorff spaces are Hausdorff. Thus the topological limit lies in $C o m p H a u s$ and the inclusion preserves it, including the empty limit.

2.1step 1.1L3L4L6L8

A monomorphism $m : A \to B$ in $C o m p H a u s$ is injective: the one-point space is compact Hausdorff, so if $m (a) = m (a^{'})$ the two maps ${*} \to A$ picking $a$ and $a^{'}$ are continuous and equalised by $m$ , whence $a = a^{'}$ . Its image is compact by the continuous-image clause of [L4] and hence closed in the Hausdorff codomain by [L8]; the corestriction $A \to m [A]$ is then a continuous bijection from a compact space to a Hausdorff space, so by [L4] the domain is homeomorphic to that image. Thus each subobject is represented by the inclusion of a closed subset, and these inclusions form a set indexed by the power set of the underlying set. This is a supplied well-powering in the sense of [L6], and intersections are the corresponding set-indexed closed subspaces.

3.1step 1.1step 2.1L5L6∎

Local smallness follows because continuous maps form subsets of function sets. Combining completeness and continuity from step 1.1, the supplied well-powering from step 2.1, and the coseparating object from [L5] gives exactly the supplied-well-powering SAFT hypotheses. The ultrafilter lemma is spent in [L1], while dependent choice is spent in [L5].

Depends on

Used by

With the SAFT initial comma objects supplied for all spaces, they assemble into the compact-Hausdorff reflection and agree on Tychonoff spaces with the constructed Stone-Cech adjunction Theorem

Dependency tree · two levels

55 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

S. Mac Lane, Categories for the Working Mathematician, compact-Hausdorff example after V.8 (standard reference, not scraped)
E. Riehl, Category Theory in Context, example 4.7.12 (standard reference, not scraped)