2026-07-03 学習ログ

Royal Road to Topology 第IV章「Continuity」を一括カード化した日。これで必須ロードマップ II–IV のカード化が完了。

やったこと

• カード化: 41 枚（20_Literature/royal_road_to_topology/chapter4、索引 royal-road-to-topology-Flashcards）
  • IV.1 像と逆像 4（随伴 📐IV.1.1–2）/ IV.2 連続写像 7（ε-δ の回復、同相、📐IV.2.6 列連続性）
  • IV.3 連続性と順序 7（始収束・終収束・商・部分収束・埋め込み、📐IV.3.5 随伴公式）
  • IV.4 始収束（族）4 / IV.5 積と選択 3 / IV.6 積収束 6（Cantor cube、各点収束、polyhedral filter）
  • IV.7 対角積 3（グラフ同相 📐IV.7.10）/ IV.8 終収束・余積 2 / IV.9 下半連続 2（選択原理）/ IV.10 補遺 3
• 進捗トラッカー更新: IV カード化 ✅（41枚）。次のカード化対象を第VII章 Topological Structures に設定。

気づき / 詰まり

• 章の背骨は随伴公式 (IV.3.5): $f\xi \geq \tau \iff f \in C(\xi,\tau) \iff \xi \geq f^-\tau$。著者自身が “very, very useful formula!” と強調。始収束・終収束・積・商・埋め込みが全部この一本から出る。Mathlib の gc_coinduced_induced と Filter.map ⊣ comap にそのまま対応。
• 連続性は列で判定できない（IV.2.7: $\nu_\mathbb{R}$ と $\sigma_\mathbb{R}$ は列上一致）が、距離化可能なら列で十分（IV.2.6）——「なぜ測度論で第一可算性・距離化可能性を気にするのか」の根拠。
• polyhedral filter = 積フィルター（IV.6.5）は測度論の筒集合（cylinder sets）の位相版。Kolmogorov 拡張定理の舞台の原型として明示的にリンクした。

明日の最初の一手

• 第III・IV章をカードで確認しながら読む（読了列はまだ ⬜）。
• もしくは第VII章 Topological Structures のカード化に着手（第V・VI章は辞書式参照）。

追記: 第I・II章カード化の監査と完了（issue #1 / Phase A）

• 監査: chp1・chp2 PDF を pdftotext -raw で全数列挙し、索引 I.1–I.5 / II.1–II.5 と突き合わせ。前セッションの未コミット成果（カード 35 枚＋章ノート更新）を PDF 原文と照合して取り込み確認。
• 追加カード 3 枚（監査で判明した残ギャップ）:
  • 📐 cards/topology/cor-ii-2-12（列型 ⟹ 可算集合を含む、$\mathbb{S} \subset \mathbb{E}$）
  • cards/topology/partition-tail-filter（Examples II.2.18/II.5.11: countably carried だが列型でも subcofinite でもない反例構成）
  • cards/topology/cofinite-filters-inf-sup（Example II.3.1: $(B_i)_0$ の inf/sup 公式）
• 索引 royal-road-to-topology-Flashcards に I・II 章の未掲載カード 38 枚を全登録。order カードの source-note を chapter1 に修正、filter-decomposition-theorem に 📐 を付与。
• 整合性チェック通過: カードファイル 213 = 索引エントリ 213（重複なし）、章ノートのリンク先も全存在。第I章 69 枚 / 第II章 53 枚。
• 進捗トラッカー更新: I・II カード化 ✅、Lean 列を実態（I: ChapterI.lean 27項目 🟡 / II: ChapterII.lean 7項目 🟡）に修正。
• カード化しなかった項目（確認リスト）: Remark II.2.11（記法の慣習—sequence カードで既出）、Exercises II.5.2–II.5.5・II.5.7（演習—手筋化は任意タスク）、Example II.5.1（II.5.2 に吸収）。

