Σ-Δ-Π随伴、もう一言 - 檜山正幸のキマイラ飼育記 (はてなBlog)

昨日、依存型に関連してΣ-Δ-Π随伴〈随伴トリオ〉の話をしたのですが、たまたま（ほんとに偶然に）別な文脈でもΣ-Δ-Π随伴が話題にのぼりました。そんなことがあったので、思いつくΣ-Δ-Π随伴の事例をザッと述べます。記事タイトルどおり、短い注釈です。

内容：

記号と言葉の準備
パラメータの取り替えに沿ったΣ-Δ-Π随伴
ガロア接続のΣ-Δ-Π随伴
データベースの場合

記号と言葉の準備

この節で述べる記号・言葉の約束は「依存型と総称型の圏論的解釈」と同じです。

Setは集合圏、Catは小さい圏の圏、CATは必ずしも小さいとは限らない圏の圏です。今注目している圏はCで、このCは集合圏Setの部分圏だとします。面倒なら、C = Set と固定して考えてもいいです。Cat ⊆ CAT、C ⊆ Set、Set∈|CAT| です。

Aは小さい圏として、関手 P:A → C in CAT のことを型理論風の言葉でC-ファミリー〈C-family〉と呼びます。関手の域Aは、C-ファミリーのパラメータ域〈{parameter | parameterization} domain〉またはインデックス域〈{index | indexing} domain〉といいます。

Cは小さいとは限りませんが、Aは小さいので具体的に取り扱い可能です。C-ファミリー（Cに値を取るファミリー）F:A → C in CAT は、C内に描かれた“形状がA”である図式〈ダイアグラム〉と考えることができます。例えば、|A| = {1, 2}, Mor(A) = {[1, 1] = id₁, [1, 2], [2, 2] = id₂} のとき、P:A → C in CAT は次のような図式（C内の一本の矢印）です。

$`\require{AMScd}
\mbox{in }\mathcal{C}\\
\:\\
\begin{CD}
P(1) @>{P([1, 2])}>> P(2)
\end{CD}
`$

Bも小さい圏で、F:A → B in Cat を関手とします。A, B をCのパラメータ域と捉えているとき、関手Fをパラメータの取り替え〈change of {parameter | parameterization} 〉といいます。パラメータの取り替えに伴うC-ファミリーの変化や操作が今回の主題です。

パラメータの取り替えに沿ったΣ-Δ-Π随伴

これから「☓☓☓に沿ったΣ-Δ-Π随伴」を考えます。☓☓☓は次のものです。

パラメータの取り替え F:A → B in Cat
射 f:A → B in C
対象 A in C （A∈|C|）

基本は一番目の「パラメータの取り替えFに沿ったΣ-Δ-Π随伴」です。残り2つは一番目から導出されます。3つの「☓☓☓に沿ったΣ-Δ-Π随伴」は次のように書きます。

$`\Sigma_F \dashv \Delta_F \dashv \Pi_F`$
$`\Sigma_f \dashv \Delta_f \dashv \Pi_f`$
$`\Sigma_A \dashv \Delta_A \dashv \Pi_A`$

最初に F:A → B in Cat に対する Δ_F を定義します。Δ_F は、Q:B → C in CAT にFを前結合〈pre-compose〉する操作 Δ_F(Q) := F＊Q です。ここで、'＊'は関手の図式順結合記号です。図式で描けば：

$`\xymatrix {
{}
&
&*{\mathcal{C}}
&
\\
{}
&*!<-2em, 0em>{R}
&
&*!<2em,0em>{Q} \ar@{|->}[ll]^-{\Delta_F}
\\
{}
&*{\mathcal{A}} \ar[rr]_{F} \ar@/^12pt/[uur]
&
&*{\mathcal{B}} \ar@/_12pt/[uul]
}\\
\mbox{commutes in }{\bf CAT}
`$

A, B, C で作られるCAT内の三角形は可換です。この可換三角形（等式 F＊Q = R）から、QをRへと引き戻す操作 Δ_F:Q $`\mapsto`$ R が定義できます。

Δ_Fは、自然変換〈2-射〉 ω::Q ⇒ Q':B → C in CAT に対しても定義できます。Δ_F(ω) := F＊ω 、ここで、'＊'は関手と自然変換のヒゲ結合〈whiskering〉です。結局Δ_Fは、Δ_F:[B, C] → [A, C] in CAT という（関手圏のあいだの）関手になります。

関手Δ_Fを基準として、Δ_Fの右随伴関手がΠ_F、左随伴関手がΣ_Fです。一般的には、左右の随伴関手〈パートナー関手〉の存在は保証されませんが、我々が扱う例（C = Set のときなど）ではΠ_FもΣ_Fも存在します。

随伴関手の定義から、次のホムセット同型が成立します。

