日記 (2018 年 6 月 27 日)
今後しばらく、 最近私が勉強している依存型の圏論的意味論についてまとめていこうと思う。 特に、 Jacobs†2 が提唱したファイブレーションと内包圏を用いたものに触れていくつもりである。 余力があれば他のモデルについてもまとめたいとは思っているが、 おそらく思っただけになると思う。
なお、 このまとめは日本語で書こうと思っているので、 各種概念の名称も日本語に翻訳していくつもりである。 ただし、 定訳がまだ存在していない概念名が多いので、 できるだけ他の文献で使われている訳語を採用しようとは思っているが、 見つからなかった場合は独自に訳語を当てる。
初めに、 基本的な道具であるファイブレーションを定義する。 これは Grothendieck†1 が降下理論の文脈で導入した概念だが、 型理論の文脈でも有用であることが分かり広く使われている。 定義のため、 まずはカルテシアン射に関する準備をする。
関手
言い換えれば、
カルテシアン射の普遍性によって、 関手で移した先が同じであるようなカルテシアン射は同型の違いを除いて高々 1 つしか存在しない。
関手
圏論でよくある普遍性を使う議論ですぐできるので、 ここでは省略する。
さて、 ファイブレーションは、 終域の圏の任意の射に対して、 そのカルテシアンな持ち上げをとることができる関手として定義される。
関手
命題 1.2 によって、 ファイブレーションに沿った持ち上げは同型の違いを除いて一意に定まる。
以降では、 ファイブレーションを表すときは矢印の上に丸を付けて
いくつかファイブレーションの例を挙げよう。 まず、 最も基本的なファイブレーションである終域ファイブレーションを紹介する。
圏
の対象は、 → の射 全体とする。f : X → Y の 2 つの対象 → の間の射は、 図式f : X → Y , f : X → Y を可換にするような射の組X X Y Y h f f k 全体とする。( h , k )
によって定義する。
このように作った圏
圏
カルテシアン性の定義と引き戻しの普遍性が同じであることを確認すれば良い。
圏
命題 1.5 より明らかである。
圏
もう 1 つの例として、 対象の族が作るファイブレーションを挙げておく。
圏
の対象は、 何らかの集合Fam ( ) で添字付けられたI の対象の族 全体とする。( X i ) i ∈ I の 2 つの対象Fam ( ) の間の射は、 写像( X i ) i ∈ I , ( Y j ) j ∈ J および各u : I → J に対するi ∈ I の射 の族の組f i : X i → Y u ( i ) の全体とする。( u , ( f i ) i ∈ I )
によって定義する。
この
圏
写像
圏
さて、 ファイブレーションと言うからにはファイバーを気にしたくなるが、 ここでのファイブレーションは圏から圏への関手なので、 ファイバーも圏になる。 これは以下のように定義される。
ファイブレーション
の対象は、 I の対象 であってX を満たすもの全体とする。p X = I の 2 つの対象 I の間の射は、X , Y の射 であってf : X → Y を満たすもの全体とする。p f = id I
として定義する。
この
このことから、 ファイブレーション
ファイブレーション
終域ファイブレーション
参考文献
- A. Grothendieck, M. Raynaud (1971) 『Revêtements étales et groupe fondamental』 Springer
- B. Jacobs (1999) 『Categorical Logic and Type Theory』 North Holland