レトラクション
図形的イメージは「レトラクションの起源（かな？）」に描きました。
計算論（再帰関数論）
よくわからんにょ。
デカルト圏の等式的計算
僕は絵を描いて（pictorial calculation）済ませてしまうことが多いのだけど、等式的計算（equational calculation）もやったほうがいいですね、念のため。等式的デカルト圏の話題は「なぜ『光が影を作ること』と『主張の一部を再主張すること』が関係するのか；あるいは、デカルト圏入門」でも扱っています（デカルト圏の基礎知識は「… デカルト圏入門」でだいたい間に合うと思います）。
記号法は（このブログ内で）通常使っているものを使います（π1、π2は射影*1）。idaを単にaと書くので注意。
デカルト圏の等式的公理：
- [1a] <f, g>;π1 = f （f:c→a, g:c→b）
- [1b] <f, g>;π2 = g （f:c→a, g:c→b）
- [2] <h;π1, h;π2> = h （h:c→a×b）
まずはペアリングの基本性質として（後で使わないけど）次を示しておきます。
- [3] <f, g> = <f', g'> ⇔ f = f' かつ g = g'
<f, g> = <f', g'>
---------------------------[両辺にπ1]
<f, g>;π1 = <f', g'>;π1
---------------------------[1a]
f = f'よって、<f, g> = <f', g'> ⇒ f = f'
同様にして <f, g> = <f', g'> ⇒ g = g'
これで「⇒」を示した。
逆向きは当たりまえ。
それと：
- [4] <π1a,b, π2a,b> = a×b
<π1a,b, π2a,b>
// 恒等射の性質
= <(a×b);π1, (a×b);π2>
// デカルト圏の公理[2]
= a×b
次に、ある種の分配律：
- [5] k:e→cとして、k;<f, g> = <k;f, k;g>
(k;<f, g>);π1 = k;(<f, g>;π1) = k;f （結合律と[1a]）
(k;<f, g>);π2 = k;(<f, g>;π2) = k;g （結合律と[1b]）
デカルト圏の公理[2]を使うと
k;<f, g> = <(k;<f, g>);π1, (k;<f, g>);π2> = <k;f, k;g>
以上を準備として：
- [6] <h, k>;(f×g) = <h;f, k;g>
- [7] a ≒ a', b ≒ b' ⇒ a×b ≒ a'×b' （≒は同型）
- [8] a×b ≒ b×a
- [9] (a×b)×c ≒ a×(b×a)
- [10] a ≒ a×t ≒ t×a （tは終対象）
[6] <h, k>;(f×g) = <h;f, k;g>
<h, k>;(f×g)
// f×gの定義
= <h, k>;<π1;f, π2;g>
// 分配律[5]
= <<h, k>;(π1;f), <h, k>;(π2;g)>
// ;の結合性
= <(<h, k>;π1);f, (<h, k>;π2);g>
// デカルト圏の公理[1a]と[1b]
= <h;f, k;g>
[7] a ≒ a', b ≒ b' ⇒ a×b ≒ a'×b' （≒は同型）
f, f', g, g' を、
f:a→a', f':a'→a, f;f' = a かつ f';f = a'
g:b→b', g':b'→b, g;g' = b かつ g';g = b'
だとする。f×g と f'×g' に関して、
(f×g);(f'×g')
// f×gの定義
= <π1;f, π2;g>;(f'×g')
// [6]
= <(π1;f);f', (π2;g);g'>
// ;の結合性
= <π1;(f;f'), π2;(g;g')>
// 仮定 f;f' = a, g;g' = b
= <π1;a π2;b>
// 恒等射の性質
= <π1, π2>
// [4]
= a×b同様にして、(f'×g');(f×g) = a'×b'
よって、 f×g と f'×g' により a×b ≒ a'×b'
[8] a×b ≒ b×a
<π2a,b, π1a,b>:a×b→b×a と
<π2b,a, π1b,a>:b×a→a×b に関して、<π2a,b, π1a,b>;<π2b,a, π1b,a>
// 分配律[4]
= <
<π2a,b, π1a,b>;π2b,a,
<π2a,b, π1a,b>;π1b,a
>
// デカルト圏の公理[1b]と[1a]
= <π1a,b, π2a,b>
// [4]
= a×b同様にして、<π2b,a, π1b,a>;<π2a,b, π1a,b> = b×a
よって、a×b ≒ b×a
[9]に関してはブレイディングの絵で済ませたいのだけど、我慢して等式的計算。要は組み合わせ計算です。
[9] (a×b)×c ≒ a×(b×a)
<π1a×b,c;π1a,b, <π1a×b,c;π2a,b, π2a×b,c>>:(a×b)×c→a×(b×c)
と
<<π1a,b×c, π2a,b×c;π1b,c>, π2a,b×c;π2b,c>:a×(b×c)→(a×b)×c
に関して、<π1;π1, <π1;π2, π2>>;<<π1, π2;π1>, π2;π2>
// 分配律[5]
= <
<π1;π1, <π1;π2, π2>>;<π1, π2;π1>
<π1;π1, <π1;π2, π2>>;π2;π2
>
// 第1成分に分配律[5]
// 第2成分にデカルト圏の公理[1b]と[1a]
= <
<
<π1;π1, <π1;π2, π2>>;π1,
<π1;π1, <π1;π2, π2>>;π2;π1
>,
π2
>
// 第1成分の“第1成分と第2成分”にデカルト圏の公理[1b]と[1a]
= <
<
π1;π1,
π1;π2
>,
π2
>
// 丁寧に書いてみる
= <
<π1a×b,c;π1a,b, π1a×b,c;π2a,b>,
π2a×b,c
>
// 第1成分にデカルト圏の公理[2]
= <π1a×b,c, π2a×b,c>
// [4]
= (a×b)×c同様にして、
<<π1, π2;π1>, π2;π2>;<π1;π1, <π1;π2, π2>> = a×(b×c)
よって、(a×b)×c ≒ a×(b×c)
[10]を示すために、次の2つを使います。tが終対象であることから、これらはほぼ自明でしょう。ビックリマークは、終対象への唯一の射です。
- [11a] f:x→t ならば f = !x
- [11b] h:x→a, !a:a→t に対して、h;!a = !x
[10] a ≒ a×t ≒ t×a （tは終対象）
<a, !a>:a→a×t と π1a,t:a×t→a に関して<a, !a>;π1
// デカルト圏の公理[1a]
= aπ1;<a, !a>
// 分配律[5]
= <π1;a, π1;!a>
// 恒等射の性質
= <π1, π1;!a>
// [11b]
= <π1, !a×t>
// [11a]
= <π1, π2>
// [4]
= a×tよって、a ≒ a×t
同様に、a ≒ t×a
僕がこんな計算をやってみるのは、川島隆太先生監修のゲームとかをやる人とたぶん同じ動機 :-)
*1:面倒なので、first/secondを区別する1と2を上付き／下付きにはしません。
