Proposition II.3.2 (フィルターの完備束)
- Proposition II.3.2 (フィルターの完備束) #Card
- $(\overline{\mathbb{F}}X, \subset)$ はどんな構造か。$\bigwedge$ と $\bigvee$ の公式は？
The set $\overline{\mathbb{F}}X$ of all (possibly improper) filters on a given set, ordered by inclusion, is a complete lattice; for non-empty $\mathbb{H}$, $$\bigwedge \mathbb{H} = \bigcap_{\mathcal{H} \in \mathbb{H}} \mathcal{H}, \qquad \bigvee \mathbb{H} = \Big(\bigcup_{\mathcal{H} \in \mathbb{H}} \mathcal{H}\Big)^\cap$$ （$\mathcal{A}^\cap$ = 有限交叉の族）。2 つの場合: $\mathcal{F}_0 \vee \mathcal{F}_1 = {F_0 \cap F_1 : F_i \in \mathcal{F}_i}$, $\mathcal{F}_0 \wedge \mathcal{F}_1 = \mathcal{F}_0 \cap \mathcal{F}_1$。
- Corollary II.3.3: $\bigvee \mathbb{H}$ が proper $\iff$ $\bigcup \mathbb{H}$ の任意の有限部分族の交叉が非空（centered）。
- proper filter だけの $\mathbb{F}X$ は束にすらならない（sup が $2^X$ に退化しうる）——improper filter を許す理由。
- 最粗は ${X}$、最細（退化）は $2^X$、極大 proper がウルトラフィルター。
証明の骨子:
- inf ＝ 共通部分: $\bigcap_{\mathcal{H} \in \mathbb{H}} \mathcal{H}$ 自身がフィルターである（isotone・有限交叉は各 $\mathcal{H}$ で成立し共通部分でも成立）。これは各 $\mathcal{H}$ に含まれる最大の族なので、包含順序で下限。
- sup ＝ 生成: $\bigcup_{\mathcal{H}} \mathcal{H}$ は各 $\mathcal{H}$ を含む最小の族だが一般にフィルターでない。有限交叉で閉じさせた $(\bigcup \mathbb{H})^\cap$ を取ると、これを isotone 化したものが $\bigcup \mathbb{H}$ を含む最小のフィルター＝上限。
- 完備性: 任意の非空 $\mathbb{H}$ に inf・sup が存在するので完備束。ただし improper $2^X$ を許すことが必須（proper だけだと sup が退化して束にならない、Cor II.3.3）。
Filter X の CompleteLattice（Mathlib は順序が逆: 本書の $\bigwedge$ が ⨆）
本ノート RoyalRoad.ChapterII.prop_II_3_2（本書 inf ＝ 族の共通部分 (f ⊔ g).sets = f.sets ∩ g.sets、Notes/ChapterII.lean、lake build 済み）