関手柱圏

F:C→D が関手のとき、関手Fの関手柱圏（functor cylinder category）というものを定義する。図形的な雰囲気が、CとDを上面と下面（底面）として、Fが母線群を形成する柱体を連想させるのでこの名前にした。Cylinder(F)、より詳しくは Cylinder(F:C→D) と書くことにする。

関手柱圏は、関手嫌悪への対策でもあるし、RPCの定式化でもある。

圏は有限表示（有限な生成グラフと有限の等式制約）を持つとする。圏そのものよりはむしろ表示を扱う。Gが表示で、Cat(G) = C とする。関手 C→D と表示 G→D を区別しないことにする。F:G→D が関手のとき、表示の圏のなかで直和 G + D を作る。次の操作をする。

• X∈|G| ごとに、i_X:X→F(X) という形式的な同型射を加える。i_X には逆 i_X^-1 がある。

この操作を施した表示を H とする。|H| = |G| + |D| で射（辺）と制約はi_Xの分だけ増えている。この表示Hから生成された圏 E := Cat(H) がFの関手柱圏Cylinder(F)となる。

E = Cylinder(F) には次の特徴がある。

1. Cは、自然にEの部分圏となる。C⊆E。
2. Dは、自然にEの部分圏となる。D⊆E。
3. F:C→D は、F:C→E とみなせる。
4. 埋め込み関手 C→E と F:C→E のあいだに自然同型がある。

[追記]もうひとつ重要な特徴がある。ただし、定式化が曖昧なんだけど。

M:D→A が、スピヴァックの意味のモデルインスタンスだとする。Aがアンビエント圏。F:C→D とMを結合した F;M = F^*M : C→A はもちろんC上のインスタンスになる。

それとは別に、MをE（Cylinder(F)）上の部分関手と考える。MはEの部分圏Dを定義域とするが、E全域への“自然な拡張”をM^~とする。

ここで自然な拡張の意味が明らかではない。稠密な部分圏とか十分な部分圏とかが関わるだろう。ともかくこのM^~が在るとして、それは、Mと、F;Mの埋め込み C⊆E に伴う前送りとの貼り合わせに一致すると思う。

[/追記]