Skip to content
Journals Garden

Convergence / Preconvergence (収束構造 / 前収束) (Section III.1)

  • Convergence / Preconvergence (収束構造 / 前収束) (Section III.1) #Card
    • Let $X \neq \emptyset$ and $\xi \subset \mathbb{F}X \times X$ a relation between (proper) filters on $X$ and points. $x$ is a $\xi$-limit of $\mathcal{F}$, written $x \in \lim_\xi \mathcal{F}$, if $(\mathcal{F}, x) \in \xi$. $\xi$ is a preconvergence if (isotone): $\mathcal{F}_0 \subset \mathcal{F}1 \implies \lim\xi \mathcal{F}0 \subset \lim\xi \mathcal{F}1$. A preconvergence is a convergence if (centered): $x \in \lim\xi x^\uparrow$ for each $x \in X$.

Back

Section titled “Back”

Let $X \neq \emptyset$ and $\xi \subset \mathbb{F}X \times X$ a relation between (proper) filters on $X$ and points. $x$ is a $\xi$-limit of $\mathcal{F}$ (or $\mathcal{F}$ converges to $x$ in $\xi$), written $x \in \lim_\xi \mathcal{F}$, if $(\mathcal{F}, x) \in \xi$.

  • (isotone): $\mathcal{F}_0 \subset \mathcal{F}1 \implies \lim\xi \mathcal{F}0 \subset \lim\xi \mathcal{F}_1$ — a relation with this property is a preconvergence.
  • (centered): $x \in \lim_\xi x^\uparrow$ — each point converges to itself. A preconvergence with this property is a convergence.

$(X, \xi)$ is a convergence space; $|\xi| = X$ is the underlying set. $\xi^-(x)$ denotes the set of filters $\xi$-converging to $x$. For a filter-base $\mathcal{B}$ one abbreviates $\lim_\xi \mathcal{B} := \lim_\xi \mathcal{B}^\uparrow$. $\mathbb{I}X$ = convergences on $X$, $\mathbb{I}^\circ X$ = preconvergences on $X$.

Meaning

Section titled “Meaning”

第III章は「フィルターが点に収束する」関係 $\xi$ そのものを公理化する。第II章の Proposition II.1.1（$\mathcal{N}(x) \subset \Gamma_\varphi$）は一つの具体例に過ぎず、ここでは任意の proper filter と点の間の関係として一般化される。

centered 条件は「各点が自分自身の主 ultrafilter $x^\uparrow$ に収束する」——すなわち principal ultrafilter of $x$ が $x$ に $\xi$-収束する、という言い換えである。収束は本書の基礎言語であり、位相はその特別な場合として第VII章で現れる。

出典: refs/math/topology/royal-road-to-topology/pdfs/chp3-2024-convergence-of-filters.pdf p.35–36

Lean

Section titled “Lean”

一般の convergence space は Mathlib 本体に無い。位相 TopologicalSpace の場合、本書の $x \in \lim \mathcal{F}$ は F ≤ 𝓝 x に対応（本書の $\mathcal{F} \subset \mathcal{G}$ は Mathlib では 𝓖 ≤ 𝓕、cards/topology/filter-decomposition-theorem の規約ブリッジ参照）。

自作の最小限の形式化: Notes/ChapterIII.lean : ConvergenceSpace（Lim : Filter X → Set X ＋ isotone/centered、proper filter は Filter.NeBot の instance-implicit で表現、lake build 済み）