量化子の随伴

同義語:quantifiers as adjoints随伴としての量化子

概要

量化子の随伴(quantifiers as adjoints)とは、部分対象の引き戻し $f^*$ に対し、存在量化 $\exists_f$ が左随伴、全称量化 $\forall_f$ が右随伴になる構造である。集合では像とファイバー全体への条件で計算できる。集合上の随伴と引き戻しとの交換を証明し、前層で全称量化にすべての制限先が必要になる理由を示す。

$$\newcommand{C}[0]{\mathbb{C}} \newcommand{N}[0]{\mathbb{N}} \newcommand{Q}[0]{\mathbb{Q}} \newcommand{R}[0]{\mathbb{R}} \newcommand{Z}[0]{\mathbb{Z}} $$

前提知識: 随伴, 引き戻し, 部分対象, 前層

定義

述語 $S(z)$ を集合 $Z$ の部分集合とみなし、写像 $f\colon Z\to Y$ によって変数を $Y$ 側へ移す。$Y$ の部分集合を $Z$ へ引き戻す操作 $f^*$ に対し、「ある $z$ が満たす」と「すべての $z$ が満たす」を返す操作はそれぞれ左随伴と右随伴になる。これが 量化子の随伴 という見方である。MM92 I §9。

部分対象の引き戻しと量化子

引き戻しをもつ圏 $\mathcal E$ の射 $f\colon Z\to Y$ を考える。対象 $Y$ について $\operatorname{Sub}(Y)$ は、$Y$ への単射(モノ射)の同型類を、$m\le m'$ を「$m$ が $m'$ を経由して分解する」で並べた順序集合である。単射の引き戻しは単射なので、部分対象の引き戻し
$$ f^*\colon\operatorname{Sub}(Y)\longrightarrow\operatorname{Sub}(Z) $$
が定まる。これに左随伴 $\exists_f$ と右随伴 $\forall_f$ があるとは、任意の $S\in\operatorname{Sub}(Z)$、$T\in\operatorname{Sub}(Y)$ について
$$ \exists_f S\leq T\quad\Longleftrightarrow\quad S\leq f^*T, \qquad f^*T\leq S\quad\Longleftrightarrow\quad T\leq\forall_f S $$
が成り立つことをいう。順序は部分対象の包含を表す。したがって $\exists_f\dashv f^*\dashv\forall_f$ であり、両量化子は存在すれば一意である。MM92 I §9。

述語 $S(x,y)$ に対して射 $p\colon X\times Y\to Y$ を投影とすれば、$\exists_p S$ は「ある $x$ に対して $S(x,y)$」、$\forall_p S$ は「すべての $x$ に対して $S(x,y)$」を表す。一般の $f$ では、量化する範囲は各 $y$ のファイバー $f^{-1}(y)$ になる。

直感

$f^*$ は述語を変数変換で読み替える。$\exists_f$ は $f^*$ で読み替えると $S$ を含むような、最小の $Y$ 側の述語、$\forall_f$ は読み替えると元の述語の内側に収まる最大の $Y$ 側の述語である。この大小関係が随伴式になり、集合の要素を直接使えない圏でも量化の意味を指定できる。

例と反例

集合上の存在・全称

$\mathbf{Set}$ で $f\colon Z\to Y$ と $S\subset Z$ に対し
$$ \exists_f S=\{y\in Y\mid \text{ある }z\in f^{-1}(y)\text{ が }S\text{ に属する}\}=f(S), $$
$$ \forall_f S=\{y\in Y\mid f^{-1}(y)\subset S\} $$
と定める。$f^{-1}(y)=\emptyset$ なら、$y$ は $\exists_f S$ に入らず、$\forall_f S$ には入る。空の範囲に対する存在文は偽、全称文は真という通常の規則と一致する。MM92 I §9。

投影と一変数の消去

$X=\{0,1\}$、$Y=\{a,b\}$、$S=\{(0,a),(1,a),(0,b)\}\subset X\times Y$ とする。投影 $p\colon X\times Y\to Y$ について $\exists_p S=\{a,b\}$ だが $\forall_p S=\{a\}$ である。$a$ のファイバーは両方とも $S$ に入り、$b$ のファイバーは片方だけ入るためである。

反例:像を全称量化に使えない

上の投影では $p(S)=\{a,b\}$ は存在量化を与えるが、全称量化は $\{a\}$ である。したがって「像をとれば全称量化にもなる」は誤りである。随伴の向きも異なり、像は $p^*$ の左随伴、全称量化は右随伴である。

性質

集合の圏での随伴

集合上の量化子の随伴

任意の写像 $f\colon Z\to Y$ に対し、上の $\exists_f$ と $\forall_f$ は $f^*T=f^{-1}(T)$ の左随伴と右随伴である。MM92 I §9。

包含を要素で確かめる

まず $\exists_f S\subset T$ は、$z\in S$ なら必ず $f(z)\in T$ という条件と同値であり、$S\subset f^{-1}(T)$ と同値である。次に $f^{-1}(T)\subset S$ は、$y\in T$ のすべての逆像 $z\in f^{-1}(y)$ が $S$ に入るという条件と同値であり、$T\subset\forall_f S$ と同値である。空ファイバーもこの同値に含まれる。$\square$

