「モノイド閉圏の事例」はシリーズ記事になる予定です（何回になるかは不明）。定義と命題は書きますが、記述はかなりラフなものとなり、解説は最小限、または省略される（解説なし）かも知れません。（[追記]最終回の記事： モノイド閉圏の事例： オシマイ - (2nd) 檜山正幸のキマイラ飼育記[/追記]）
ドラフト状態で公開するので、後からの変更が激しくなるでしょう。単一の記事内での変更に留まらず、記事の構成が大幅に変化するかも知れません -- それは、記述・投稿の時間順序が論理的順序にはならないと思うからです。
内容：
この事例について
モノイド閉圏〈monoidal closed category | 閉モノイド圏 | closed monoidal category〉の事例を提供します。この事例の名前（固有名）をSGMC（Simple Graphs with Monoidal Closed structure）とします。名前から想像できるように、SGMCのベースとなる圏（台圏）は単純グラフの圏SGです。
単純グラフの圏SGは、比較的簡単で扱いやすい圏ですが、その上にモノイド閉構造を載せたSGMCはあまり簡単ではありません。構造の具体的な定義や具体的な計算に手間がかかるのです。導入までの時間がかかり過ぎる点では、モノイド閉圏の学習用の事例には向いていません。
一方で、計算をガッツリ練習したい人には有意義な事例だと思います。具体的な計算をするための計算デバイス*1が必要なので、計算デバイスの構成も一連の記事内で扱います。紹介する計算デバイス（ラムダ計算の変種）が最良の計算手法かどうか分かりませんが、必要な計算は実行できます。
具体的な計算は計算用紙を消費するだけで面白くはありません。ひたすらドブ板計算です。圏論ではドブ板計算に頼る場面は思いの外多く、2008年の記事で「圏論は、ほぼ計算だけ」と言ってます（ちょっと言い過ぎたけど）。
[追記]これより下はもはやあまり意味がない。引き続く記事内に定義と記述がある。[/追記]
用語と記法
二項演算子記号とコンビネータの記号
| 名称 | 図式順記法 | 反図式順記法 | 備考 |
|---|---|---|---|
| 適用 | . （ドット） | -(-) | |
| 結合 | ; | |
|
| モノイド積 | □ | □ | 同じ |
| ヒゲ結合 | ; | |
オーバーロード |
| 右カリー化 | rΦ | いつもは rΛ | |
| 左カリー化 | ℓΦ | いつもは ℓΛ | |
| 右反カリー化 | rΨ | いつもは rΓ | |
| 左反カリー化 | ℓΨ | いつもは ℓΓ |
内部二項演算子記号と内部コンビネータの記号
| 図式順外部演算 | 図式順内部演算 | 反図式順外部演算 | 反図式順内部演算 |
|---|---|---|---|
| . | ->- （into と読む） | -(-) | -<-> |
| ; | |
|
|
| rΦ | rφ | ||
| ℓΦ | ℓφ | ||
| rΨ | rψ | ||
| ℓΨ | ℓψ |
二項演算子記号の使用目的
| 記号 | 使用目的 |
|---|---|
| ., -(-) | 写像〈射〉の値, 関手の値, 自然変換の値〈成分〉 |
| ;, |
射の結合, 自然変換の縦結合 |
| *, ・ | 関手の結合, 自然変換の横結合 |
| (-)^ | bump-upオペレーター |
露骨な表示
随伴系の単位と余単位の露骨な〈陽な | explicit〉表示をメモしておきます。
対象 A∈|SG| が定義する随伴系 AΣ の単位 Aη、ただし、左肩のAは省略。
- η := Aη （略記）
η::SG^⇒[A, -□A]:SG→SG
X.η:X→[A, X□A]
:= (
λ0x∈X.(
λ0∈A. (x, a) ∈X□A
ALSO
λ1(a→a')∈A. (x, a→a') ∈X□A
)
ALSO
λ1(x→x')∈X.(
λ01a∈A. (x, a)→(x', a) ∈X□A
)
)
対象 A∈|SG| が定義する随伴系 AΣ の余単位 Aε、ただし、左肩のAは省略。
- ε := Aε （略記）
ε::[A, -]□A⇒SG^:SG→SG
X.ε:[A, X]□A→X
:= (
λ0(f, a)∈[A, X]□A. f(a) ∈X
ALSO
λ1(f⇒f', a)∈[A, X]□A. (f⇒f')a ∈X
OR
λ1(f, a→a')∈[A, X]□A. f(a→a') ∈X
)
*1:デバイスは、もちろんハードウェアのことではありません。仕掛け、からくり、道具立て、といった意味です。メカニズム、マシーナリー、とかも言います。
