Skip to content
Journals Garden

Royal Road to Topology Chapter I

Chapter I. Preliminaries

Section titled “Chapter I. Preliminaries”

This chapter outlines the basic set-theoretic concepts, relations, maps, orders, polarities, and cardinalities assumed throughout.

I.1. Relations and Maps

Section titled “I.1. Relations and Maps”

Basic Notations

Section titled “Basic Notations”

Relations

Section titled “Relations”

[!NOTE] Proposition I.1.1 For $R \subset X \times Y$, $A \subset X$, and $B \subset Y$, the following statements are equivalent:

  1. $RA \cap B \neq \emptyset$
  2. $A \cap R^- B \neq \emptyset$
  3. $R \cap (A \times B) \neq \emptyset$

📇 cards/topology/prop-i-1-1 証明（自然言語）. いずれの条件も「ある $x \in A$ と $y \in B$ が存在して $(x, y) \in R$」という同一の主張を、像・逆像・直積のどの側から述べるかの違いにすぎない。実際:

  • $(1) \Rightarrow (2)$: $y \in RA \cap B$ をとると、$y \in RA$ より $x \in A$ で $(x,y) \in R$ が、$y \in B$ も成り立つ。よって $x \in A$ かつ $x \in R^- B$、すなわち $x \in A \cap R^- B$。
  • $(2) \Rightarrow (3)$: $x \in A \cap R^- B$ をとると $x \in A$ かつ $(x, y) \in R$ なる $y \in B$ がある。ゆえに $(x, y) \in R \cap (A \times B)$。
  • $(3) \Rightarrow (1)$: $(x, y) \in R \cap (A \times B)$ をとると $y \in RA$（$x \in A$ が証人）かつ $y \in B$。ゆえに $y \in RA \cap B$。

Lean. Notes/ChapterI.lean : RoyalRoad.ChapterI.prop_I_1_1（lake build 済み）

theorem prop_I_1_1 (R : Set (X × Y)) (A : Set X) (B : Set Y) :
    [ (relImage R A ∩ B).Nonempty,
      (A ∩ relPreimage R B).Nonempty,
      (R ∩ A ×ˢ B).Nonempty ].TFAE := by
  tfae_have 1 → 2 := by
    rintro ⟨y, ⟨x, hxA, hR⟩, hyB⟩
    exact ⟨x, hxA, y, hyB, hR⟩
  tfae_have 2 → 3 := by
    rintro ⟨x, hxA, y, hyB, hR⟩
    exact ⟨(x, y), hR, hxA, hyB⟩
  tfae_have 3 → 1 := by
    rintro ⟨⟨x, y⟩, hR, hxA, hyB⟩
    exact ⟨y, ⟨x, hxA, hR⟩, hyB⟩
  tfae_finish

Maps (Functions)

Section titled “Maps (Functions)”

[!NOTE] Proposition I.1.2 A relation $F \subset X \times Y$ is a graph if and only if $F^-Y = X$ and $F^-y_0 \cap F^-y_1 \neq \emptyset \implies y_0 = y_1$.

📇 cards/topology/prop-i-1-2 証明（自然言語）. $F$ がグラフであるとは、各 $x \in X$ にちょうど一つの $y$ で $(x, y) \in F$ となるもの（存在性 + 一意性）が対応すること。

  • ($\Rightarrow$) 存在性から各 $x$ にある $y$ で $(x, y) \in F$、ゆえに $x \in F^- Y$。よって $F^- Y = X$。一意性から、$x \in F^- y_0 \cap F^- y_1$ なら $(x, y_0), (x, y_1) \in F$ より $y_0 = y_1$。
  • ($\Leftarrow$) $F^- Y = X$ より各 $x$ に少なくとも一つの $y$ が対応（存在性）。一価性条件から二つ対応すれば一致（一意性）。ゆえにグラフ。

Lean. Notes/ChapterI.lean : RoyalRoad.ChapterI.prop_I_1_2（全域性 relPreimage F univ = univ、一価性で定式化。IsGraph F := ∀ x, ∃! y, (x, y) ∈ F）

[!NOTE] Corollary I.1.6 A relation $F \subset X \times Y$ is a graph if and only if its inverse relation $F^-$ is surjective and injective.

📇 cards/topology/cor-i-1-6 証明（自然言語）. Proposition I.1.2 の二条件を逆関係 $F^-$ の言葉に翻訳するだけ。$F^-$ の全射性 $F^- Y = X$ は全域性そのもの。$F^-$ の単射性 $F^- y_0 \cap F^- y_1 \neq \emptyset \implies y_0 = y_1$ は一価性そのもの。よって I.1.2 と同値。

