Skip to content
Journals Garden

Royal Road to Topology Chapter II

Chapter 2: From Convergence of Sequences to the Concept of Filter

Section titled “Chapter 2: From Convergence of Sequences to the Concept of Filter”

This chapter traces the transition from the classical convergence of sequences to the more general and powerful concept of filters.

数学的意味（原著より）

Section titled “数学的意味（原著より）”

章冒頭

Section titled “章冒頭”

フィルターは本書の主要道具であるが、列も単純で有用な装置として残る。フィルターアプローチは列に基づく技法より洞察に富み、射程が広く、器用である。一方、列は列挙のためのものであり、数学の基本的手続の一つである。大まかに言えば、定理の定式化と証明にはフィルターに匹敵するものはなく、反例の構成には列に勝るものはない。

出典: refs/math/topology/royal-road-to-topology/pdfs/chp2-2024-from-convergence-of-sequences-to-the-concept-of-filter.pdf p.17

II.1 Convergence of sequences

Section titled “II.1 Convergence of sequences”

実数直線上の収束の基本定義（Def (A)）を、本書のアプローチの根底にある新しい側面を明らかにする形で再定式化する。$|\varphi(n) - x| < \varepsilon$ は $\varphi(n) \in ]x - \varepsilon, x + \varepsilon[$ に相当するので、Def (B) では「各 $\varepsilon > 0$ について ${n \in \mathbb{N} : \varphi(n) \notin ]x - \varepsilon, x + \varepsilon[}$ が有限」という条件に書き換えられる。

出典: p.17–18

Def (B) は列の指標集合 $\mathbb{N}$ 上の標準的な順序に言及していない——Def (A) では使われていた。したがって、指標の任意の置換は収束に影響しない。指標集合上の順序は、収束の観点からは無用、少なくとも不要である。よって $\mathbb{N}$ の代わりに任意の無限可算集合 $N$ を指標に取れる（Def (C)）。

出典: p.18

$N$ の cofinite 部分集合は、包含関係と有限交で閉じる。区間 $]x - ε, x + ε[$ は $x$ の（対称な）近傍の特例である。より一般に、$]a, b[\subset V$ なる $a < x < b$ が存在する $V \subset \mathbb{R}$ を $x$ の近傍と呼び、すべての近傍の族を $\mathcal{N}(x)$ と表す。$\mathcal{N}(x)$ は isotone・finitely complete・proper である。 > 出典: p.18–19 $\varphi \in X^N$ に対し $\Gamma_\varphi := {E \subset X : \varphi^{-1}(E) \text{ が } N \text{ 上 cofinite}}$ と定める（(II.1.1)）。$\Gamma_\varphi$ も isotone・finitely complete・proper である。Proposition II.1.1 により、$\varphi$ が $x$ に収束することは $\mathcal{N}(x) \subset \Gamma_\varphi$ と同値である。 > 出典: p.19 本節の到達点は二つある。収束の観点から、列 $\varphi : N \to X$ は指標集合 $N$ 上の順序から解放されるだけでなく、最終的には指標集合そのものからも解放される。奇跡のように見えるが、これは単に適切な視点に過ぎない。ただし cofinite 集合の構造は自然数の自然な順序の残滓である。 > 出典: p.20 ### II.2 The concept of filter 前節で、実数直線上の列の収束が、列に関連する集合族と点に関連する集合族の包含で特徴づけられることを見た。さらにこれらの族は isotone・finitely complete・proper という共通の性質を持つ。 > 出典: p.20–21 この共通性質からフィルター概念が抽出される。近傍族 $\mathcal{N}(x)$ と (II.1.1) で列に付随する族 $\Gamma_\varphi$ は proper filter である。 > 出典: p.21 --- ## II.1. Convergence of Sequences - cards/topology/sequence

II.2. The Concept of Filter

Section titled “II.2. The Concept of Filter”

II.3. Order on Filters

Section titled “II.3. Order on Filters”

II.4. Decomposition into Free and Principal Filters

Section titled “II.4. Decomposition into Free and Principal Filters”

[!IMPORTANT] 規約ブリッジ（本書 ↔ Mathlib） 本書のフィルター順序は族の包含 $\mathcal{F} \subset \mathcal{G}$（大きい族＝finer）。Mathlib Filter は逆順序 f ≤ g ↔ g.sets ⊆ f.sets。対応は:

本書Mathlib
$\mathcal{F} \subset \mathcal{G}$（$\mathcal{G}$ が finer）𝓖 ≤ 𝓕
$\mathcal{F} \wedge \mathcal{G}$（meet=族の共通部分）𝓕 ⊔ 𝓖
$\mathcal{F} \vee \mathcal{G}$（join=生成）𝓕 ⊓ 𝓖
proper（$\emptyset \notin \mathcal{F}$）Filter.NeBot
improper $2^X$（$\emptyset \in \mathcal{F}$）⊥
$\operatorname{ker}\mathcal{F} = \bigcap\mathcal{F}$Filter.ker f
principal $s^\uparrow$𝓟 s

ゆえに本書の $\mathcal{F} = \mathcal{F}^* \wedge \mathcal{F}^\bullet$, $\mathcal{F}^* \vee \mathcal{F}^\bullet = 2^X$ は Mathlib で f = f* ⊔ f•, Disjoint f* f• に翻訳される。

[!NOTE] Theorem II.4.1 (Filter Decomposition Theorem) 任意のフィルター $\mathcal{F}$ は、自由部分 $\mathcal{F}^$ と主部分 $\mathcal{F}^\bullet = (\operatorname{ker}\mathcal{F})^\uparrow$ に一意に分解される: $$\mathcal{F} = \mathcal{F}^ \wedge \mathcal{F}^\bullet, \qquad \mathcal{F}^* \vee \mathcal{F}^\bullet = 2^X$$ ここで $\mathcal{F}^$ は自由（$\operatorname{ker}\mathcal{F}^ = \emptyset$）、$\mathcal{F}^\bullet$ は主。

証明（自然言語）. $K := \operatorname{ker}\mathcal{F}$ とおく。自由部分を基底 ${A \setminus K : A \in \mathcal{F}}$ の生成するフィルター $\mathcal{F}^$、主部分を $\mathcal{F}^\bullet := K^\uparrow$ と定める。Mathlib 順序では $\mathcal{F}^ = \mathcal{F} \sqcap \mathcal{P}(K^c)$、$\mathcal{F}^\bullet = \mathcal{P}(K)$。

  • 自由性: $\operatorname{ker}\mathcal{F}^* = \operatorname{ker}\mathcal{F} \cap K^c = K \cap K^c = \emptyset$。
  • $\mathcal{F}^ \vee \mathcal{F}^\bullet = 2^X$**: $\mathcal{F}^ \sqcap \mathcal{F}^\bullet \le \mathcal{P}(K^c) \sqcap \mathcal{P}(K) = \mathcal{P}(K^c \cap K) = \mathcal{P}(\emptyset) = \bot$、すなわち両者は素。
  • *$\mathcal{F} = \mathcal{F}^ \wedge \mathcal{F}^\bullet$**（Mathlib f = f* ⊔ f•）:
    • ($\ge$ 側) $\mathcal{F}^* \le \mathcal{F}$ かつ $\mathcal{F}^\bullet = \mathcal{P}(K) \le \mathcal{F}$（$K \subseteq$ 各 $A \in \mathcal{F}$）。よって上限 $\le \mathcal{F}$。
    • ($\le$ 側) $S$ が右辺に属するとは $K \subseteq S$ かつ $K \cup S \in \mathcal{F}$。$K \subseteq S$ より $K \cup S = S$ なので $S \in \mathcal{F}$。

一意性: $\mathcal{F}^\bullet$ は核 $K$ から一意に定まり、$\mathcal{F}^*$ も $\mathcal{F}$ と $\mathcal{F}^\bullet$ から一意に定まる。$\blacksquare$

Lean. Notes/ChapterII.lean : RoyalRoad.ChapterII.thm_II_4_1（lake build 済み）

def freePart (f : Filter X) : Filter X := f ⊓ 𝓟 (Filter.ker f)ᶜ
def principalPart (f : Filter X) : Filter X := 𝓟 (Filter.ker f)


theorem decomposition (f : Filter X) : f = freePart f ⊔ principalPart f := by
  unfold freePart principalPart
  apply le_antisymm
  · rw [le_def]
    intro S hS
    rw [mem_sup] at hS
    obtain ⟨hfree, hprin⟩ := hS
    rw [mem_inf_principal', compl_compl] at hfree
    rw [mem_principal] at hprin
    rwa [union_eq_self_of_subset_left hprin] at hfree
  · exact sup_le inf_le_left (gi_principal_ker.gc.l_u_le f)


theorem thm_II_4_1 (f : Filter X) :
    f = freePart f ⊔ principalPart f ∧
      Filter.ker (freePart f) = ∅ ∧
      principalPart f = 𝓟 (Filter.ker f) ∧
      Disjoint (freePart f) (principalPart f) :=
  ⟨decomposition f, freePart_ker f, rfl, freePart_disjoint_principalPart f⟩

II.5. Supplement

Section titled “II.5. Supplement”

章の背骨

Section titled “章の背骨”

[!IMPORTANT] 列 → フィルター → 完備束

  1. 列の収束（Def (A)→(B)→(C)）: 指標の順序は不要；cofinite 集合の構造が残る
  2. $\Gamma_\varphi$ と $\mathcal{N}(x)$（(II.1.1), Prop II.1.1）: 収束 ⟺ $\mathcal{N}(x) \subset \Gamma_\varphi$——族の包含に還元
  3. フィルター公理（II.2）: $\mathcal{N}(x)$ と $\Gamma_\varphi$ の共通性質（isotone, finitely complete）から抽出
  4. 列型フィルター（Def II.2.9）: $\mathcal{F} = \Gamma_\varphi$——列はフィルターに還元されるが、逆は成り立たない（Example II.2.23）
  5. フィルターの順序と完備束（II.3, Prop II.3.2）: $(\overline{\mathbb{F}}X, \subset)$ は complete lattice；proper フィルター全体 $\mathbb{F}X$ は lattice すらならない場合がある
  6. ウルトラフィルター（Def II.3.9）: $\mathbb{F}X$ の極大元；各 proper filter はある ultrafilter に含まれる（Zorn）
  7. 自由部分と主部分（Thm II.4.1）: 任意のフィルター $\mathcal{F} = \mathcal{F}^* \wedge \mathcal{F}^\bullet$ に一意分解

[!NOTE] 本書 ↔ 第III章への橋 第II章は「列が点に収束する」を $\mathcal{N}(x) \subset \Gamma_\varphi$ で特徴づける。第III章ではこの包含を一般化し、任意の proper filter $\mathcal{F}$ が点 $x$ に収束する関係 $x \in \lim \mathcal{F}$ を公理化する。列は反例・具体化の道具として残る（Preface p.vii–viii, 章冒頭 p.17）。

[!NOTE] Def (A)→(B)→(C) はどこで効くか（cards/topology/convergence-of-sequence 参照）

  • (A)→(B)（順序 → cofinite）: $\Gamma_\varphi$（(II.1.1)）を可能にし、$\mathcal{N}(x)$ と $\Gamma_\varphi$ の共通性質から II.2節のフィルター公理が抽出される。(B) なしにフィルター概念は生まれない。
  • (B)→(C)（$\mathbb{N}$ 固定 → 任意の無限可算集合）は3か所で具体的に必須になる：
    1. 部分列（Prop II.1.3）: 単調写像でなく、異なる可算集合間の単射 $\gamma \in N^K$ で定義できる。
    2. 列型フィルター（Def II.2.9, cards/topology/sequential-filter）: $\mathcal{F} = \Gamma_\varphi$ の $\varphi \in X^N$ は $N$ を固定しないからこそ、指標の付け替えで生成される同じフィルターを同一視できる。
    3. Example II.2.18/II.5.11（cards/topology/partition-tail-filter）: 可算個の無限集合の非交和自体を新たな指標集合に使う。
  • 第III章 cards/topology/standard-sequential-convergence（$\sigma_\mathbb{R}$）の $\varphi[(\mathbb{N})0] \subset \mathcal{F}$ は $\Gamma\varphi \subset \mathcal{F}$——Prop II.1.1 の「収束＝フィルター包含」を任意のフィルターへ一般化した形での再利用。