このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

Σ-Δ-Π随伴、もう一言

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

内容:

記号と言葉の準備

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

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

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

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

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

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

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

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

  1. パラメータの取り替え F:AB in Cat
  2. 射 f:A → B in C
  3. 対象 A in C (A∈|C|)

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

  1. \Sigma_F \dashv \Delta_F \dashv \Pi_F
  2. \Sigma_f \dashv \Delta_f \dashv \Pi_f
  3. \Sigma_A \dashv \Delta_A \dashv \Pi_A

最初に F:AB in Cat に対する ΔF を定義します。ΔF は、Q:BC 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':BC 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\circf (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 や、π1: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:ASet とみなすのでした。

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

  • ΔF:[B, Set] → [A, Set] in CAT

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

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