Proposition IV.1.4 (フィルターの逆像)
- Proposition IV.1.4 (フィルターの逆像) #Card
- proper filter $\mathcal{G}$ の逆像 $f^-[\mathcal{G}]$ がフィルター基底になる条件。
If $\mathcal{G}$ is a proper filter on $Y$ and $f \in Y^X$, then $f^-[\mathcal{G}]$ is a filter-base if and only if $f(X) \cap G \neq \emptyset$ for every $G \in \mathcal{G}$.
- $f^-(G_0 \cap G_1) = f^-(G_0) \cap f^-(G_1)$ なので、問題は空でないことだけ。
- $f$ が単射なら $f^-[\mathcal{G}]$ はフィルターそのもの。
証明の骨子. 逆像は交叉と可換: $f^-(G_0 \cap G_1) = f^-(G_0) \cap f^-(G_1)$。よって $f^-[\mathcal{G}]$ が有限交叉で下に閉じることは $\mathcal{G}$ 側から自動で従い、filter-base になるための唯一の障害は「空集合が現れないこと」だけである（proper filter の特徴づけ Prop II.2.2 と同じ論法）。各 $G \in \mathcal{G}$ について $f^-(G) \neq \emptyset \iff f(X) \cap G \neq \emptyset$（$x \in f^-(G) \iff f(x) \in G \cap f(X)$）。ゆえに $f^-[\mathcal{G}]$ が filter-base $\iff$ すべての $G \in \mathcal{G}$ で $f(X) \cap G \neq \emptyset$。$f$ 単射なら cards/topology/image-preimage-adjunction の等号 $f^-[f[\cdot]]=\cdot$ により $f^-[\mathcal{G}]$ は upward-closed で、そのままフィルター。∎
Filter.comap f G（Filter.comap_neBot_iff）