Lemma II.2.8 (自由フィルターの特徴づけ)
- Lemma II.2.8 (自由フィルターの特徴づけ) #Card
- 無限集合上の proper filter が自由であることの $(X)_0$ による言い換え。
A proper filter $\mathcal{F}$ on an infinite set $X$ is free if and only if $\mathcal{F} \supset (X)_0$（補有限フィルターを含む）.
証明の骨子:
-
（$\Rightarrow$）$\mathcal{F}$ 自由 $\iff \operatorname{ker}\mathcal{F} = \bigcap_{F \in \mathcal{F}} F = \emptyset$。すると各 $x \in X$ に対し $x \notin F$ なる $F \in \mathcal{F}$ があり、isotone より $X \setminus {x} \in \mathcal{F}$。有限交叉閉性から任意の有限 $G$ で $X \setminus G = \bigcap_{x \in G}(X \setminus {x}) \in \mathcal{F}$、すなわち $(X)_0 \subset \mathcal{F}$。
-
（$\Leftarrow$）逆に $(X)_0 \subset \mathcal{F}$ なら、$\operatorname{ker}(X)0 = \bigcap{x}(X \setminus {x}) = \emptyset$ かつ $\operatorname{ker}\mathcal{F} \subset \operatorname{ker}(X)_0 = \emptyset$、よって $\mathcal{F}$ は自由。
-
鍵: 自由性を「各点を除く集合を含む」に翻訳し、有限交叉で cofinite 集合すべてを回収する。
-
$(X)_0$ は最粗の自由フィルター——第III章の「補有限収束が最粗の自由収束」（cards/topology/lem-iii-3-9）の土台。
Filter.le_cofinite_iff_eventually_ne 系（Mathlib 順序では f ≤ cofinite）
本ノート RoyalRoad.ChapterII.lem_II_2_8（f ≤ cofinite ↔ ker f = ∅、Notes/ChapterII.lean、lake build 済み）