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

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

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

参照用 記事

依存型とΣ-Δ-Π随伴、そしてカン拡張

「依存積型」と「依存和型」に関しては、もうサンザンだよー、あったく‥‥(昨日の記事「依存型と総称型の圏論的解釈」の冒頭を参照)

ふんとに「依存ナントカ型」って紛らわしいよねぇ。それで、「依存ナントカ型」と言うのはやめます。

なんかまた間違える混乱する気がするので、今後は見たままのパイ型/シグマ型を使おうと思います。

パイ〈Π〉とかシグマ〈Σ〉って呼び名にすると、思い出すことがあります -- \Sigma \dashv \Delta \dashv \Pi という随伴の系列です。依存型のパイ型/シグマ型も、この“Σ-Δ-Π随伴”の事例です。パイ型/シグマ型をもう少し一般化することができて、それはカン拡張になります。

てな話を手短かにします。昨日の記事「依存型と総称型の圏論的解釈」の続きです。

内容:

錐と、定数関手からの自然変換

依存型と総称型の圏論的解釈」と同様、Cは集合圏Setの部分圏であるデカルト閉圏とします(この仮定はあまり使いませんが)。F:J(A) → C は、J(A)をインデックス域とするC-ファミリーとします。これは単に「Fは関手だ」と言っているのと同じです。ψは、X∈|C| を頂点として、Fを底面とする錐だとします。

錐ψについてもっと詳しく言うと; a∈A ごとに ψa:X → F(a) in C が割り当てられているときに、その全体を〈cone〉というのです。ただし、今回の錐はちょっと特殊で、底面である関手 F:J(A) → C が離散圏からの関手なので、図式可換性に関する条件が何もありません。域が離散圏じゃなければ図式可換性の条件が加わります。

「錐ψ、頂点X、底面F」なんて呼び名をするのは次のような感じだからです。A = {a, b, c} の絵です*1


F: \{a, b, c\} \to \mathcal{C} \mbox{ in }{\bf CAT}\\
\:\\
\mbox{in }\mathcal{C}\\
\xymatrix@R+1pc {
  {}
  &*{X} \ar[dl]_-{\psi_a} \ar[d]|-{\psi_b} \ar[dr]^-{\psi_c}
  &
\\
  *{F(a)}
  &*{F(b)}
  &*{F(c)}
}

頂点から底面に向かう射を、僕は“成分線”と呼んでいます。すぐ下で説明するように、自然変換の成分〈component〉だからです。

J(A)のすべての対象(集合Aの要素)を特定対象Xに対応させる関手を KA(X):J(A) → C とします。

  • すべての a∈A に対して、KA(X)(a) = X

Xを頂点、Fを底面とする錐ψは、定数関手KA(X)からFへの自然変換と同じです。ちょっと考えればわかることだと思います。

上の事実から、錐ψを自然変換の記法で書くことにします。

  • ψ::KA(X) ⇒ F:J(A) → C in CAT

CATの2-射である自然変換は、関手圏の射〈1-射〉なので次のようにも書けます。

  • ψ:KA(X) → F in [J(A), C]

ここで、[J(A), C] は、J(A)からCへの関手を対象として自然変換を射とする関手圏です。関手圏[J(A), C]のホムセットを使って次のように書いても同じことです。

  • ψ∈[J(A), C](KA(X), F)

右随伴Πと左随伴Σ

ファミリー〈関手〉F:J(A) → C のパイ型 ΠA(F) とは、極限 Limj(A)(F) のことでした。極限の定義から、錐 ψ:KA(X) → F in [J(A), C] と射 f:X → ΠA(F) は1:1対応するのでした。この1:1対応は次のように書けます。左辺は錐の集合、右辺は射の集合です。

  •  [J(A), \mathcal{C}](K_A(X), F) \cong \mathcal{C}(X, \Pi_A(F))

実際には関手性とか自然性とかのチェックが必要なんですが、上記の同型は、関手KAと関手ΠAが随伴関手ペアであることを主張しています。

  •  K_A:\mathcal{C} \to [J(A), \mathcal{C}] \mbox{ in }{\bf CAT}
  •  \Pi_A:[J(A), \mathcal{C}] \to \mathcal{C} \mbox{ in }{\bf CAT}
  •  K_A \dashv \Pi_A

同様に、ファミリーFのシグマ型は次のホムセット同型を与えます。右辺のホムセットは、余頂点Yで底面がFである余錐の集合とみなせます(余錐は錐の矢印の向きを逆にしたものです)。

  •  \mathcal{C}(\Sigma_A(F), Y) \cong  [J(A), \mathcal{C}](F, K_A(Y))

