「論理や型理論の圏論的意味論 // 導出システムの圏と圏の圏」において、導出システム達を対象とする圏に触れました。しかし、導出システムのあいだの準同型射（それが圏の射となる）を素朴に考えていては、どうもうまくないようです。
導出システムは、複圏〈オペラッド〉と密接に関係があります。導出システムの代わりに、複圏が対象であるような圏をまずは考えてみます。複圏のあいだの射は、通常の準同型射ではなくて、もっとゆるい概念であるプレ準同型射とします。
複圏〈オペラッド〉を対象として、複圏のあいだのプレ準同型射を射とする圏が、導出システムの記述と分析にふさわしい気がします。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\hyp}{\text{－} }
%\newcommand{\Q}[1]{\text{'#1'}}
\newcommand{\T}[1]{\text{#1}}
\newcommand{\In}{ \text{ in } }
%\newcommand{\twoto}{\Rightarrow }
%\newcommand{\Imp}{\Rightarrow }
`$
内容：
圏のあいだのプレ準同型射
目的は複圏〈オペラッド〉ですが、手始めに圏のあいだのプレ準同型射を定義します。次の記法はいつもどおりです。
- 圏 $`\cat{C}`$
- 圏の対象の集合 $`\mrm{Obj}(\cat{C}) = |\cat{C}|`$
- 圏の射の集合 $`\mrm{Mor}(\cat{C})`$
- 射にその域を対応させる写像 $`\mrm{dom} = \mrm{dom}_\cat{C} : \mrm{Mor}(\cat{C})\to \mrm{Obj}(\cat{C})`$
- 射にその余域を対応させる写像 $`\mrm{cod} = \mrm{cod}_\cat{C} : \mrm{Mor}(\cat{C})\to \mrm{Obj}(\cat{C})`$
- ホムセット $`\mrm{Hom}_\cat{C}(\hyp, \hyp) = \cat{C}(\hyp, \hyp)`$
次のように定義をします。
$`\quad \mrm{Prof}(\cat{C}) := \mrm{Obj}(\cat{C})\times \mrm{Obj}(\cat{C})`$
$`\quad \mrm{bdry}_{\cat{C}} :=\langle \mrm{dom}_{\cat{C}}, \mrm{cod}_{\cat{C}} \rangle \;: \mrm{Mor}(\cat{C}) \to \mrm{Prof}(\cat{C})`$
$`\mrm{Prof}(\cat{C})`$ は、圏 $`\cat{C}`$ のプロファイルの集合〈set of profiles〉と呼びます。$`\mrm{bdry}`$ は境界〈boundary〉のことで、$`\mrm{dom}, \mrm{cod}`$ をひとまとめにした写像です。$`\mrm{bdry}_\cat{C}`$ は圏 $`\cat{C}`$ の境界写像〈boundary map〉と呼びます。射 $`f`$ に対する $`\mrm{bdry}(f)`$ は、$`f`$ の境界プロファイル〈boundary profile〉ですが、単に境界、あるいは単にプロファイルともいいます。
$`\cat{C}, \cat{D}`$ を小さい圏だとして、$`\cat{C}`$ から $`\cat{D}`$ へのプレ準同型射〈pre-homomorphism〉 $`F`$ とは、次の2つの写像のペアです。
$`\quad F_\mrm{prof} : \mrm{Prof}(\cat{C}) \to \mrm{Prof}(\cat{D}) \In \mbf{Set}`$
$`\quad F_\mrm{mor} : \mrm{Mor}(\cat{C}) \to \mrm{Mor}(\cat{D}) \In \mbf{Set}`$
プレ準同型射の条件〈法則 | 公理〉として、次の図式を可換にすることを要請します。
$`\quad \xymatrix{
\mrm{Mor}(\cat{C}) \ar[d]_{\mrm{bdry}_\cat{C}} \ar[r]^{F_\mrm{mor}}
& \mrm{Mor}(\cat{D}) \ar[d]^{\mrm{bdry}_\cat{D}}
\\
\mrm{Prof}(\cat{C}) \ar[r]^{F_\mrm{prof}}
& \mrm{Prof}(\cat{D})
}\\
\quad \text{commutative }\In \mbf{Set}
`$
プレ準同型射では、対象のあいだの写像は考えてません。代わりに、プロファイルのあいだの写像 $`F_\mrm{prof}`$ を考えます。また、プレ準同型射は、圏の結合〈composition | 合成〉や恒等射とは無関係です。プレ準同型射に関手性は要求していません。
プレ準同型射の事例を挙げます； $`\cat{C} = (\cat{C}, \times, \mbf{1}, [\hyp, \hyp])`$ をデカルト閉圏として、プレ準同型射 $`F: \cat{C} \to \cat{C}`$ を次のように定義します。
- $`F_\mrm{prof}( (A, B) ) := (\mbf{1}, [A, B])`$
- $`F_\mrm{mor}( f:A \to B ) := ( \hat{f} : \mbf{1} \to [A, B])`$ （$`\hat{f}`$ は、$`f`$ のカリー化）
小さい圏を対象として、圏のあいだのプレ準同型射を射とする圏を次のように書きます。
$`\quad {_1 \mbf{Cat}}^\mrm{pre}`$
- 先頭下付きの $`1`$ は、2-圏ではなくて、1-圏であることを示します。
- 右肩の $`\mrm{pre}`$ は、射が関手ではなくてプレ準同型射であることを示します。
複圏〈オペラッド〉のあいだのプレ準同型射
前節は、概念に慣れるための小手調べで、複圏〈オペラッド〉に対してプレ準同型射を定義するのが目的です。ここでは、「複圏」と「オペラッド」は完全に同義語として使います。
複圏〈オペラッド〉では、特有の用語法があります。
| 圏 | 複圏〈オペラッド〉 |
|---|---|
| 対象 | 色 |
| 射 | 複射 | オペレーター | オペレーション |
| 結合 | 複結合 | オペラッド結合 |
| 恒等射 | 恒等{複射 | オペレーター | オペレーション} |
ここでは、複圏〈オペラッド〉特有の用語法・記法は使わず、（若干紛らわしいのは承知ですが）圏と同じ用語法・記法にします。例えば、複射やオペレーターとは言わず、単に射と呼びます。
複圏 $`\cat{M}`$ のプロファイルの集合は次のように定義します。
$`\quad \mrm{Prof}(\cat{M}) := \mrm{List}(\mrm{Obj}(\cat{M}))\times \mrm{Obj}(\cat{M})`$
射 $`f`$ に対する境界プロファイル $`\mrm{bdry}(f)`$ は次の形です。
$`\quad ( (A_1, \cdots, A_n), B )`$
通常、矢印をペアの区切り記号にして次の形で書いています。
$`\quad ( (A_1, \cdots, A_n)\to B )`$
丸括弧は省略されることが多いです。
複圏 $`\cat{M}`$ のプロファイル（$`\mrm{Prof}(\cat{M})`$ の要素）をギリシャ文字一文字 $`\alpha, \beta`$ などで代表させることにします。例えば：
$`\quad \alpha = ( (A_1, \cdots, A_n), B )`$
ホムセットは次のように定義できます。
$`\text{For }\alpha = ( (A_1, \cdots, A_n), B ) \; \in \mrm{Prof}(\cat{M})\\
\quad \mrm{Hom}_\cat{M}(\alpha) = \cat{M}(\alpha) = \cat{M}( ( (A_1, \cdots, A_n), B ) ) \\
:= \{f\in \mrm{Mor}(\cat{M}) \mid \mrm{bdry}(f) = \alpha \}
`$
適宜丸括弧は省略します。
複圏の射 $`f\in \cat{M}(\alpha)`$ を、境界プロファイルを添えて次のように書きます。
$`\quad f : \alpha`$
$`\quad f : (A_1, \cdots, A_n) \to B`$
ここでも、適宜丸括弧の省略はします。
ホムセットは、境界写像の逆像ファミリーであることは心にとめておいてください。
$`\quad \mrm{Hom}_\cat{M} = {\mrm{bdry}_\cat{M}}^{-1} : \mrm{Prof}(\cat{M}) \to |\mbf{Set}|\In \mbf{SET}`$
$`\mrm{bdry}`$ と $`\mrm{Hom}`$ は、バンドル-ファミリー対応（「バンドル-ファミリー対応 再考」参照）の事例です。
2つの複圏 $`\cat{M},\cat{N}`$ のあいだのプレ準同型射は、圏の場合と同様に定義できます。プロファイルの集合のあいだの写像と、射の集合のあいだの写像のペアで可換性を満たすものです。プレ準同型射は、複圏の対象〈オペラッドの色〉には関与しないことが重要です。
複圏〈multicategory〉を対象として、プレ準同型射を射とする圏は次のように書きます。
$`\quad {_1\mbf{Multicat}}^\mrm{pre}`$
そしてそれから
導出システム〈演繹系〉のあいだの準同型射として、例えば、自然演繹システムをシーケント計算システムに埋め込みたいことがあります。そのような埋め込みは、複圏の通常の準同型射を使ってはうまく記述できません。
対象〈色〉に関与せず、ゆるい概念であるプレ準同型射を使えば、「自然演繹 → シーケント計算」の埋め込みもうまく記述できそうです。
