論理計算と随伴関手(17) - エレファント・コンピューティング調査報告

下方向が証明図の方向になるように書き直しました。

$\require{AMScd} \begin{CD} P(\bar{L}) @> f_n >> P(\bar{L}) \\ @A \overleftarrow{\gamma}^{n-m} AA @VV \overrightarrow{\gamma}^{n-m} V \\ P(\bar{L}) @> f_m >> P(\bar{L}) \\ @A \overleftarrow{\gamma}^{m} AA @VV \overrightarrow{\gamma}^{m} V \\ P(\bar{L}) @>> f_0 > P(\bar{L}) \end{CD}$

前回の例で考えると $f_m(\{\gamma \vdash rep(n-m, [a]^{n-m} )\}) = \{1\}$ が成り立てば良いので $f_m = \overleftarrow{\gamma}^{n-m}$ とすれば良いということになります。

$\overleftarrow{\gamma}^{n}(\{s\}) = \{1\}$ を満たす $s \in \bar{S}$ を考えます。「 $s$ を $n$ 項から $m$ 項に切り詰めたもの」は $\overrightarrow{\gamma}^{m}(\{1\}) = \overrightarrow{\gamma}^{m}(\overleftarrow{\gamma}^{n}(\{s\}))$ となります。

$\overrightarrow{\gamma}^{m} \circ \overleftarrow{\gamma}^{n}$ からなる射影系の射影的極限を証明図の極限と考えることができるということになります。