追記: 第I〜IV章の演習選別と解答（issues #2 #3 / Phase B+C）

• 演習選別（Phase B）: LADR 方式（⭐＝測度論的確率統計に効く問題）で 20 問を選別。
  • 第I章は演習節がないため本文の証明省略命題から 6 問（Prop I.1.2 / Rem I.1.3 / Prop I.2.1 / Prop I.3.8⭐ / Prop I.4.2 / Cor I.5.6⭐）
  • 第II章 II.5.2–II.5.5, II.5.7（5問）／ 第III章 III.7.1–III.7.5（5問）／ 第IV章 IV.10.4, IV.10.8, IV.10.9, IV.10.13（4問）
• 解答（Phase C）: 全 20 問を「方針 → 詳細」形式で解決 ✅。書籍未解答の III.7.5（3距離の挟み込み $t \leq d \leq s \leq m \cdot t$）と IV.10.9（円周 $\rho$ と区間 $\mu$ の非同相）も含む。
• IV.10.9 は連結性（XIII章）不使用の縛りがポイント: sup による中間値定理の自前証明＋「円周では中間値が 2 つの弧で 2 回実現される」counting 論法で単射性と矛盾させた。
• technique カード 5 枚（索引 royal-road-to-topology-Flashcards に登録、計 218 枚で整合性チェック通過）:
  • cards/topology/technique-witness-selection（対角選択・証人選択—II.5.3/II.5.4/III.7.1/III.7.4 で計 4 回登場）
  • cards/topology/technique-mod-finite（有限修正不変。a.e. 同値類の組合せ論的原型）
  • cards/topology/technique-metric-equivalence（定数倍挟み込み ⇒ 同一収束）
  • cards/topology/technique-galois-adjunction（随伴で extrema を運ぶ—I.3.8/I.4.2/IV.10.8/IV.10.13 を貫く）
  • cards/topology/technique-intermediate-value（sup による IVT＋中間値の個数不変量）
• 進捗トラッカー更新: 演習列 I–IV ✅、カード数 II=55 / III=51 / IV=43。

気づき（演習から）

• 対角選択（witness selection）が第II・III章の Supplement を貫く背骨だった。可算基 → 収束列が作れる、という第一可算性の実利が体感できる。
• II.5.5（cocountable は可算交叉で閉じる）は「a.s. 事象は可算個の共通部分で閉じる」そのもの。IV.10.11 で早速使われており、測度論への伏線が明示的。
• 随伴公式 (IV.3.5) は演習でも主役: IV.10.8 の 4 等式は全部「支配する対象の一致」の一行芸に潰れる。弱位相・積 σ-代数の計算規則の原型。

追記: 第VII章 Topological Structures のカード化（issue #4 / Phase D-1）

• chp7-2024-topological-structures.pdf を pdftotext -raw で全文抽出・読解。
• カード 28 枚（20_Literature/royal_road_to_topology/chapter7 を新規作成、索引 royal-road-to-topology-Flashcards に登録）:
  • VII.1 閉集合・閉包 5（Kuratowski 公理 📐、adherence 冪等 ⟺ cl=adh 📐）
  • VII.2 開集合・内部・近傍 5（Sorgenfrey の開閉集合例、(VII.2.8) 近傍の入れ子条件 📐）
  • VII.3 位相 7（位相の定義、$\lim$ の閉集合表示 📐、連続性の開閉集合特徴づけ 📐、連続性5同値条件 📐、prime pretopology は位相 📐）
  • VII.4 位相クラスの構造 5（topologizer $T$、radial topology、$T$ の非可換性＝Arens topology、完備束 📐、free 保存 📐）
  • VII.5 Sierpiński 位相 2（initially dense 定理 📐、Sierpiński 立方体への埋め込み）
  • VII.6 ネット（*節） 2（フィルターへの帰着、subnet）
  • VII.7 補遺 2（古典的定義との同値性、pointwise property）
