Skip to content
Journals Garden

Lemma IV.10.7 (像はフィルターの inf と可換)

  • Lemma IV.10.7 (像はフィルターの inf と可換) #Card
    • $h[\bigwedge \mathbb{F}]$ はどうなるか。像と自由部分・主部分の関係は？

Back

Section titled “Back”

For any collection $\mathbb{F}$ of filters and a map $h$, $$h\left[\bigwedge \mathbb{F}\right] = \bigwedge {h[\mathcal{F}] : \mathcal{F} \in \mathbb{F}}.$$

  • 帰結: $f[\mathcal{F}] = f[\mathcal{F}^*] \wedge f[\mathcal{F}^\bullet]$（自由部分・主部分の分解 cards/topology/filter-decomposition-theorem と併用）。$f[\mathcal{F}^\bullet]$ は主フィルター。
  • ただし自由フィルターの像は自由とは限らない（$f : X \to {0}$ なら $f[(X)_0] = {0}^\uparrow$ は主）。一方 $f(\operatorname{ker}\mathcal{F}) \subset \operatorname{ker} f[\mathcal{F}]$ (IV.10.4)。

証明の骨子. inf（$\bigwedge$）は「各フィルターから 1 つずつ取った要素の和集合で下から近似される」ことを使う。$\bigwedge\mathbb{F}$ の一般の要素は $\bigcup_{\mathcal{F}\in\mathbb{F}} F_{\mathcal{F}}$（各 $F_\mathcal{F} \in \mathcal{F}$、cards/topology/cofinite-filters-inf-sup と同型の inf 公式）を含む集合として書ける。

  • $W \in h[\bigwedge\mathbb{F}]$ $\iff$ ある $\bigcup_{\mathcal{F}} F_\mathcal{F} \in \bigwedge\mathbb{F}$（各 $F_\mathcal{F}\in\mathcal{F}$）で $h(\bigcup_\mathcal{F} F_\mathcal{F}) = \bigcup_\mathcal{F} h(F_\mathcal{F}) \subset W$ $\iff$ 各 $\mathcal{F}$ で $h(F_\mathcal{F}) \subset W$ となる $F_\mathcal{F}\in\mathcal{F}$ が取れる、すなわち $W \in h[\mathcal{F}]$ が各 $\mathcal{F}$ で成立 $\iff W \in \bigwedge{h[\mathcal{F}] : \mathcal{F}\in\mathbb{F}}$。 像が和集合と可換（$h(\bigcup A_i) = \bigcup h(A_i)$）である点が鍵。ゆえに $h[\bigwedge\mathbb{F}] = \bigwedge{h[\mathcal{F}]}$。
  • 帰結: 分解 $\mathcal{F} = \mathcal{F}^* \wedge \mathcal{F}^\bullet$（cards/topology/filter-decomposition-theorem）に適用して $f[\mathcal{F}] = f[\mathcal{F}^*] \wedge f[\mathcal{F}^\bullet]$。$\mathcal{F}^\bullet$ は主（$\operatorname{ker}\mathcal{F}$ 上）ゆえ $f[\mathcal{F}^\bullet]$ も主。∎

Lean

Section titled “Lean”

Filter.map_iInf…は単射時のみ等号。一般の inf との可換は Filter.map_inf_le 系に注意（Mathlib 順序では sup 側: Filter.map_sup）