引き戻しと量化子の交換

集合における Beck–Chevalley の等式

集合の引き戻し正方形
$$ \begin{array}{ccc} Z'&\xrightarrow{g'}&Z\\ \big\downarrow f'&&\big\downarrow f\\ Y'&\xrightarrow{g}&Y \end{array} $$
において、$S\subset Z$ に対し
$$ g^*(\exists_f S)=\exists_{f'}((g')^*S),\qquad g^*(\forall_f S)=\forall_{f'}((g')^*S) $$
である。これは量化する変数とは別の変数を代入しても結果が一致することを表す。MM92 IV §9(初等トポス一般の場合。$\mathbf{Set}$ はその特別な場合)。

同じファイバーを比較する

$Z'$ を $\{(z,y')\mid f(z)=g(y')\}$ と表す。$y'\in Y'$ が左辺の存在量化に入る条件は、$f(z)=g(y')$ かつ $z\in S$ である $z$ が存在すること。右辺では $(z,y')\in Z'$ が $(g')^*S$ に入り、$f'(z,y')=y'$ となる条件なので同じである。全称量化についても、左辺の条件は $f(z)=g(y')$ であるすべての $z$ が $S$ に入ること。これは $f'^{-1}(y')$ のすべての $(z,y')$ が $(g')^*S$ に入るという右辺の条件と同じである。よって両等式が従う。$\square$

前層での全称量化

部分前層 $S\subset Z$ とは、各対象 $U$ で $S(U)\subset Z(U)$ が制限で閉じる(任意の $u\colon V\to U$ で $Z(u)(S(U))\subset S(V)$)ものをいう。前層の射の引き戻しは点ごとに計算されるので、$\operatorname{Sub}(Z)$ は部分前層の包含順序と同一視でき、部分前層 $T\subset Y$ の引き戻しは $(f^*T)(U)=f_U^{-1}(T(U))$ で与えられる。
集合上の全称量化を点ごとに適用するだけでは、前層の制限写像で閉じないことがある。例えば $\mathcal C$ を $0\to1$ の二元鎖、$Y=1$(各対象で一元集合)、$Z(1)=\emptyset$、$Z(0)=\{*\}$、$S=\emptyset$ とすると、集合の全称量化を点ごとに適用した値は、$U=1$ ではファイバー $Z(1)=\emptyset$ が空だから $\{*\}$、$U=0$ では $\emptyset$ となり、制限 $Y(1)\to Y(0)$ で閉じない(破れる条件:制限への閉性。実際は後述の式により $(\forall_fS)(1)=\emptyset$ になる)。そこで後続のすべての射も条件に入れる。

部分前層の量化子

$\mathcal C$ を小圏、$f\colon Z\to Y$ を集合値前層の射とする。部分前層 $S\subset Z$ に対し、$\exists_f S$ は $f$ の点ごとの像であり、$\forall_f S$ は
$$ (\forall_f S)(U)=\{y\in Y(U)\mid\text{すべての }u\colon V\to U\text{ と }z\in Z(V)\text{ について、}f_V(z)=Y(u)y\Rightarrow z\in S(V)\} $$
で定まる。このとき $\exists_f\dashv f^*\dashv\forall_f$ である。MM92 I §9, Exercise 10。

像と安定な全称条件

$f_U(S(U))$ は $U$ に関する制限に閉じる。実際、$f_U(s)$ を $u\colon V\to U$ で制限すると $f_V(Z(u)s)$ になり、$S$ が部分前層だから $Z(u)s\in S(V)$。ゆえに点ごとの像は部分前層である。$\exists_f S\subset T$ と $S\subset f^*T$ は各 $U$ の集合での同値を並べたものなので左随伴が従う。
右辺を $Q(U)$ とおく。$y\in Q(U)$ を $u\colon U'\to U$ で制限し、さらに $v\colon V\to U'$ と $z\in Z(V)$ をとる。$f_V(z)=Y(v)Y(u)y=Y(u\circ v)y$ なら、$y\in Q(U)$ の条件から $z\in S(V)$。したがって $Q$ は部分前層である。$f^*T\subset S$ なら $y\in T(U)$ のすべての制限 $Y(u)y$ は $T(V)$ にあるので、その逆像の $z$ は $S(V)$ に入り、$T\subset Q$。逆に $T\subset Q$ なら $z\in(f^*T)(U)$ に対し $f_U(z)\in T(U)\subset Q(U)$ として $u=\operatorname{id}_U$ を適用すれば $z\in S(U)$。ゆえに $f^*T\subset S$。これが右随伴の条件である。$\square$

この式の $u$ を省くと、今いる対象でのファイバーだけを調べることになる。前層の論理では、その後のすべての制限先でも述語が真であることを確かめて初めて全称量化となる。Heyting代数の部分前層の含意も同じ形の「すべての制限先」を使う。

関連項目

参考文献

Mathpediaは寄付と、参考文献の書籍リンク(Amazonアソシエイト)の紹介料で運営されています。 支援について / 寄付する