• 前提の第V章 Families of Sets（grill 1枚）・第VI章 Pretopologies（adherence/inherence/pretopologizer/Bourdaud 前位相など 9枚）はルール通り最小の辞書カードのみ作成し、スタブ章ノート chapter5.md・chapter6.md（カードリストのみ）を新規作成。_home.md に3章分のリンクを追加。
• 進捗トラッカー更新: VII カード化 ✅（28枚）、V・VI 🟡（辞書分のみ、1枚/9枚）。次のカード化対象を第VIII章に設定。
• 整合性チェック: カードファイル総数 256 = 索引エントリ数一致、リンク先ファイルすべて存在。

気づき（第VII章）

• 章の核心は一行: 「位相 = adherence が冪等な前位相」。この冪等性一つから $\operatorname{adh}=\operatorname{cl}$（Cor VII.1.8）、Kuratowski 閉包公理の完全成立、$\lim_\theta \mathcal{F} = \bigcap \operatorname{cl}_\theta A$（近傍フィルターによる古典的収束）が芋づる式に出る。
• pretopologizer $S_0$ と topologizer $T$ の非対称性が地味だが重要: $S_0$ は始収束・積と完全に可換（Thm VI.6.3）だが、$T$ は可換しない（Arens topology の反例、Example VII.4.6）。「位相のクラスが扱いにくい」という本書冒頭の主張が、この一つの定理の欠如に集約されている。
• Sierpiński 位相が位相クラスで initially dense（Thm VII.5.2）という事実は、Bourdaud 前位相が前位相クラスで initially dense（Cor VI.7.5, 第VI章）の直接の類似物。2点・3点の極小試験空間へ埋め込むことで任意の構造を復元できる、という発想が本書全体で繰り返される。
• ネット（VII.6, *節）はフィルターに完全に帰着する（Prop VII.6.3-6.4）ため、Mathlib が Filter.Tendsto を基本に据えている設計判断とも一致。深追い不要と判断し2枚に留めた。

追記: 第VIII章 Adherences, Covers and Compactness のカード化（issue #5 / Phase D-2）

• chp8-2024-adherences-covers-and-compactness.pdf（13p）を pdftotext -raw で全文抽出・読解。
• カード 31 枚（20_Literature/royal_road_to_topology/chapter8 を新規作成、索引 royal-road-to-topology-Flashcards に登録）:
  • VIII.1 族の adherence 8（超フィルターへの帰着 📐、Hausdorff⟹adh=lim 📐＋Sierpiński反例、円周の反例＝族の adherence は元の交叉の adherence より真に大きい）
  • VIII.2 被覆・inherence 7（$\xi$-cover の3同値表現 📐、細分は被覆を保つ 📐、位相での開被覆との同値性、pseudocover）
  • VIII.3 コンパクト収束 13（Heine–Borel 📐、連続写像はコンパクト性を保つ 📐、Tikhonov の定理 📐、有限部分被覆による古典的特徴づけ 📐、閉部分集合の継承（分離公理不要）📐 と Hausdorff での逆（コンパクト⟹閉）📐 の非対称性、countably compact・Lindelöf）
  • VIII.4 補遺 3（free収束での列の adherence 公式 📐、$1/x$ のグラフ閉/不連続の反例）
• 前提の第V章 Families of Sets に refines relation（$\mathcal{R}\triangleleft\mathcal{P}$）の辞書カード1枚を追加（V章計2枚）。第VI章は本章では追加なし。
• 進捗トラッカー更新: VIII カード化 ✅（31枚）、V 🟡（辞書2枚）。次のカード化対象を第IX章に設定。
• 整合性チェック: カードファイル総数 288 = 索引エントリ数一致、リンク先ファイルすべて存在。

気づき（第VIII章）

