ユニタリ対応の圏の集合論的構成
JavaScriptのBoolean仕様にあきれつつ、線形代数も考えてみた。
ユニタリ対応の圏は圏論的に作るとスマート。Span(UEmb)とCosp(URet)まではキレイに作れる。だが、Span(UEmb)とCosp(URet)を貼り合わせるところは、いまいちクリアになってない。
ユニタリ対応を集合論的に構成するとシチメンドクサイのが難点だが、手で触った感じがするし、貼り合わせが具体的になる。以下、集合論的に構成してみる。対象は有限次元内積空間。
まず、今までユニタリ埋め込み、ユニタリ引き込みと呼んでいたもの（線形写像）を、全域ユニタリ埋め込み、余全域ユニタリ引き込みと形容詞を付ける。そして、ユニタリ埋め込みとユニタリ引き込みを新たに次のように定義する。
- V⊆Uで、f:V→W が全域ユニタリ埋め込みのとき、(V⊆U, f)を、「U→Wのユニタリ埋め込み」と呼ぶ。
- V⊆Wで、f:U→V が余全域ユニタリ引き込みのとき、(V⊆W, f)を、「U→Wのユニタリ引き込み」と呼ぶ。
ユニタリ埋め込みと引き込みの全体を UEMB(U, W), URET(U, W)（全部大文字にした）とし、UCORR(U, W) = UEMB(U, W)∪URET(U, W) とする。UCORR(U, W) と UCORR(W, Z)の結合は、場合分けをして定義できる。場合分けが面倒だが、結果は自然な計算となる。
eを埋め込みの象徴、rを引き込みの象徴とすると、e;e = e, e;r = r, r;e = r, r;r = r となり、随伴でeとrがトグルする。雰囲気的には e = 1, r = 0 としての掛け算。随伴は x† = 1 - x 、あくまで雰囲気だが。
UCorr(U, W) = UCORR(U, W)/≡ としてユニタリ対応を定義するが、同値関係 A ≡ B とは次のどれか（少なくとも1つ）が成立すること：
- A = B
- A∈URET, B∈UEMB で A† = B-1
- B∈URET, A∈UEMB で B† = A-1
(-)-1:UEMB(U, W)→UEMB(W, U) は自然に定義できる。ダガーは、(-)†:URET(U, W)→UEMB(W, U) とEMBとRETを互いに入れ替える。
これらの定義が整合的であることを示すには：
- ≡がほんとに同値関係であること
- 同値類に関して、場合分けで定義した結合がwell-definedであること
を示す必要がある。場合分けが多くて非常に面倒だが、基本的に手間の問題。
面倒になる理由は、直交補空間と直交分解を使わないからで、これが使えるなら手間は減る。が、直交概念を使わない定式化にも意味はあるだろう、たぶん。
