指標の工作
指標の圏が有限余完備であることが本質的。ただし、非モノイド的なので、モノイド積は定義できない。非モノイド的有限余完備圏。それと、ゴグエンのいうinclusiveで、やせた部分圏としてinclusionが定義されている。双対的にはprojectionだが、inclusioinと考えたほうが自然(余完備だから)。
有限余完備性から、融合和〈貼り合わせ | amalgamation | gluing | pasting | cofiber sum〉がある。injectionは埋め込みと言い換えてもいいだろう。新しい操作として、引き剥がし〈tear-off | rip-off | detach〉を考える。
- 埋め込み(包含) i:Δ→Σ, j:Δ→Γ を使った貼り合わせは Σ #i,j Γ と書く。
- 埋め込み(包含) k:Γ→Σ による引き剥がしを Γ ∸k Σ と書く。
ドットマイナスを使えないときは、- でも \でもかまわない。埋め込み k:Γ→Σ があると、これに伴う余スパン (i, j): Γ←Δ→(Σ ∸k Γ) が定義できる。この余スパンを使って貼り合わせをすると元に戻る。雑に書くと:
- (Σ ∸ Γ) # Γ = Σ
この等式(ほんとは同型)が、指標の圏におけるカリー同型の基礎となる。
これが一律に示せるわけではなくて、個別ケースの寄せ集めとして証明できる(はず)。これの証明が難しい(つうか、現状実行できない)のは、埋め込み、貼り合わせ、引き剥がし(特に引き剥がし)の定義がハッキリしてないから。
指標=コンピュータッド=箙 とみるとき、境界付き箙を考えてないせいだと思う。指標の圏を境界付き高次箙の圏とみなして、それが生成する高次圏をモデルと考える必要がある。
インスティチューションの意味でのモデル関手は、指標圏からドクトリン(構造付き圏の2-圏)への関手となるが、余デカルト閉構造をデカルト閉構造に写す。およそ、
- 〚Σ # Γ 〛 = 〚Σ〛×〚Γ〛
- 〚Σ ∸ Γ〛 = 〚Σ〛〚Γ〛
スローガンとしては、
- 足し算が掛け算に、引き算が指数ベキに写る
足し算/引き算は指標の工作であり、モデル側の指数ベキは関手圏で与えられる。