• 章全体が一本の道筋: 「族の adherence」（VIII.1）→「被覆はadherence/inherenceの言い換え」（VIII.2, Lemma VIII.2.3 が要）→「コンパクト＝全フィルターが adherent」（VIII.3）→ 位相に特殊化すると「開被覆は有限部分被覆を持つ」という古典的定義そのものが定理として出てくる（Cor VIII.3.8）。抽象的な集合演算子の言葉で組み立てた定義が、最後に馴染みの形に「戻ってくる」構成がこの章の見せ場。
• Tikhonov の定理の証明が圧倒的に短い: 超フィルターの押し出し $p_i[\mathcal{U}]$ が各成分で収束点を持つことを選ぶだけ（選択公理は「超フィルターの存在」に既に押し込まれている）。古典的な証明（有限交叉性質の議論）より本書のフィルター言語の方が簡潔になる好例として明示的に強調されていた。
• コンパクト⟹閉の非対称性が印象的: 閉部分集合がコンパクト性を継承する方向は分離公理なしで成り立つ（Prop VIII.3.14）が、逆向き（コンパクト⟹閉）は Hausdorff 性が本質的に必要（Prop VIII.3.16、反例 Sierpiński 位相の ${0}$）。「なぜコンパクト・ハウスドルフ空間が位相空間論で特別扱いされるか」の技術的理由がここに集約されている。
• 測度論への伏線: 二分法による Heine–Borel の証明・超フィルターの押し出しによる Tikhonov の証明は、どちらも Kolmogorov 拡張定理や Prokhorov の定理（測度の緊密性）の位相的土台に直結する。

追記: 第IX章 Topological Concepts のカード化（issue #6 / Phase D-3）

• chp9-2024-topological-concepts.pdf（27p、章中最大）を pdftotext -raw で全文抽出・読解。
• カード 37 枚（20_Literature/royal_road_to_topology/chapter9 を新規作成、索引 royal-road-to-topology-Flashcards に登録）:
  • IX.1 分離公理 12（Hausdorff⟺対角閉 📐、正則・正規の近傍フィルターによる特徴づけ 📐、Niemytzki平面＝Hausdorff・正則だが非正規の古典反例、Sierpiński位相＝正規だが非正則、hereditarily normal の3同値 📐）
  • IX.2 基底 6（base の内在的判定 📐、weight・second countable、density≤weight 📐 と距離化可能なら等号、Sorgenfrey線の weight=$\mathfrak{c}$＝距離化不可能性の実例）
  • IX.3 コンパクト性の位相版 8（Hausdorff+compact⟹正則+正規 📐、線形順序位相のコンパクト性⟺完備束 📐、Sorgenfrey線のコンパクト集合は可算、辞書式順序の単位正方形＝コンパクトだが非可分）
  • IX.4 写像の型 5（topologically quotient map、開写像/閉写像⟹quotient 📐、円の被覆写像による開閉の非対称例、perfect map 📐）
  • IX.5 補遺 6（Sierpiński立方体への埋め込み次元 📐、グラフの閉性 📐、FIP・Cantor条件によるコンパクト性の別表現 📐、dense/nowhere dense/meager/residual、pretopologically/topologically Hausdorff の非対称反例2連発）
• Thm IX.5.16（point-finite 被覆の縮小補題）・Lemma IX.5.17 は paracompactness 準備の発展的（*付き）定理のためカード化を見送り、章ノートに明記。
• 進捗トラッカー更新: IX カード化 ✅（37枚）。次のカード化対象を第X章に設定。
• 整合性チェック: カードファイル総数 325 = 索引エントリ数一致、リンク先ファイルすべて存在。

気づき（第IX章）