Lean. Notes/ChapterI.lean : RoyalRoad.ChapterI.cor_I_1_6（relImage (relInv F) univ = relPreimage F univ などの翻訳補題を経て prop_I_1_2 に帰着）

I.2. Equivalence Relations

Section titled “I.2. Equivalence Relations”

[!NOTE] Proposition I.2.1 There exists a bijection between equivalence relations on a non-empty set $X$ and surjective maps defined on $X$.

📇 cards/topology/prop-i-2-1 証明（自然言語）. 対応を両方向に構成して互いに逆であることを示す。

  • 同値関係 $\sim$ には標準全射 $X \to X/{\sim}$（$x \mapsto [x]$）を対応させる。
  • 全射 $f : X \to Y$ には核 $\ker f := {(a, b) : f(a) = f(b)}$（同値関係）を対応させる。

標準全射の核はもとの $\sim$ に一致し（$[a] = [b] \iff a \sim b$）、逆に全射 $f$ の核による商 $X/\ker f$ は $f$ の像（全射なので $Y$）と全単射 $[x] \mapsto f(x)$ で一致する。よって（全射を終域の付け替えで同一視すれば）両者は全単射に対応する。

Lean. Notes/ChapterI.lean : RoyalRoad.ChapterI.prop_I_2_1_ker_mk（Setoid.ker (Quotient.mk r) = r）と prop_I_2_1_quotientEquiv（Quotient (Setoid.ker f) ≃ Y、Mathlib Setoid.quotientKerEquivOfSurjective）で対応の両輪を形式化。

I.3. Order

Section titled “I.3. Order”

[!NOTE] Proposition I.3.8 An order isomorphism $f$ preserves extrema: $$f\left(\bigvee A\right) = \bigvee f(A), \quad f\left(\bigwedge A\right) = \bigwedge f(A)$$

📇 cards/topology/prop-i-3-8 証明（自然言語）. $\bigvee A$ について示す（$\bigwedge$ は双対）。$s = \bigvee A$ は $A$ の上界の最小元。$f$ は順序同型なので、$x$ が $A$ の上界 $\iff$ $f(x)$ が $f(A)$ の上界（$a \le x \iff f(a) \le f(x)$）。順序同型は順序を保つ全単射ゆえ「最小の上界」を「最小の上界」に写す。したがって $f(s)$ は $f(A)$ の上限、すなわち $f(\bigvee A) = \bigvee f(A)$。

Lean. Notes/ChapterI.lean : RoyalRoad.ChapterI.prop_I_3_8_sSup / prop_I_3_8_sInf（完備束上で OrderIso.map_sSup / map_sInf を再利用。e (sSup A) = sSup (e '' A)）

I.4. Polarities

Section titled “I.4. Polarities”

[!NOTE] Proposition I.4.2 For $R \subset X \times Y$, $A \subset X$, and $B \subset Y$, the following are equivalent:

  1. $R^\circ A \supset B$
  2. $A \subset R^{-\circ} B$
  3. $A \times B \subset R$

📇 cards/topology/prop-i-4-2 証明（自然言語）. $R^\circ A = {y : \forall x \in A,\ (x, y) \in R}$、$R^{-\circ} B = {x : \forall y \in B,\ (x, y) \in R}$。三条件はいずれも「$\forall x \in A,\ \forall y \in B,\ (x, y) \in R$」の言い換え:

  • (1) $B \subset R^\circ A$: $\forall y \in B,\ \forall x \in A,\ (x, y) \in R$。
  • (2) $A \subset R^{-\circ} B$: $\forall x \in A,\ \forall y \in B,\ (x, y) \in R$。
  • (3) $A \times B \subset R$: $\forall (x, y) \in A \times B,\ (x, y) \in R$。

全称の順序を入れ替えるだけで互いに同値。

Lean. Notes/ChapterI.lean : RoyalRoad.ChapterI.prop_I_4_2（polar, polarInv を定義し TFAE で）

[!NOTE] Proposition I.4.1 The pair $(R^\circ, R^{-\circ})$ is an inverse order isomorphism (with respect to $\subset$) between $R$-bipolars and $R^-$-bipolars.

