LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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 ultrafilter-limit map of a compact Hausdorff space is an algebra for the ultrafilter monad

Statement

Let $X$ be compact Hausdorff, and define $ξ_{X} : β X \to X$ by sending each ultrafilter to its unique limit. Then $ξ_{X}$ is an algebra for the ultrafilter monad:

$ξ_{X} η_{X} = 1_{X}, ξ_{X} μ_{X} = ξ_{X} β (ξ_{X}) .$

Facts & Assumptions

Given: A compact Hausdorff space $X$ and its ultrafilter-limit map $ξ_{X}$ .

[L1]

Every ultrafilter on a compact Hausdorff space has exactly one limit (A given ultrafilter on a compact Hausdorff space has a unique limit).

[L2]

The ultrafilter monad has principal unit $η_{X} (x) = {A \subseteq X : x \in A}$ and flattening multiplication $μ_{X} (W) = {A \subseteq X : \hat{A} \in W}$ , where $\hat{A} = {U : A \in U}$ (The ultrafilter endofunctor with principal unit and flattening multiplication).

[L3]

A $T$ -algebra structure $a$ satisfies $a η = 1$ and $a T (a) = a μ$ (Algebra and algebra homomorphism for a monad).

Proof

technique · direct

1.1L1construct

By [L1], $ξ_{X}$ is defined on every ultrafilter. When $X = \emptyset$ , both $β X$ and $X$ are empty and the unique empty map satisfies the equations below.

2.1step 1.1L2algebra

The principal ultrafilter $η_{X} (x)$ contains every neighbourhood of $x$ , so it converges to $x$ . Uniqueness in [L1] gives $ξ_{X} η_{X} (x) = x$ for every $x$ .

2.2step 1.1L2algebra

Let $W$ be an ultrafilter on $β X$ . If an open neighbourhood $O$ of a point belongs to the pushforward $β (ξ_{X}) (W)$ , then $ξ_{X}^{- 1} [O] \in W$ . Every ultrafilter whose limit lies in $O$ contains $O$ , so $ξ_{X}^{- 1} [O] \subseteq \hat{O}$ ; upward closure gives $\hat{O} \in W$ , hence $O \in μ_{X} (W)$ by [L2]. Thus every limit of the pushforward is a limit of the flattening.

3.1step 2.2L1

Both ultrafilters in step 2.2 have unique limits by [L1], so their limits coincide: $ξ_{X} β (ξ_{X}) (W) = ξ_{X} μ_{X} (W)$ .

4.1step 2.1step 3.1L3∎

Steps 2.1 and 3.1 are exactly the unit and multiplication equations in [L3], so $ξ_{X}$ is an ultrafilter algebra.

Depends on

Used by

Under the ultrafilter lemma, compact Hausdorff spaces and ultrafilter algebras are recovered by the two limit constructions Theorem

Dependency tree · two levels

14 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

J. Goubault-Larrecq, Algebras of filter-related monads: I. Ultrafilters and Manes' theorem (standard reference, not scraped)