• 分離公理の階層（$T_0\prec T_1\prec T_2\prec T_3\prec T_4$）はどちらの方向にも一方通行であることが2つの反例で鮮やかに示される: Niemytzki 平面は Hausdorff・正則だが非正規（正則から正規は出ない）、Sierpiński 位相は正規だが非正則（正規から正則は $T_1$ なしでは出ない）。「normal + free ⟹ regular」という条件付きの含意（$T_1$ が要）が両反例の橋渡しになっている。
• コンパクト・ハウスドルフ空間が『無料で』正則・正規を手に入れる（Prop IX.3.3/3.4）という事実の証明が、どちらも「Hausdorff性による点ごとの分離 → コンパクト性による有限本への圧縮」という同一パターンの繰り返しだった。コンパクト性の本質的な効能がここに集約されている。
• Sorgenfrey 線が「zero-dimensional・可算稠密・可算指標」なのに「weight = $\mathfrak{c}$」という非対称性（density < weight）を示すことで、cards/topology/density-weight-inequality（距離化可能なら density=weight）の逆が距離化不可能な空間で本質的に破れることが具体的にわかった。これが Sorgenfrey 線が距離化不可能であることの直接証明になっている。
• Cantor 条件（減少閉集合列の交わり非空 ⟺ 可算コンパクト）と FIP（有限交叉性質 ⟺ コンパクト）は、開被覆・超フィルターに次ぐ3つ目・4つ目の同値な顔としてコンパクト性を特徴づける。すべて「ド・モルガンの法則で双対化するだけ」という統一的な導出パターンが心地よかった。

追記: 第X章 Functional Study of Topologies のカード化（issue #7 / Phase D-4、重要ロードマップ VII–X 完了）

• chp10-2024-functional-study-of-topologies.pdf（47p、全章中最大）を pdftotext -raw で全文抽出・読解。
• カード 38 枚（20_Literature/royal_road_to_topology/chapter10 を新規作成、索引 royal-road-to-topology-Flashcards に登録）:
  • X.1–X.2 下・上収束、半連続関数、同程度連続族 3
  • X.3 距離・距離化可能位相の詳細 5（可算積の距離化可能性、Baire 空間、一様収束の距離化可能性、全有界⟺可算コンパクト位相ではコンパクトと一致）
  • X.4 完備距離化可能位相 6（Cauchy フィルター、完備性の4同値条件、Cantor の定理、ベールのカテゴリー定理、$G_\delta/F_\sigma$、$\mathbb{Q}$の非完備距離化可能性）
  • X.5 完備化 2（Hausdorff の完備化定理、一様連続写像の稠密部分からの延長）
  • X.6 関数的閉・開集合 2
  • X.7 関数的分離 10（Urysohnの補題、Tietze拡張定理、perfectly normal と Vedenisov の定理、Niemytzki平面型の反例、Sorgenfrey平面の非正規性、分離公理の対応表）
  • X.8（*付き）Hausdorff・正則だが連続関数が定数のみの反例 1（骨子のみ）
  • X.9 関数的始収束 4（関数的正則性=関数的始収束=擬距離化可能性の三位一体、Tikhonov立方体への埋め込み、Urysohnの距離化定理）
  • X.10 補遺 5（Dini の定理、Stone–Weierstraßの定理、可算稠密線形順序の一意性）
• 進捗トラッカー更新: X カード化 ✅（38枚）。これで重要ロードマップ VII–X（標準位相の舞台）が完了。次のカード化対象は 🎯本命 XII・XV・XXII・XXIV（guide.md 参照）。
• 整合性チェック: カードファイル総数 363 = 索引エントリ数一致、リンク先ファイルすべて存在。

気づき（第X章）