📇 cards/topology/prop-i-4-1 証明（自然言語）. I.4.2 の (1)$\iff$(2) は随伴 $B \subset R^\circ A \iff A \subset R^{-\circ} B$、すなわち $(R^\circ, R^{-\circ})$ が反変ガロア接続をなすこと。一般のガロア接続論から、双極作用素 $A \mapsto R^{\circ\circ} A := R^{-\circ}(R^\circ A)$ は閉包作用素となる。実際:

  • 拡大性 $A \subset R^{\circ\circ} A$、
  • 単調性 $A_0 \subset A_1 \implies R^{\circ\circ} A_0 \subset R^{\circ\circ} A_1$、
  • 冪等性 $R^{\circ\circ}(R^{\circ\circ} A) = R^{\circ\circ} A$。

閉包で固定される集合（=双極）の上では $R^\circ$ と $R^{-\circ}$ は互いに逆の反変全単射となり、$R$-双極と $R^-$-双極の間の逆順序同型を与える。

Lean. Notes/ChapterI.lean : RoyalRoad.ChapterI.prop_I_4_1_adjunction（随伴）, bipolar_extensive / bipolar_mono / bipolar_idem（閉包作用素の三性質）, polar_antitone。

I.5. Finite and Infinite Cardinals

Section titled “I.5. Finite and Infinite Cardinals”

[!NOTE] Proposition I.5.3 A set $X$ is countable if and only if it is either finite and non-empty, or $\text{card } X = \aleph_0$.

📇 cards/topology/prop-i-5-3 証明（自然言語）. 本書の「可算」は「$\mathbb{N}$ の像」、すなわち全射 $\mathbb{N} \to X$ が存在すること（像は空でない）。

  • ($\Rightarrow$) 全射 $f : \mathbb{N} \to X$ があれば $X$ は空でなく可算濃度。$X$ が有限なら「有限かつ空でない」。無限なら可算無限ゆえ $X \simeq \mathbb{N}$、すなわち $\text{card } X = \aleph_0$。
  • ($\Leftarrow$) 有限かつ空でなければ要素を有限列に並べ、最後の要素で埋めて $\mathbb{N}$ から全射が作れる。$X \simeq \mathbb{N}$ ならその全単射（の逆）が全射を与える。

Lean. Notes/ChapterI.lean : RoyalRoad.ChapterI.prop_I_5_3（(∃ f : ℕ → X, Surjective f) ↔ ((Finite X ∧ Nonempty X) ∨ Nonempty (X ≃ ℕ))。finite_or_infinite、nonempty_denumerable_iff、countable_iff_exists_surjective を利用）

[!NOTE] Proposition I.5.4 & Corollary I.5.6

  • The countable union of countable sets is countable.
  • The product of two countable sets is countable.
  • Consequently, the set of rational numbers $\mathbb{Q}$ is countable.

📇 cards/topology/prop-i-5-4 証明（自然言語）.

  • 可算和: 添字集合が可算で各 $s_i$ が可算なら、$\mathbb{N} \times \mathbb{N}$ が可算（対関数）であることから $\bigcup_i s_i$ も $\mathbb{N}$ の像として可算。
  • 積: $s, t$ が可算なら $s \times t$ は $\mathbb{N} \times \mathbb{N}$ の像として可算。
  • 系: $\mathbb{Q}$ は各 $n$ に対する ${m/n : m \in \mathbb{Z}}$（可算）の可算和なので可算。

Lean. Notes/ChapterI.lean : RoyalRoad.ChapterI.prop_I_5_4_iUnion（Set.countable_iUnion）, cor_I_5_6_prod（Set.Countable.prod）, cor_I_5_6_rat（ℚ の可算インスタンス + Set.countable_univ）

[!NOTE] Theorem I.5.8 (Cantor) For every set $X$: $$\text{card } X < \text{card } 2^X$$

📇 cards/topology/thm-i-5-8-cantor 証明（自然言語）. $\text{card } X \le \text{card } 2^X$ は $x \mapsto {x}$ が単射より明らか。等号不成立を背理法で示す。全射 $g : X \to 2^X$ があると仮定し、対角集合 $D := {x \in X : x \notin g(x)}$ をとる。全射性より $D = g(x_0)$ なる $x_0$ がある。すると $x_0 \in D \iff x_0 \notin g(x_0) = D$ となり矛盾。ゆえに全射は存在せず、$\text{card } X < \text{card } 2^X$。

Lean. Notes/ChapterI.lean : RoyalRoad.ChapterI.thm_I_5_8_cantor（Cardinal.mk X < Cardinal.mk (Set X)。Cardinal.mk_set で $2^{#X}$ に直し Cardinal.cantor を適用）