ΤΑ ΖΙΦΙΛΟΥΒΙΒΛΙΑ

日記 (2018 年 6 月 27 日)

今後しばらく、 最近私が勉強している依存型の圏論的意味論についてまとめていこうと思う。 特に、 Jacobs†2 が提唱したファイブレーションと内包圏を用いたものに触れていくつもりである。 余力があれば他のモデルについてもまとめたいとは思っているが、 おそらく思っただけになると思う。

なお、 このまとめは日本語で書こうと思っているので、 各種概念の名称も日本語に翻訳していくつもりである。 ただし、 定訳がまだ存在していない概念名が多いので、 できるだけ他の文献で使われている訳語を採用しようとは思っているが、 見つからなかった場合は独自に訳語を当てる。

初めに、 基本的な道具であるファイブレーションを定義する。 これは Grothendieck†1 が降下理論の文脈で導入した概念だが、 型理論の文脈でも有用であることが分かり広く使われている。 定義のため、 まずはカルテシアン射に関する準備をする。

定義 1.1.

関手 p:󰒜→󰒙 を考える。 󰒜 の射 f:X→Y が以下の条件を満たすとする。 すなわち、 󰒜 の射 g:Z→Y であって、 ある 󰒙 の射 w:pZ→pX によって pg=pf∘w と分解できるものに対し、 󰒜 の射 h:Z→X であって、 ph=w かつ f∘h=g をともに満たすものが唯一存在する。 このとき、 f は p に関して 「カルテシアン (cartesian)」 であるという。 図式では、 ZXYhgfpZpXpYwpgpf と表せる。

言い換えれば、 f:X→Y がカルテシアンであるというのは、 何らかの g:Z→Y が、 p で移した先の 󰒙 で f を経由するなら、 元の 󰒜 でも同様に f を経由する、 ということである。

カルテシアン射の普遍性によって、 関手で移した先が同じであるようなカルテシアン射は同型の違いを除いて高々 1 つしか存在しない。

命題 1.2.

関手 p:󰒜→󰒙 を考える。 󰒜 の射 f:X→Y,f󰎘:X󰎘→Y がともにカルテシアンであって pf=pf󰎘 を満たすならば、 ある 󰒜 の同型射 φ:X→X󰎘 が存在して、 f󰎘∘φ=f となる。

証明.

圏論でよくある普遍性を使う議論ですぐできるので、 ここでは省略する。

さて、 ファイブレーションは、 終域の圏の任意の射に対して、 そのカルテシアンな持ち上げをとることができる関手として定義される。

定義 1.3.

関手 p:󰒜→󰒙 に対し、 任意の 󰒙 の射 u:I→J および 󰒜 の対象 Y で pY=J を満たすものに対し、 󰒜 のカルテシアン射 f:X→Y であって pf=u を満たすものが存在するとする。 このとき、 p を 「ファイブレーション (fibration)」 という。 また、 f を p に沿った u の 「持ち上げ (lifting)」 といい、 f の定義域を u∗Y で表し、 f 自身は uY で表す。

命題 1.2 によって、 ファイブレーションに沿った持ち上げは同型の違いを除いて一意に定まる。

以降では、 ファイブレーションを表すときは矢印の上に丸を付けて p:󰒜󰔊→󰒙 のように表すことにする。

いくつかファイブレーションの例を挙げよう。 まず、 最も基本的なファイブレーションである終域ファイブレーションを紹介する。

定義 1.4.

圏 󰒚 に対し、 圏 󰒚→ を、

  • 󰒚→ の対象は、 󰒚 の射 f:X→Y 全体とする。
  • 󰒚→ の 2 つの対象 f:X→Y,f󰎘:X󰎘→Y󰎘 の間の射は、 図式 XX󰎘YYhff󰎘k を可換にするような射の組 (h,k) 全体とする。

によって定義する。

このように作った圏 󰒚→ に対し、 cod: 󰒚→ ⟶ 󰒚 ❲f:X→Y❳ ⟼ X という関手が考えられる。 すると、 この関手に関するカルテシアン射は引き戻しとちょうど対応する。

命題 1.5.

