Alphabeta MathHow 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.
A continuous bijection of compact Hausdorff spaces is a homeomorphism, by conservativity
Statement
Assume UL/BPI. Every continuous bijection between compact Hausdorff spaces is a homeomorphism.
Facts & Assumptions
Given: UL/BPI and a continuous bijection between compact Hausdorff spaces.
Every monadic functor reflects isomorphisms (Every monadic functor is conservative).
Under UL/BPI, compact Hausdorff spaces are monadic over sets (Under the ultrafilter lemma, compact Hausdorff spaces are monadic over sets).
A homeomorphism is a continuous bijection whose inverse is continuous (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).
Proof
By [L1] and [L2], the underlying-set functor from compact Hausdorff spaces reflects isomorphisms.
The underlying function of is a bijection, hence an isomorphism in . Conservativity from step 1.1 makes an isomorphism in the category of compact Hausdorff spaces.
The categorical inverse of is a continuous map, so is a continuous bijection with continuous inverse and is a homeomorphism by [L3]. This includes empty and singleton spaces.
Remarks
The same conclusion has a direct topological proof: 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 makes the inverse send closed sets to closed sets when the codomain is Hausdorff. The proof above records how the conclusion follows instead from monadic conservativity.
Depends on
- Under the ultrafilter lemma, compact Hausdorff spaces are monadic over sets
- Every monadic functor is conservative
- Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological
- Topological spaces and continuous maps form the large locally small category $\mathbf{Top}$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
21 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, 2nd ed., Corollary 5.6.2 (standard reference, not scraped)