「述語論理とインデックス付き圏と限量随伴性」、「全称記号の導入規則について考える」において、述語論理の背後に限量随伴性（quantification as adjunction）があって、形式的な推論の規則を支配していることを述べました。
論理の真偽値がなす圏は、順序集合（むしろプレ順序集合）と考えていいことが多いので、そのときは順序構造の随伴性になります。順序構造の随伴性はガロア接続（Galois connection）とも呼ばれます。ガロア接続を圏論なしで扱うことが出来ますが、ここでは関手対の随伴性の特殊ケースとして圏論的に扱ってみます。
内容：
プレ順序集合と単調写像
A = (A, ≦) をプレ順序集合（preordered set）とします。例によって、(A, ≦) という書き方は記号の乱用で、文字'A'はプレ順序構造全体と、その台集合（underlying set）の両方の意味で使っています。プレ順序の公理は次の2つだけです。
- a∈A に対して、a ≦ a （反射性）
- a, b, c∈A に対して、a ≦ b, b ≦ c ならば a ≦ c （推移性）
A, Bがプレ順序集合で、写像 f:A→B が次の性質を持つなら単調写像（monotone map）と呼びます。
- a ≦ b ならば f(a) ≦ f(b)
次を満たすならば反単調写像（antitone/anti-monotone map）です。
- a ≦ b ならば f(b) ≦ f(a)
すべてのプレ順序集合と、そのあいだの単調写像は圏Preordをなします。圏Preordは、圏と関手の圏Catの簡易版だとみなせます。Catで意味を持つ概念は、すべてPreordにその対応物があります。その理由は簡単で、プレ順序集合はやせた圏なので、Preord⊆Cat とみなせるからです。単調写像は関手で、反単調写像は反変関手です。
圏論の一般的な概念を、プレ順序集合に適用するのはよい練習問題になります。例えば、プレ順序集合に対するモナドを考えることができます。以下の記事に書いてあります。
プレ順序集合のホムセット
プレ順序集合に対して、圏論の概念や記法を使って議論することにします。Aがプレ順序集合で、a, b∈A のとき、集合A(a, b)を次のように定義します。
- a ≦ b が成立しているときは、A(a, b)は単元集合（singleton set）。
- a ≦ b が成立していないときは、A(a, b)は空集合。
単元集合の唯一の要素は何でもいいです。2つの例を挙げておきます。
- 例1： a ≦ b が成立しているときは、A(a, b) = {0}
- 例2： a ≦ b が成立しているときは、A(a, b) = {(a, b)}
A(a, b)を定義したのは、圏のホムセットの概念を使いたいからです。A(a, b)を上のように定義しておくと、次が2つの主張が同じ意味になります。
- A(a, b)
A(c, d)
- a ≦ b ⇔ c ≦ d
A(a, b) A(c, d) という集合の同型が成立するのは次のどちらかの場合です。
不等号で書き換えると：
- a ≦ b かつ c ≦ d
- a ≦ b でなく、かつ c ≦ d でもない
要するに、a ≦ b と c ≦ d の真偽は一致するので、a ≦ b ⇔ c ≦ d です。
順序随伴性
f:A→B, g:B→A がプレ順序集合のあいだの単調写像のとき、fとgが随伴ペア（adjoint pair, a pair of adjoint monotone maps）であることは、次のように定義できます。
- a∈A, b∈B に対して、B(f(a), b)
前節の結果より、不等号と論理同値（⇔）で書けば：
- a∈A, b∈B に対して、f(a) ≦ b ⇔ a ≦ g(b)
この場合、fをgの左随伴（right adjoint）、gをfの右随伴（left adjoint）と呼び、次のように書きます。
- f -| g
順序の場合は、左随伴の代わりに下随伴（lower adjoint）、右随伴の代わりに上随伴（upper adjoint）とも呼びます。
例1
論理に関係した順序随伴の例を挙げます。演繹定理（deduction theorem）と呼ばれる随伴性です。
Xを集合としてPow(X)をベキ集合とします。Pow(X)は、部分集合の包含順序で順序集合になります。W∈Pow(X) をひとつ選んで固定します。FとGを、任意の S∈Pow(X) に対して以下のように定義します。F, Gが単調になることはすぐに確認できます。
- F(S) := S∩W
- G(S) := Wc∪S （(-)cは補集合）
このとき、次が成立します。
- F(S) ⊆ T ⇔ S ⊆ G(T)
F, Gの定義を使って書き換えれば：
- S∩W ⊆ T ⇔ S ⊆ Wc∪T
このF, Gは随伴ペアの例で、F -| G となっています。
例2
もうひとつ、ベキ集合を使った例を挙げましょう。これも論理に関係していて、存在限量子（existential quantifier）に関する限量随伴性です。対応する推論の方法は「述語論理とインデックス付き圏と限量随伴性」で述べました（ただし、全称限量子の話で存在限量子は触れてない）。
f:X→Y を写像として、S⊆X に対するfによる像をf*(S)、T⊆Y に対するfによる逆像をf*(T)とします。f*:Pow(X)→Pow(Y), f*:Pow(Y)→Pow(X) となり、f*, f* ともに単調写像になります。この状況で次が成立します。
- f*(S) ⊆ T ⇔ S ⊆ f*(T)
f* -| f* ですね。
単位と余単位
2つの単調写像f, gの随伴性 f -| g を定義する同型を再掲します。
- B(f(a), b)
ここで b = f(a) と置けば：
- B(f(a), f(a))
不等式と論理同値で書き換えれば：
- f(a) ≦ f(a) ⇔ a ≦ g(f(a))
f(a) ≦ f(a) は常に成立するので、a ≦ g(f(a)) も常に成立することになります。これにより次の不等式が得られました。
- a ≦ g(f(a))
同様にして次の不等式も得られます。
- f(g(b)) ≦ b
上記の2つの不等式は、任意のa, bに対して成立していることから次のようにも書けます。
- ∀a∈A. a ≦ g(f(a))
- ∀b∈B. f(g(b) ≦ b
恒等写像をidA, idB、写像の反図式順結合を'・'で書くと：
- idA ≦ g・f
- f・g ≦ idB
1番目の不等式を、随伴性 f -| g の単位不等式（unit enequality）、2番目の不等式を、随伴性 f -| g の余単位不等式（counit enequality）と呼びます。これは、圏論の用語「随伴の単位」「随伴の余単位」をそのまま使っています。
随伴性と単位・余単位
プレ順序集合のあいだの単調写像 f:A→B, g:B→A に関して、次のステートメントは同じことです。
- a∈A, b∈B に対して、B(f(a), b)
- a∈A, b∈B に対して、f(a) ≦ b ⇔ a ≦ g(b)
- f -| g （fとgは互いに随伴）
さらには、単位・余単位不等式によっても随伴性が記述できます。つまり、次のような同値があります。
- f -| g ⇔ 単位・余単位不等式が成立する
'⇒'方向は前節で示したので、逆方向の主張を示しましょう。単位・余単位不等式と f(a) ≦ b も仮定します。次のようにして、a ≦ g(b) が示せます。
仮定より f(a) ≦ b これとgの単調性から g(f(a)) ≦ g(b) ……(1) 単位不等式より a ≦ g(f(a)) ……(2) (1), (2), ≦の推移性より a ≦ g(b)
同様に、a ≦ g(b) を仮定して、余単位不等式から f(a) ≦ b が示せます。つまり、
- 単位・余単位不等式が成立するならば、f(a) ≦ b ⇔ a ≦ g(b) （随伴性）が言える。
これで、fとgの随伴性と、それに対する単位・余単位不等式が同値であることが分かりました。
具体例を見ておきましょう。集合X, Yのベキ集合に対する像・逆像 f*:Pow(X)→Pow(Y), f*:Pow(Y)→Pow(X) に関して、随伴性は次の形でした。
- f*(S) ⊆ T ⇔ S ⊆ f*(T)
対応する単位・余単位不等式は次のとおり。
- idPow(X) ⊆ f*・f*
- f*・f* ⊆ idPow(Y)
S⊆X, T⊆Y を使って書けば：
- S ⊆ f*(f*(S))
- f*(f*(T)) ⊆ T
おわりに
順序随伴（ガロア接続）が、関手の随伴性と同じ定義を持ち、単位と余単位によっても記述できることが分かったと思います。しかし、プレ順序構造に関する概念が、圏論的概念とホントに対応していることを心底納得するのは意外と困難です。使っている記法があまりに違いすぎるのです。
「双対や随伴に強くなるためのトレーニング」で述べたような上下左右の使い方の乖離も記法の違いに含まれます。不等号・不等式を縦書きにして、順序の推移性による推論を左から右に向かって行う、とかに慣れないと、心底納得した気になれないと思います。
このへんの、伝統的・常識的記法が障壁・撹乱要因となり、理解と学習を妨げている現象はいずれ取り上げたいと思います。（[追記]「記法バイアスと記法独立な把握： 順序随伴を例として」で取り上げました。[/追記]）