圏 󰒚 をとる。 図式 XX󰎘YYhff󰎘k によって定められる 󰒚→ の射 (h,k):f→f󰎘 に対し、 (h,k) が cod:󰒚→→󰒚 に関してカルテシアンであるための必要十分条件は、 上の図式が引き戻しとなることである。

証明.

カルテシアン性の定義と引き戻しの普遍性が同じであることを確認すれば良い。

命題 1.6.

圏 󰒚 をとる。 関手 cod:󰒚→→󰒚 がファイブレーションであるための必要十分条件は、 󰒚 が引き戻しをもつことである。

証明.

命題 1.5 より明らかである。

定義 1.7.

圏 󰒚 は引き戻しをもつとする。 ファイブレーション cod:󰒚→󰔊→󰒚 を 󰒚 に付随する 「終域ファイブレーション (codomain fibration)」 という。

もう 1 つの例として、 対象の族が作るファイブレーションを挙げておく。

定義 1.8.

圏 󰒚 に対し、 圏 Fam(󰒚) を、

  • Fam(󰒚) の対象は、 何らかの集合 I で添字付けられた 󰒚 の対象の族 (Xi)i∈I 全体とする。
  • Fam(󰒚) の 2 つの対象 (Xi)i∈I,(Yj)j∈J の間の射は、 写像 u:I→J および各 i∈I に対する 󰒚 の射 fi:Xi→Yu(i) の族の組 (u,(fi)i∈I) の全体とする。

によって定義する。

この Fam(󰒚) に対しては、 ind: Fam(󰒚) ⟶ Set (Xi)i∈I ⟼ I という関手が考えられ、 これはファイブレーションになる。

命題 1.9.

圏 󰒚 をとる。 関手 ind:Fam(󰒚)→Set は常にファイブレーションである。

証明.

写像 u:I→J と対象族 (Yj)j∈J に対し、 終域を (Yj)j∈J とするような u の持ち上げが存在すれば良い。 そのような射は、 (u,(idu(i))i∈I):(Yu(i))i∈I→(Yj)j∈J によって与えられる。

定義 1.10.

圏 󰒚 をとる。 ファイブレーション ind:Fam(󰒚)󰔊→Set を 󰒚 に付随する 「族ファイブレーション (family fibration)」 という。

さて、 ファイブレーションと言うからにはファイバーを気にしたくなるが、 ここでのファイブレーションは圏から圏への関手なので、 ファイバーも圏になる。 これは以下のように定義される。

定義 1.11.

ファイブレーション p:󰒜󰔊→󰒙 を考える。 󰒙 の各対象 I に対し、 圏 󰒜I を、

  • 󰒜I の対象は、 󰒜 の対象 X であって pX=I を満たすもの全体とする。
  • 󰒜I の 2 つの対象 X,Y の間の射は、 󰒜 の射 f:X→Y であって pf=idI を満たすもの全体とする。

として定義する。 この 󰒜I を I 上の 「ファイバー圏 (fibre category)」 という。

このことから、 ファイブレーション p:󰒜󰔊→󰒙 があるとき、 󰒜 の対象 X で pX=I を満たすもの (すなわち 󰒜I の対象) を、 単に I 上の対象と呼ぶことがある。 また、 何らかのファイバー圏に入る射に関しては、 以下の用語も用意しておく。

定義 1.12.

ファイブレーション p:󰒜󰔊→󰒙 を考える。 󰒜 の射 f:X→Y が p によって恒等射に移るとき、 f は 「垂直 (vertical)」 であるという。

終域ファイブレーション cod:󰒚→→󰒚 を考えると、 ある対象 I の上のファイバー圏 󰒚→I はスライス圏 󰒚/I に一致していることが分かる。 また、 族ファイブレーション ind:Fam(󰒚)→Set に関しては、 集合 I 上のファイバー圏 Fam(󰒚)I は関手圏 󰒚I に一致している。

参考文献

  1. A. Grothendieck, M. Raynaud (1971) 『Revêtements étales et groupe fondamental』 Springer
  2. B. Jacobs (1999) 『Categorical Logic and Type Theory』 North Holland