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.
Under the ultrafilter lemma, compact Hausdorff spaces are monadic over sets
Statement
Assume UL/BPI. The underlying-set functor is monadic. Its induced monad is the ultrafilter monad, and its comparison with the Eilenberg–Moore category of ultrafilter algebras is an equivalence, in fact an isomorphism over .
Facts & Assumptions
Given: UL/BPI and the ultrafilter monad on .
Compact Hausdorff spaces and ultrafilter algebras are recovered by inverse object and morphism constructions over (Under the ultrafilter lemma, compact Hausdorff spaces and ultrafilter algebras are recovered by the two limit constructions).
The Eilenberg–Moore adjunction of a monad induces that monad on the nose (The free–forgetful Eilenberg–Moore adjunction induces the given monad).
A right adjoint is monadic when its comparison functor is an equivalence of categories (Monadic and strictly monadic functors).
Proof
By [L1], the category with its underlying-set functor is isomorphic over to the Eilenberg–Moore category .
Transport the Eilenberg–Moore free-forgetful adjunction across this isomorphism. Its right adjoint is the compact-Hausdorff underlying-set functor.
By [L2], the monad induced by this adjunction is the ultrafilter monad on the nose.
The comparison is the isomorphism of [L1], hence an equivalence. Therefore the underlying-set functor is monadic by [L3], with UL/BPI as the only choice assumption used in [L1].
Depends on
- Under the ultrafilter lemma, compact Hausdorff spaces and ultrafilter algebras are recovered by the two limit constructions
- The free–forgetful Eilenberg–Moore adjunction induces the given monad
- Monadic and strictly monadic functors
- The ultrafilter endofunctor with principal unit and flattening multiplication is a monad
- The ultrafilter extension principle (UL/BPI)
Used by
Dependency tree · two levels
19 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.5.6 (standard reference, not scraped)
- J. Goubault-Larrecq, Algebras of filter-related monads: I. Ultrafilters and Manes' theorem (standard reference, not scraped)