手筋: 随伴（Galois 接続）で extrema を運ぶ (Ex IV.10.8 / Prop I.3.8 / Prop I.4.2)
- 手筋: 随伴（Galois 接続）で extrema を運ぶ (Ex IV.10.8 / Prop I.3.8 / Prop I.4.2) #Card
- 終収束・始収束や polar のような対をなす作用素の等式（extrema の保存など）を一撃で示す手筋は？
核: 随伴関係 $$f\xi \geq \tau \iff \xi \geq f^-\tau \qquad \text{(IV.3.5)}$$ があるとき、等式 $\theta_1 = \theta_2$ は反対称性より「支配する対象が同じ ($\forall \tau: \theta_i \geq \tau$ が一致)」に帰着できる。随伴の左側は $\bigwedge$ を、右側は $\bigvee$ を保存する: $$f\Bigl(\bigwedge_{\Xi}\xi\Bigr) = \bigwedge_{\Xi} f\xi, \qquad f^-\Bigl(\bigvee_{T}\tau\Bigr) = \bigvee_{T} f^-\tau \qquad \text{(Ex IV.10.8)}$$ 証明は $f(\bigwedge \xi) \geq \tau \iff \bigwedge \xi \geq f^-\tau \iff \forall \xi: \xi \geq f^-\tau \iff \forall \xi: f\xi \geq \tau \iff \bigwedge f\xi \geq \tau$ と鎖でつなぐだけ。
同族の実例.
- Prop I.3.8: 順序同型（両向き随伴）は $\bigvee, \bigwedge$ の両方を保存——「上界集合の対応」の議論はこの特殊形。
- Prop I.4.2: $R^{\circ}A \supset B \iff A \subset R^{-\circ}B \iff A \times B \subset R$ は反変 Galois 接続の定義式。bipolar の閉包性 (I.4.5–I.4.7) が自動で従う。
- Ex IV.10.13: $\bigvee_j \xi_j = (\prod_j \xi_j)|_{\Delta(X)}$——上限＝対角埋め込みによる始収束。
- 像・逆像 $f[\cdot] \dashv f^-[\cdot]$（IV.1）、位相の $\mathrm{gc_coinduced_induced}$。
射程: 弱位相 $\sigma(X, {f_j}) = \bigvee_j f_j^-\tau_j$・積収束・商収束の計算規則はすべてこの1本から出る。測度論では積 $\sigma$-代数（$\bigvee$ で生成）・分布の弱収束位相が同じ文法。
Mathlib: GaloisConnection（gc.l_iSup / gc.u_iInf）、位相では gc_coinduced_induced、フィルターでは Filter.gc_map_comap。