日記 (2018 年 7 月 17 日)

ファイブレーション p:󰒜󰔊→󰒙 を固定する。 このとき、 任意の 󰒙 の射 u:I→J に対し、 持ち上げ先の終域となる 󰒜J の対象 Y を指定すれば、 持ち上げ uY:u∗Y→Y が存在する。 命題 1.2 により、 この持ち上げは同型の違いを除けば一意に定まるが、 同型分の自由度はある。 型理論の意味論を作るにあたっては、 本当に等しいのか同型なのかを明確に区別する必要があるため、 これでは少し不便である。 そこで、 各 u と Y に対し、 その持ち上げ uY を 1 つ選ぶことを考える。

より明確には、 ファイブレーションと持ち上げの選択の組 (p,(uY)u,Y) を劈開ファイブレーションというのである。 したがって、 ファイブレーションそのものが同じでも持ち上げの選択が異なっていれば、 劈開ファイブレーションとしては別物だと考える。

なお、 この日本語訳は私独自のものである。 ちなみに、 一般用語としての劈開とは、 光ファイバーを綺麗に切断するために入れる切れ込みや、 結晶のある特定方向へ割れやすい性質のことである。

さて、 劈開ファイブレーション p:󰒜󰔊→󰒙 と 󰒙 の射 u:I→J があると、 󰒜J の対象 Y に対して、 選ばれた持ち上げの始域 u∗Y を対応させることができる。 この対応は関手に拡張することができる。 実際、 射 f:Y→Y󰎘 に対し、 uY のカルテシアン性によって、 図式 u∗YYu∗Y󰎘Y󰎘u∗fuYfuY󰎘 を可換にする破線の射が一意に存在する。 以上により、 射 u:I→J は、 ファイバー圏の間の関手 u∗: 󰒜J ⟶ 󰒜I Y ⟼ u∗Y を誘導する。 この関手は型理論における代入と密接な関係がある。

持ち上げを 1 つ定めることで、 あるファイバー圏から別のファイバー圏への関手を作ることができたわけだが、 これだけでは少し困ることがある。 例えば、 劈開ファイブレーション p:󰒜󰔊→󰒙 を固定して、 2 つの 󰒙 の射 u:I→J,v:J→K があるとしよう。 上のような方法で 󰒜K から 󰒜I に関手を作ろうとすると、 まず v による 󰒜J への関手と u による 󰒜I への関手を別々に作って合成する方法と、 v∘u によって一気に 󰒜I への関手を作る方法の、 2 種類が考えられる。 持ち上げは同型の違いを除いて一意なので、 それぞれの方法で作った関手は同型の違いを除けば一致するが、 完全に一致する保証はない。 より具体的には、 各 󰒜K の対象 Z に対し、 図式 u∗v∗Zv∗Z(v∘u)∗ZXuv∗ZvZv∘uZ において誘導される破線の射は、 同型射ではあるが恒等射ではない。 先程も少し触れたように、 u∗ という形の関手は型理論の代入の解釈をするときに出てくるのだが、 上の破線の射が恒等射ではないということは、 代入を 2 回に分けて行うのと 1 回で一気に行うのでは異なる結果になってしまうということである。 これは、 同じ項は同型ではなく完全に等しい対象に解釈したいという理念に反してしまう。 そこで、 以下のような定義をする。

6 月 27 日で例として挙げたいくつかのファイブレーションについて、 持ち上げの選択の代表例を挙げておく。

圏 󰒚 に付随する族ファイブレーション ind:Fam(󰒚)󰔊→Set を考える。 終域を (Yj)j∈J とする写像 u:I→J の持ち上げの代表例として (u,(idu(i))i∈I):(Yu(i))i∈I→(Yj)j∈J がとれる。 この選択に関して、 ind は分裂ファイブレーションになる。

次に、 Set 上の終域ファイブレーション cod:Set→󰔊→Set を考える。 写像 u:I→J の持ち上げは、 引き戻し図式 I×JYYIJfu で与えられるのであった。 Set での引き戻しの選び方として代表的なのは、 I×JY={(i,y)∈I×Y∣u(i)=f(y)} であろうが、 この持ち上げの選択では分裂ファイブレーションにならない。 実際、 別の射 v:J→K に対し、 2 つの引き戻し I×KYYIJKfuvI×J(J×KY)J×KYYIJKfuv を上の方法で計算すると、 それぞれ I×KY = {(i,y)∈I×Y∣v(u(i))=f(y)} I×J(J×KY) = {(i,(j,y))∈I×(J×Y)∣u(i)=j,v(j)=f(y)} となり、 確かに同型ではあるが別物である。 なお、 合成と厳密に可換な Set での引き戻しの選び方が存在するかは、 どうやら未解決らしい。

参考文献

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