Skip to content
Journals Garden

Initial Convergence $f^-\tau$ (始収束) (Definition IV.3.1)

  • Initial Convergence $f^-\tau$ (始収束) (Definition IV.3.1) #Card
    • The coarsest convergence on $X$ for which $f : X \to Y$ is continuous to $\tau$; formula: $\lim_{f^-\tau} \mathcal{F} = f^-(\lim_\tau f[\mathcal{F}])$.

Back

Section titled “Back”

Let $f : X \to Y$ and $\tau$ a convergence on $Y$. The coarsest convergence on $X$ for which $f$ is continuous is called the initial convergence with respect to $(f, \tau)$, denoted $f^-\tau$. It always exists and uniquely (Proposition IV.3.2), with the instrumental formula $$\lim_{f^-\tau} \mathcal{F} = f^-(\lim_\tau f[\mathcal{F}]). \tag{IV.3.1}$$

  • 始収束は「点の収束」というよりファイバーの収束: $x \in \lim_{f^-\tau} \mathcal{F} \implies f^-(f(x)) \subset \lim_{f^-\tau} \mathcal{F}$（Proposition IV.3.3）。$f$ 単射ならファイバーは一点で通常の収束。
  • $f(f^-\tau) \geq \tau$（全射なら等号、Prop IV.10.6）。

Lean

Section titled “Lean”

位相の場合 TopologicalSpace.induced f τ（𝓝 は nhds_induced : 𝓝 x = comap f (𝓝 (f x))）。一般の ConvergenceSpace では Notes/ChapterIV.lean : initialConv（公式 (IV.3.1) をそのまま定義に採用、lake build 済み）