• 章全体が1つの定理に収束する構成だった: 「関数的正則性 = 関数的始収束 = 擬距離化可能性」（Thm X.9.5, Prop X.9.7）。位相的な分離公理（正則・正規）が「開集合の存在」という定性的な話なのに対し、関数的分離公理は「連続関数という道具で位相そのものを復元できる」という定量的・構成的な主張になっている。
• Urysohnの補題とTietze拡張定理が同じ「幾何級数で誤差を縮める」技法（$\tfrac13,\tfrac23$ の分割 → $(\tfrac23)^n$ 減衰）を核にしていることが、証明を読んで初めて明示的に繋がった。関数的閉集合の可算交叉の補題（Lemma X.6.3, X.6.4）が両方の証明のエンジンとして再利用されている。
• 位相的分離と関数的分離は独立という事実が、2段階の反例（Example X.7.7 の「Hausdorff・正則だが関数的正則でない」、Theorem X.8.5 の「連続関数が定数のみ」という極限まで推し進めた反例）で徹底的に示される。これは測度論で「なぜ完全正則性（Tychonoff空間）が可測構造の議論で重視されるか」の直接の答えになっている。
• Dini の定理が Cantor 条件（第IX章の補遺）一つから一行で従う構成が美しかった。単調収束定理・優収束定理といった測度論の収束定理群の位相的な原型がここにある実感があった。

追記: 第III・IV章の Lean 形式化（issue #8 / Phase E、必須ロードマップ I–IV 完了）

• refs/math/topology/royal-road-to-topology/lean/（サブモジュール）に Notes/ChapterIII.lean・Notes/ChapterIV.lean を新規作成。Notes.lean に import 追加。
• ChapterIII.lean: ConvergenceSpace X 構造体を自作（Lim : Filter X → Set X、isotone・centered 公理は Filter.NeBot（proper filter）を instance-implicit で要求）。離散収束 discrete・混沌収束 chaotic、IsFiner（本書の ≥）、IsPretopology・近傍系フィルター vicinityFilter（sSup で構成）、prop_III_1_11（前位相 ⟺ 各点が自分の近傍系フィルターに収束）、prop_III_3_2（離散が最も finer、混沌が最も coarser）を証明。
• ChapterIV.lean: Continuous（連続写像）、initialConv（始収束 $f^-\tau$、公式 (IV.3.1) を直接定義）、finalConv（終収束 $f\xi$、全射性を仮定せず「$f$ を連続にする収束すべての交わり」として一般に構成）、prop_IV_3_5（随伴公式 $f\xi\geq\tau \iff f\in C(\xi,\tau) \iff \xi\geq f^-\tau$ を TFAE で証明）。
• lake exe cache get でキャッシュ取得（既に完備、ダウンロード不要）、lake build をエラーゼロで完走（既存 ChapterI・II も含め全体ビルド確認）。
• カード7枚（convergence・discrete-convergence・chaotic-convergence・continuous-map・initial-convergence・final-convergence・pretopology）と prop-iii-1-11・prop-iii-3-2 の ## Lean 欄にポインタを追記。随伴公式には専用カードが無かったため新規 prop-iv-3-5 を作成（索引・chapter4.md にも登録）。
• 進捗トラッカー更新: III・IV の Lean 列を 🟡 に更新。これで必須ロードマップ I–IV が完全に完了。

気づき（Lean 形式化）

• 本書の「proper filter のみを収束の対象にする」という制約が、Mathlib の Filter X（improper ⊥ を含む一般の完備束）とズレる箇所だった。Lim 自体は全フィルター上で定義される全域関数にしつつ、公理（isotone）だけ両側に [Filter.NeBot] を instance-implicit で要求する設計にしたことで、⊥ での挙動を公理から自由にしつつ本書に忠実な形式化ができた。
• 離散収束の isotone 証明（{y} ∈ p かつ p proper なら p = pure y）が「principal ultrafilter は proper filter の中で atom（極小元）」という事実の直接証明になっており、集合論的直感（${y}\cap s=\emptyset$ なら $\emptyset\in p$ で矛盾）がそのまま Lean の証明項になった。
• 終収束 $f\xi$ を本書の explicit な公式（全射の場合のみ）でなく「$f$ を連続にする収束すべての交わり」として一般的に構成したことで、非全射の場合分けを一切書かずに随伴公式が証明できた。抽象的な universal property による定義が、具体的な場合分けよりも形式化を大幅に単純化する好例だった。