「順序のあるなし」、「順序がいつどこで導入されたか」などは、意識する必要がある。
明示的コアージョン、暗示的〈暗黙の〉コアージョンについては「ブール型と自然数型の明示的なコアージョン」参照。明示的コアージョンは煩雑になるので「やれ」とは言わないが、書く側は意識する必要はある。暗示的コアージョンが「読む側で解決可能か?」と考えて、「困難」と判断したら、なにか対処する。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\hyp}{\text{-} }
\newcommand{\Imp}{\Rightarrow }
\newcommand{\In}{ \text{ in } }
\newcommand{\T}[1]{ \text{#1} }
`$
よくあるコアージョン
| 名前 | 短縮形 | $`\T{圏}`$ | 備考 |
|---|---|---|---|
| set | set | $`\mbf{Set}`$ | |
| ordered set | ord | $`\mbf{Ord}`$ | |
| vector space | vect | $`\mbf{Vect}`$ | スカラーは実数 |
| ordered vector space | ovect | $`\mbf{OVect}`$ | リース空間 |
強制可能関係〈coercible relation〉:
- $`\T{set} \Imp \T{ord}`$ (離散順序)
- $`\T{ord} \Imp \T{set}`$ (忘却)
- $`\T{ovect} \Imp \T{ord}`$ (忘却)
- $`\T{ovect} \Imp \T{vect}`$ (忘却)
強制可能性の全体はコアージョングラフになる。が、一般的には推移性が保証されないので、グラフから順序集合〈やせた圏〉は作れない。タチが良いコアージョングラフが順序集合になる〈順序集合を生成できる〉ことはある。
書き方:
- $`(X \T{ is xxx})`$ は、「$`X`$ は本来 $`\T{xxx}`$ である」
- $`(X \T{ as xxx})`$ は、「$`X`$ は強制により $`\T{xxx}`$ とみなす」
- 暗黙のコアージョンを使わない約束なら、単なる $`X`$ は“本来の型”と解釈する。
自然数達に本来的に順序があるとするなら、
- $`\mbf{N}`$ は順序集合(大小順序)
- $`(\mbf{N}\T{ as set})`$ は集合(順序集合の台集合)
自然数達は本来的に集合だとするなら、
- $`\mbf{N}`$ は集合
- $`(\mbf{N}\T{ as ord})`$ は離散順序集合
規則的コアージョンとアドホック・コアージョン
通常「パラメトリック vs. アドホック」と言うが、ここでは「規則的 vs. アドホック」にする。
通常の記号運用では、「$`\mbf{N}`$ は集合」だとしても、「$`(\mbf{N}\T{ as ord})`$ は離散順序集合」とはしない。$`(\mbf{N}\T{ as ord})`$ は大小順序を考える。つまり、「任意の集合は離散順序集合とみなせる」という一般的な規則でコアージョンしないで、自然数固有の例外的コアージョン(アドホック・コアージョン)を適用している。
アドホック・コアージョンは、
- 自然数の順序って言ったら、そりゃ大小順序でしょう
という“常識”を記述している。
暗黙に想定するコアージョングラフには、
- 一般的な規則を記述するコアージョングラフ
- アドホック規則〈特有な例外規則〉を記述するコアージョングラフ
があって、アドホック規則が優先される。
コアージョングラフは複雑で(習慣的・恣意的アドホック・コアージョンが入るので)合理性を持たない。しかも暗黙化される。暗黙なので、共有・合意が困難。我々の理解やコミュニケーションの障害になる。
内部ホムとコアージョン
圏 $`\cat{C}`$ の内部ホムを $`[\hyp, \hyp]_{\cat{C}}`$ とする。
- $`[\hyp, \hyp]_\mbf{Set}`$ は、単なる関数集合。
- $`[\hyp, \hyp]_\mbf{Ord}`$ は、順序保存関数の集合に“関数のあいだの順序”を入れる。
- $`[\hyp, \hyp]_\mbf{Vect}`$ は、線形写像の集合に“関数の足し算・スカラー倍”を入れる。
- $`[\hyp, \hyp]_\mbf{OVect}`$ は、ベクトル空間 $`[(\hyp \T{ as vect}), (\hyp \T{ as vect})]_\mbf{Vect}`$ の正錐として、正錐を保存する写像達の集合を指定した順序ベクトル空間。
例えば、$`A`$ が集合で、$`V`$ が順序ベクトル空間のとき、$`[A, V]`$ の解釈は色々ある。アドホック規則があれば、$`(A \T{ as ord})`$ が離散順序とは限らない。一般的な規則で $`(A \T{ as vect})`$ は自由生成ベクトル空間だとして、$`(A \T{ as ovect})`$ は“第一象限”を正錐とする順序ベクトル空間とする。
- $`[A, (V \T{ as set})]_{\mbf{Set}}`$
- $`[(A \T{ as ord}), (\T{V as ord})]_{\mbf{Ord}}`$
- $`[(A \T{ as vect}), (V \T{ as vect})]_{\mbf{Vect}}`$
- $`[(A \T{ as ovect}), V]_{\mbf{OVect}}`$
- $`([(A \T{ as ord}), (V \T{ as ord})]_{\mbf{Ord}} \T{ as set})`$
$`[X, Y]`$ と書いたとき意識すべきことは:
- ブラケットはどこの内部ホムか?
- $`X, Y`$ にどんなコアージョンを施しているか/いないか?
- $`[X, Y]`$ をさらにコアージョンしているか?