ベクトル空間のインデックス構造とスカラー構造続き - (保存用) 檜山正幸のキマイラ飼育記メモ編

ネームとコネームに関しては、

コンパクト閉圏と絵算で理解する線形代数とシーケント計算（入り口だけ） - 檜山正幸のキマイラ飼育記

「f, ^∩f, f_∪ の三位一体」を基礎に据えて、コンパクト論理のシーケント計算を道具にして線形代数（の初歩）を展開するのは面白いなー、と思っています。そのことをチャント書いたことはないので、まー、いつか書くかも。

上記の記事では、ev:A $\otimes$ A^*→I なので左右の順序（テンソル積の順序）が逆になっている。右上ベンディングじゃなくて、左上ベンディング。

基底に関しては：

a:I→X が基底
Iが基底のインデックス集合
Im(a) = {a(i)∈X | i∈I} を基底集合
aを基底集合のインデキシング
インデキシングが包含写像である基底をダイレクト基底
Iが[n]である基底を番号基底〈numbered basis〉、インデキシングを番号インデキシング、または番号付け／ナンバリング
基底のインデキシングの線形拡張をフレーム、ただし、次の別用法が考えられる。
- フレーム＝基底集合
- フレーム＝番号基底
- フレーム＝番号基底の線形拡張
フレームの逆写像を逆フレーム
フレームと逆フレームを使った表示を同伴射〈associated/assigned morphism〉

コンパクト論理との関係

構造操作〈規則〉として、換（置換群の作用、テンソル積の対称性）
構造操作として、Iと¬Iに関する単位増、単位現（単位に対する右単位律と左単位律）

公理命題または公理シーケント

A → A 恒等
(¬A, A →) 矛盾＝ev
(→ A, ¬A) 排中律＝coev
¬¬A → A と A → ¬¬A 二重否定＝ジェー＝ゲルファント変換
I → ¬I 禅論理の原理単位のシャー

推論規則

 Γ → Δ   Φ → Ψ
 -------------------[マージ＝空カット]
 Γ, Φ → Δ, Ψ

 Γ, A → Δ
 ---------------[否定]
 Γ → ¬A, Δ

 Γ, A, B, Γ' → Δ
 --------------------[テンソル積 右]
 Γ, A×B, Γ' → Δ


 Γ → Δ, A, B, Δ'
 -------------------[テンソル積 左]
 Γ → Δ, A×B, Δ'


 Γ → Δ,A   A,Ψ → Φ
 ------------------------[カット]
   Γ, Ψ → Δ, Φ

 Γ → Δ   Δ → Φ
 ------------------------[フルカット]
   Γ → Φ

絵算と論理

ケーブル＝ワイヤーの並び＝ワイヤーラベルのリストが命題
ストリング図（ダイアグラム）がシーケント＝自然演繹の証明図
ストリング図の変形がシーケントの推論＝自然演繹の証明図の変形＝自然演繹の基本リーズニング
ストリング図の変形ツリーがシーケントの証明図＝自然演繹のリーズニング図

カリー／ハワード対応により、コンパクト論理とコンパクト閉圏が対応する。コンパクト論理のモデルがコンパクト閉圏で、コンパクト閉圏の具体例がテンソル計算系。

そのとき問題になるのは、テンソル計算系が厳密モノイド圏上の厳密コンパクト構造を持つ。厳密コンパクト構造は、双対化子が厳密に対合的で、ゲルファント変換を経由しない（イコールになる）