Proposition II.3.10 (ウルトラフィルターの二分性)
- Proposition II.3.10 (ウルトラフィルターの二分性) #Card
- $\mathcal{F}$ がウルトラフィルターであることの「$A$ か $A^c$ か」による特徴づけ。
A filter $\mathcal{F}$ on $X$ is an ultrafilter if and only if either $A \in \mathcal{F}$ or $X \setminus A \in \mathcal{F}$ for every $\emptyset \neq A \subset X$.
証明の骨子:
-
（$\Rightarrow$）$\mathcal{F}$ ウルトラ、$\emptyset \neq A \notin \mathcal{F}$ とする。isotone より各 $F \in \mathcal{F}$ で $F \setminus A \neq \emptyset$（さもなくば $F \subset A$ から $A \in \mathcal{F}$）。よって ${F \setminus A : F \in \mathcal{F}}$ は filter-base で $\mathcal{F} \setminus A := \mathcal{F} \vee (X\setminus A)^\uparrow \supset \mathcal{F}$ は proper。極大性より $\mathcal{F} \setminus A = \mathcal{F}$、ゆえに $X \setminus A \in \mathcal{F}$。
-
（$\Leftarrow$）対偶。$\mathcal{F}$ が極大でないなら真の proper 細分 $\mathcal{H} \supsetneq \mathcal{F}$ があり、$A \in \mathcal{H} \setminus \mathcal{F}$ を取る。$\mathcal{H}$ proper より $X \setminus A \notin \mathcal{F}$（もし属せば $A \cap (X\setminus A)=\emptyset \in \mathcal{H}$）。よって $A$ も $A^c$ も $\mathcal{F}$ に無い、二分性が破れる。
-
鍵: 「$A \notin \mathcal{F}$」から $\mathcal{F}$ を $X\setminus A$ 側へ真に拡大できるかが極大性を測る。
-
記法: $\mathcal{F} \vee A := \mathcal{F} \vee {A}^\uparrow$（restriction）、$\mathcal{F} \setminus A := \mathcal{F} \vee (X \setminus A)^\uparrow$。
-
任意の proper filter はウルトラフィルターに拡大できる（Kuratowski–Zorn、Cor XXVII.4.9）；$\beta\mathcal{F}$ = $\mathcal{F}$ を含むウルトラフィルター全体、$\beta X$ = $X$ 上のウルトラフィルター全体。
Ultrafilter.mem_or_compl_mem / 拡大は Ultrafilter.exists_le
本ノート RoyalRoad.ChapterII.prop_II_3_10（(∃ u : Ultrafilter X, ↑u = f) ↔ ∀ A, A ∈ f ∨ Aᶜ ∈ f、Notes/ChapterII.lean、lake build 済み）