関手ΣAと関手KAが随伴関手ペアになります。

  •  K_A:\mathcal{C} \to [J(A), \mathcal{C}] \mbox{ in }{\bf CAT}
  •  \Sigma_A:[J(A), \mathcal{C}] \to \mathcal{C} \mbox{ in }{\bf CAT}
  •  \Sigma_A \dashv K_A

カン拡張によるパイ型とシグマ型

関手 KA:C → [J(A), C] が、関手 Δ!A:[J(1), C] → [J(A), C] と事実上同じであることを見ましょう。まずはΔの意味を説明する必要があります。

射 f:A → B in C があるとき、反レイフィケーション関手Jにより、関手 J(f):J(A) → J(B) in CAT が誘導されます。J(f) をプレ結合〈pre-compose〉することは、[J(B), C] → [J(A), C] という関手(関手圏のあいだの関手)を定義します。その関手を Δf とします*2

  •  \Delta_f(\mbox{-}) := J(f)\ast \mbox{-}
  •  \Delta_f:[J(B), \mathcal{C}] \to [J(A), \mathcal{C}] \mbox{ in }{\bf CAT}

引数〈argument〉が下付きだったり丸括弧だったりは、習慣や気まぐれで意味はありませんプログラミング言語だと、引数渡し構文が一種類だけのものがありますが、それはそれで見にくい(視認性が悪い)もんです。下付き・上付き・括弧・併置などをテキトーに(根拠なく)使い分けるのは視認性向上にはなります。

さて、C内で、Aから終対象1への唯一の射を !A:A → 1 in C とすると、これは J(!A):J(A) → J(1) in CAT を誘導し、さらにJ(!A)のプレ結合により次の関手(関手圏のあいだの関手)が作られます。

  •  \Delta_{!_A}:[J({\bf 1}), \mathcal{C}] \to [J(A), \mathcal{C}] \mbox{ in }{\bf CAT}

Δ!AとKAは、次の可換図式の意味で“事実上同じ”です。

\require{AMScd}
\begin{CD}
  [J({\bf 1}), \mathcal{C}] @>{\Delta_{!_A}}>> [J(A), \mathcal{C}] \\
  @V{\cong}VV                                  @| \\
  \mathcal{C}                 @>>{K_A}>        [J(A), \mathcal{C}]
\end{CD}\\
\mbox{commutes in }{\bf CAT}

KAの代わりにΔ!AとKAを使って先の“随伴を定義するホムセット同型”を書いてみます。

  •  [J(A), \mathcal{C}](\Delta_{!_A}(X), F) \cong [J({\bf 1}), \mathcal{C}](X, \Pi_A(F))
  •  [J({\bf 1}),\mathcal{C}](\Sigma_A(F), Y) \cong  [J(A), \mathcal{C}](F, \Delta_{!_A}(Y))

これを見ると、パイ型とシグマ型の新しい特徴付けが分かってきます。それは次のようです。

  •  \Pi_A(F) = Ran_{J(!_A)}(F)
  •  \Sigma_A(F) = Lan_{J(!_A)}(F)

つまり、J(!A)に沿ったFの右カン拡張がFのパイ型で、J(!A)に沿ったFの左カン拡張がFのシグマ型です。

となると、!Aという特別な射ではなくて、一般の射 f:A → B in C に沿った左右のカン拡張を考えてもいいでしょう。次のように定義します。

  •  \Pi_f(F) := Ran_{J(f)}(F)
  •  \Sigma_f(F) := Lan_{J(f)}(F)

fに沿ったパイ型/シグマ型を特徴付けるホムセット同型は次のようになります。

  •  [J(A), \mathcal{C}](\Delta_f(X), F) \cong [J(B), \mathcal{C}](X, \Pi_f(F))
  •  [J(B),\mathcal{C}](\Sigma_f(F), Y) \cong  [J(A), \mathcal{C}](F, \Delta_f(Y))

今述べたことを簡潔に言うと、

  •  \Sigma_f \dashv \Delta_f \dashv \Pi_f

あるいはもっと短く:

  •  \Sigma \dashv \Delta \dashv \Pi

以上は、単に定義を書いただけで、型理論的意味付けを与えていません。が、型理論(あるいは論理やデータベース)としても意味があると思えます。

*1:この絵を見ると、スパンと錐〈コーン〉が同じもので、コスパンと余錐〈ココーン〉が同じものだと分かりますね。

*2:Δfは、“J(f)による引き戻し”なので、J(f)とfを同一視して、短く f* とも書きます。