PropositionStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16‡ 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.

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.1

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.

L1L2L3L7

2.1

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.

step 1.1L3L4L6L8

3.1

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].

step 1.1step 2.1L5L6∎

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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 135 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

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)