Proposition IV.1.3 (フィルターの像)
- Proposition IV.1.3 (フィルターの像) #Card
- proper filter $\mathcal{F}$ の像 $f[\mathcal{F}]$ は何になるか。
If $\mathcal{F}$ is a proper filter on $X$ and $f \in Y^X$, then $f[\mathcal{F}]$ is a filter-base on $Y$.
- $f(F_0) \cap f(F_1) \supset f(F_0 \cap F_1)$ と $\mathcal{F}$ が proper であることから。
- $f[\mathcal{F}]^\uparrow = f[\mathcal{F}]$（フィルターそのもの）$\iff f(X) = Y$。
証明の骨子. filter-base の 2 条件を確認する。
- 有限交叉で下に閉じる: $B_0, B_1 \in f[\mathcal{F}]$ なら $B_i = f(F_i)$（$F_i \in \mathcal{F}$）。$B_0 \cap B_1 = f(F_0) \cap f(F_1) \supset f(F_0 \cap F_1)$、かつ $F_0 \cap F_1 \in \mathcal{F}$（$\mathcal{F}$ は有限完備）ゆえ $f(F_0 \cap F_1) \in f[\mathcal{F}]$ がその下界を与える。
- 空集合を含まない（proper）: もし $\emptyset \in f[\mathcal{F}]$ なら $\emptyset = f(F)$ となる $F \in \mathcal{F}$ が存在し、これは $F = \emptyset$ を意味して $\mathcal{F}$ が proper であることに反する。∎
Filter.map f F（Mathlib では像は常にフィルターとして定義される）