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

日記 (2018 年 7 月 23 日)

これまでファイブレーションについての基本的な概念を定義してきた。 ここで、 ファイブレーションと密接な関係がある、 もしくはファイブレーションの別の捉え方とも考えられる、 別の概念について触れておく。

ファイブレーション p:󰒜→󰒙 があると、 󰒙 の各対象 I に対してその上のファイバー圏 󰒜I が定まるので、 ファイブレーションとはファイバー圏を集めたものとも見なすことができる。 しかし、 󰒙 の対象 I に対して何か圏が紐付けられていて、 そのような圏を全て集めたもの考えたければ、 わざわざファイバーなどを考えなくても、 単に 󰒙 の対象から圏への対応を作れば良いだけである。 このような考え方で圏の集まりを扱うのが、 以下に定義する添字付き圏である。

定義 3.1.

圏 󰒙 に対して、

  • 󰒙 の対象 I に対し、 圏 ΨI が定まっている。
  • 󰒙 の射 u:I→J に対し、 関手 Ψu:ΨJ→ΨI が定まっている。
  • 󰒙 の対象 I に対し、 自然同型 ηI:idΨI⇒ΨidI が存在する。
  • 󰒙 の射 u:I→J,v:J→K に対し、 自然同型 μuv:Ψu∘Ψv⇒Ψ(v∘u) が存在する。

となっているとする。 さらに、 任意の 󰒙 の射 u:I→J,v:J→K,w:K→L に対し、 ΨuΨidI∘ΨuΨuΨu∘ΨidIηI∗ΨuΨu∗ηIμidI,uμu,idI Ψu∘Ψv∘ΨwΨu∘Ψ(w∘v)Ψ(v∘u)∘ΨwΨ(w∘v∘u)Ψu∗μvwμuv∗Ψwμu,w∘vμv∘u,w が可換であるとする。 このとき Ψ:󰒙∘→Cat と書き、 これを 󰒙 上の 「添字付き圏 (indexed category)」 という。

2-射として恒等射のみを考えることで普通の圏 󰒙∘ を 2-圏だと思えば、 添字付き圏 Ψ:󰒙∘→Cat とは単なる 2-圏の間の擬関手のことである。

最初に述べたように、 ファイブレーション p:󰒜→󰒙 があると、 そのファイバー圏をとることによって 󰒙 の対象に圏を対応させることができる。 これを添字付き圏に拡張するにはファイバー圏の間の関手を作る必要があるが、 それを行うには、 7 月 17 日でも触れたように持ち上げを 1 つ選んでおく必要があるので、 p は少なくとも劈開ファイブレーションである必要がある。

命題 3.2.

劈開ファイブレーション p:󰒜→󰒙 に対し、 ファイバー圏を対応させる関係 󰂡p: 󰒙∘ ⟶ Cat I ⟼ 󰒜I u ⟼ u∗ は添字付き圏を定める。

証明.

上で定められた関係に対して、 添字付き圏の公理が全て満たされていることを確かめれば良い。 持ち上げの普遍性を使うだけでできるので面倒なだけで何も難しくないが、 全部省略してしまうのも味気ないので一部分だけ確かめておこう。

󰒙 の射 u:I→J,v:J→K および 󰒜K の対象 Z に対し、 󰒜 の射 (μuv)Z:u∗v∗Z→(v∘u)∗Z を、 図式 u∗v∗Zv∗Z(v∘u)∗ZZ(μuv)Zuv∗ZvZv∘uZ を可換にする破線の射として定める。 この (v∘u)∗Z は v∘uZ のカルテシアン性によって一意に定まる射である。 また、 uv∗Z∘vZ もカルテシアンであるから、 (μuv)Z の逆向きの射も誘導され、 分解の一意性によって (μuv)Z とその射は互いに逆写像である。

このように作られた同型射 (μuv)Z:u∗v∗Z→(v∘u)∗Z は Z に関して自然である。 これは以下のように確かめられる。 任意の射 f:Z→Z󰎘 に対し、 図式 u∗v∗Zv∗Zu∗v∗Z󰎘v∗Z󰎘(v∘u)∗ZZ(v∘u)∗Z󰎘Z󰎘uv∗Z(μuv)Zu∗v∗fvZv∗fuv∗Z󰎘(μuv)Z󰎘vZ󰎘v∘uZ(v∘u)∗ffv∘uZ󰎘 を考える。 上面と底面と右の斜めの面は u∗ などの定義によって可換で、 背面と前面は (μuv)Z などの定義から可換である。 問題は左の面だが、 他の面の可換性から、 左の面を構成している 2 つの射はともに v∘uZ󰎘 のカルテシアン性によって誘導される u∗v∗Z からの射になっている。 したがって、 分解の一意性から、 左の面を構成する 2 つの射は等しい。 以上によって (μuv)Z の Z に関する自然性が示され、 自然同型 μuv:u∗∘v∗⇒(v∘u)∗ が得られた。

