Lemmas IV.1.1–IV.1.2 (像と逆像の随伴)
- Lemmas IV.1.1–IV.1.2 (像と逆像の随伴) #Card
- 集合族に対する $f[\cdot]$ と $f^-[\cdot]$ の粗細関係と、随伴公式 (IV.1.4)。
For $f : X \to Y$, writing $f[\mathcal{F}] := {f(F) : F \in \mathcal{F}}$ and $f^-[\mathcal{G}] := {f^-(G) : G \in \mathcal{G}}$:
- Lemma IV.1.1: $\mathcal{G} \geq f^-[f[\mathcal{G}]]$ for $\mathcal{G} \subset 2^X$; equality if $f$ is injective.
- Lemma IV.1.2: $f[f^-[\mathcal{H}]] \geq \mathcal{H}$ for $\mathcal{H} \subset 2^Y$; equality if $f$ is surjective.
- 帰結の随伴公式 (IV.1.4): $f^-[\mathcal{H}] \leq \mathcal{G} \iff \mathcal{H} \leq f[\mathcal{G}]$（Galois 接続）。
（土台は $f(f^-(B)) \subset B$（全射で等号）と $A \subset f^-(f(A))$（単射で等号）。）
証明の骨子. 集合レベルの包含 $A \subset f^-(f(A))$・$f(f^-(B)) \subset B$（cards/topology/technique-galois-adjunction）を族に持ち上げる。
- IV.1.1: $f^-[f[\mathcal{G}]] = {f^-(f(G)) : G \in \mathcal{G}}$。各 $G \subset f^-(f(G))$ より $\mathcal{G} \geq f^-[f[\mathcal{G}]]$（細分＝より小さい集合を含む側）。$f$ 単射なら $G = f^-(f(G))$ で等号。
- IV.1.2: $f[f^-[\mathcal{H}]] = {f(f^-(H)) : H \in \mathcal{H}}$。各 $f(f^-(H)) \subset H$ より $f[f^-[\mathcal{H}]] \geq \mathcal{H}$。$f$ 全射なら $f(f^-(H)) = H$ で等号。
- 随伴 (IV.1.4): 上の 2 つから即従う。$\mathcal{H} \leq f[\mathcal{G}] \Rightarrow f^-[\mathcal{H}] \leq f^-[f[\mathcal{G}]] \leq \mathcal{G}$（最後は IV.1.1）。逆に $f^-[\mathcal{H}] \leq \mathcal{G} \Rightarrow \mathcal{H} \leq f[f^-[\mathcal{H}]] \leq f[\mathcal{G}]$（最初は IV.1.2）。ゆえに $f^-[\mathcal{H}] \leq \mathcal{G} \iff \mathcal{H} \leq f[\mathcal{G}]$、すなわち $f[\cdot] \dashv f^-[\cdot]$ の Galois 接続。∎
Filter.map f ⊣ Filter.comap f（Filter.map_le_iff_le_comap）