$` [\mathcal{A}, \mathcal{C}](\Delta_F(Q), P) \cong [\mathcal{B}, \mathcal{C}](Q, \Pi_F(P)) `$
$` [\mathcal{A}, \mathcal{C}](P, \Delta_F(Q)) \cong [\mathcal{B}, \mathcal{C}](\Sigma_F(P), Q) `$

この状況を簡略に記した形が次です。

$`\Sigma_F \dashv \Delta_F \dashv \Pi_F`$

二番目のΣ-Δ-Π随伴である $`\Sigma_f \dashv \Delta_f \dashv \Pi_f`$ は、f:A → B in C に対して、F = J(f), A = J(A), B = J(B) （Jは反レイフィケーション埋め込み関手）と置けば得られます。つまり、

$` \Delta_f := \Delta_{J(f)}`$

さらに、f = !_A, B = 1 と置けば $`\Sigma_A \dashv \Delta_A \dashv \Pi_A`$ が得られます。

$` \Delta_A := \Delta_{!_A} := \Delta_{J(!_A)}`$

「依存型と総称型の圏論的解釈」と「依存型とΣ-Δ-Π随伴、そしてカン拡張」で述べたのは、このような状況でした。

ガロア接続のΣ-Δ-Π随伴

ガロア接続とは、順序集合（またはプレ順序集合）に対して定義した随伴概念です。ガロア接続に馴染みがないなら、次の記事とそこからのリンクをたどってみてください。

ガロア接続（順序随伴系）の簡単な例

以前にも何度か述べたことがありますが、論理における全称限量子と存在限量子の双対性は、ガロア接続に関するΣ-Δ-Π随伴（随伴トリオともいう）により統御されています。どういう状況かを説明しましょう。

B = {0, 1} をブール値の集合とします。0 < 1 という順序を考えます。すると、集合A上の述語〈真偽値関数〉の集合 Pred(A) := Map(A, B) は順序集合になります。写像 f:A → B in Set があると、順序集合のあいだの単調写像〈順序保存写像〉 Δ_f:Pred(B) → Pred(A) in Ord が誘導されます（Ordは順序集合の圏）。

Δ_f(q) := f;q = q$`\circ`$f （qにfを“代入”）

ここから先の議論は前節と同じですが、随伴を定義するホムセット同型は次のような論理同値（記号は'⇔'）で与えられます。

For p∈Pred(A), q∈Pred(B)
(Δ_f(q) ≦ p on A) ⇔ (q ≦ Π_f(p) on B)
For p∈Pred(A), q∈Pred(B)
(p ≦ Δ_f(q) on A) ⇔ (Σ_f(p) ≦ q on B)

論理では、f:A → B in Set として、!_A:A → 1 in Set や、π₁:A×B → A がよく使われます。そして、Π_f を ∀_f と書き、Σ_f を ∃_f と書く習慣です。

もうひとつ別な例として、CompHousをコンパクト・ハウスドルフ空間と連続写像の圏とします。[0, ∞] := R∪{∞} を無限大を入れた区間として、位相と順序を常識的に入れます。すると、[0, ∞]∈CompHous。区間 [0, ∞] は順序を持つので、連続写像の空間 C(A, [0, ∞]) は順序集合になります。つまり、C(A, [0, ∞])∈Ord。これで、論理の述語のときと同じセットアップになりました。

連続写像 f:A → B in CompHouse に対して、順序集合のあいだの単調写像 Δ_f:C(B, [0, ∞]) → C(A, [0, ∞]) in Ord が誘導されます。ここから先は論理の場合と同じように定義して、連続関数の最大値／最小値の議論ができます。コンパクト・ハウスドルフの仮定がなくても、∞を入れているので連続関数の上限／下限は定義可能です。

データベースの場合

最後にほんとに一言だけ、データベースの場合に触れておきます。スピヴァックの関手データモデル（「衝撃的なデータベース理論・関手的データモデル入門」参照）によれば、データベーススキーマの圏は、小さい圏の圏Catと同一視可能です。特定のスキーマAのデータベース状態は関手 P:A → Set とみなすのでした。

スキーマのあいだの射 F:A → B in Cat があると、B上のデータベース状態 Q:B → Set は、A上のデータベース状態 F＊Q に引き戻せます。この状態引き戻し操作がΔ_Fです。

Δ_F:[B, Set] → [A, Set] in CAT

Δ_Fを基準にして随伴関手トリオ $`\Sigma_F \dashv \Delta_F \dashv \Pi_F`$ を考えると、データマイグレーション関手が得られます。$`\Pi_F `$ がテーブルジョインによる変換、$`\Sigma_F `$ がテーブルユニオンによる変換です。

あっ、プログラム検証のホーア論理とプレ条件／ポスト条件の例を忘れた、まっいいや。