󰒙 の対象 I に対しての自然同型 ηI:id󰒜I⇒idI∗ も同様に構成できる。 添字付き圏の残りの条件に関しても、 分解の一意性を用いて証明できる。

さて、 すると、 逆に添字付き圏から劈開ファイブレーションを作れるのかが気になってくるが、 実はこちらも可能である。

定義 3.3.

添字付き圏 Ψ:󰒙∘→Cat に対し、 圏 ∫Ψ を

  • ∫Ψ の対象は、 󰒙 の対象 I と ΨI の対象 X の組 (I,X) とする。
  • ∫Ψ の 2 つの対象 (I,X),(J,Y) の間の射は、 󰒙 の射 u:I→J と ΨI の射 f:X→(Ψu)Y の組 (u,f) とする。
  • ∫Ψ の 2 つの射 (u,f):(I,X)→(J,Y),(v,g):(J,Y)→(K,Z) の合成は、 X(Ψu)Y(Ψu∘Ψv)Z(Ψ(v∘u))Zf(Ψu)g(μuv)Z を h とするとき、 (v∘u,h) であるとする。

によって定める。 この圏を Ψ による 「Grothendieck 構成 (— construction)」 という。

命題 3.4.

添字付き圏 Ψ:󰒙∘→Cat に対し、 関手 󰂡Ψ: ∫Ψ ⟶ 󰒙 (I,X) ⟼ I を考える。 終域を (J,Y) とする射 u:I→J の持ち上げとして (u,id(Ψu)Y):(I,(Ψu)Y)→(J,Y) を選ぶことにより、 󰂡Ψ は劈開ファイブレーションになる。

劈開の選び方が、 7 月 17 日で例に挙げた、 ある圏 󰒚 の族ファイブレーション ind:Fam(󰒚)󰔊→Set と似ていることにも注目すべきだろう。

証明.

任意の 󰒙 の射 u:I→J と ΨJ の対象 Y に対し、 (u,id(Ψu)Y):(I,(Ψu)Y)→(J,Y) がカルテシアンであることを示せば良い。 そのためには、 任意の ∫Ψ の射 (v,g):(K,Z)→(J,Y) と 󰒙 の射 w:K→I について、 KIJwvu(K,Z)(I,(Ψu)Y)(J,Y)(v,g)(u,id)♤ の左側の図式を可換であるとき、 右側の図式を可換にする破線の射であって、 p によって w に移るものが一意に存在することを示せば良い。

まず、 そのような破線の射が p によって w に移ることから、 破線の射の第 1 成分は w でなければならない。 また、 第 2 成分は右側の図式の可換性から、 Z(Ψw∘Ψu)Y(Ψw∘Ψu)Y(Ψv)Y(Ψw)id(μwv)Y が g に等しいような破線の射である必要があるが、 (Ψw)id(Ψu)Y=id(Ψw∘Ψu)Y であり、 さらに (μwv)Y は同型射だから、 そのような射は (μwv)Y−1∘g しかない。 よって、 (w,(μwv)Y−1∘g):(K,Z)→(I,(Ψu)Y) は、 p で w に移り式 ♤ の右側の図式を可換にする唯一の射である。

以上によって、 劈開ファイブレーションと添字付き圏は相互に構成できることが分かった。 ところで、 劈開ファイブレーションより性質の良い分裂ファイブレーションというものがあったが、 添字付き圏の方でこれに対応するものがどういうものかということにも触れておこう。

定義 3.5.

添字付き圏 Ψ:󰒙∘→Cat について、 上記の定義の記号で ηI および μuv たちが全て恒等な自然変換であるとき、 Ψ は 「厳密 (strict)」 であるという。

命題 3.6.

劈開ファイブレーション p:󰒜→󰒙 に対し、 p が分裂ならば 󰂡p は厳密である。

命題 3.7.

添字付き圏 Ψ:󰒙∘→Cat に対し、 Ψ が厳密ならば 󰂡Ψ は分裂である。

以上により、 分裂ファイブレーションと厳密添字付き圏は相互に構成可能であって、 少し計算すると分かるが、 この構成は同型の違いを除いて互いに逆になっている。 したがって、 分裂ファイブレーションが成す圏と厳密添字付き圏が成す圏は圏同値であることになるが、 これは 2-圏同値にまで拡張できる。 この辺りの定式化はまた次の記事で行いたい。

参考文献

  1. B. Jacobs (1999) 『Categorical Logic and Type Theory』 North Holland