檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2016-12-09 (金)

証明検証系Mizarのジレンマと証明系の村

| 16:44 | 証明検証系Mizarのジレンマと証明系の村を含むブックマーク

証明検証系Mizarを試した印象の続報です。

内容:

  1. 「これはひどい!」が、「これは素晴らしい!!」
  2. Mizarコミュニティ
  3. Mizarの可能性

「これはひどい!」が、「これは素晴らしい!!」

Mizarの解説にあるサンプルコードはほぼ動きません*1。僕が試した範囲ではひとつも動きませんでした。理由は簡単で、構文的に完全じゃないからです。特に、構文上必須であるenviron部はたいてい欠如してます。

environ部とは、当該の証明記述ファイル(.mizファイル)が依存しているライブラリファイル(コンパイルされているが、.mizファイルと同等)を列挙する部分です。モジュールのインポート宣言と思えばいいです。

このインポート宣言を書くのが尋常じゃなく難しいのです。なぜなら:

  • モジュールはグルーピングも階層化もされてなく、1257個がフラットに配置されている。
  • モジュール名は8文字までの英数字(アンダースコアは許す)に限定される。
  • モジュールから何をインポートするかにより、インポート宣言が10種類に分かれている。
  • 再帰的なインポートはサポートされない。関連するモジュールを明示的にすべて列挙する必要がある。
  • モジュールの依存関係を表示するツールはない
  • 定義や定理がどのモジュールに含まれるかの検索は、grepと目視による。

ちょっと信じられない仕様ですが、その悲惨さを感じるには実例を見るといいでしょう。自然数(natural number)に関する定理達は、数学のかなり基本的な部分ですが、それを記述しているモジュール(.mizファイル)nat_1.mizのenviron部は次です。

environ

 vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
      RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
      FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
      FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1;
 constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2,
      PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1,
      SETFAM_1, ZFMISC_1, BINOP_1;
 registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, CARD_1,
      RELSET_1, FUNCT_2, PBOOLE;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions SETFAM_1, TARSKI, XBOOLE_0, RELAT_1;
 equalities ORDINAL1, XBOOLE_0, CARD_1;
 expansions SETFAM_1, ORDINAL1, TARSKI, XBOOLE_0;
 theorems AXIOMS, ORDINAL1, XCMPLX_1, XREAL_1, XXREAL_0, TARSKI, ORDINAL2,
      XBOOLE_0, CARD_1, FUNCT_2, FUNCT_1, FUNCOP_1, PBOOLE, RELSET_1, RELAT_1,
      PARTFUN1, SUBSET_1, NUMBERS, ENUMSET1, XBOOLE_1;
 schemes SUBSET_1, ORDINAL2, FUNCT_2, PBOOLE, BINOP_1;

列挙されている8文字以内の大文字の名前が、nat_1.mizが参照している他のモジュールの名前達です。これらのモジュール名をどうやって知ったのでしょうか? たぶん、nat_1.mizのケースでは、著者が他のモジュールの全貌(=MMLライブラリ)を熟知していた、ってことでしょう。

では、僕のようにMMLライブラリについて何も知らない者が、自分で新しく.mizファイルを書くときはどうすればいいのでしょうか? 僕が調べた範囲では、

  • 難しいけど頑張れ

という、言い訳だか精神論だか励ましだか分かんない文言しかなかったです。

他にも驚かされることがイッパイで:

  • 新しく定義した名前や記号のインデックス(一種のハッシュマップ)を、手動で作成・メンテナンスしなくてはならない。
  • ソースファイル(自分で書いた.mizファイル)と同じディレクトリに一時的中間ファイルが生成される。それも、1ソースファイルに対して25中間ファイル。他の一時ディレクトリに書き出すオプションは見あたらない。
  • エラーレポートは、ソースファイルにエラー番号が埋め込まれる。タグジャンプは使えないし、毎回(エラーがあれば)ソースが書き換えられる。
  • エラー番号に対するテキストは、mizar.msg(Mizar Errors Explanation File)を見ないと分からない。(addfmsgというツールを使えば、ソースファイルのお尻にテキストメッセージを挿入してはくれるが。)

僕が「証明検証系Mizarを試してみる」で次のように書いた理由はこれでお分かりでしょう。

Mizarは20世紀で時間が止まってしまったような印象を受けます。


なにから何まで今風じゃなくて、MS-DOSの時代にタイムスリップしたみたい。

“地獄の使い勝手”です。しかし一方、

証明記述の可読性が高いのは本当で、構文の設計は優れたものだと思います。CoqやIsabelleとは比べものにならないくらい読みやすいです。

構文や意味モデルはホントに素晴らしいんですよ。ソフトウェアとしては「こんなもん使えるか!」と投げ出すレベルなんですが、CoqやIsabelleでは代替できない機能と用途を持っているので、フラストレーションに耐えながら調べたり試したりしています。

Mizarコミュニティ

Mizarは、1970年代初頭に、アンジェイ・トリブレッツ*2(Andrzej Trybulec 1941-2013)がMS-DOS上のTurbo Pascal*3で実装をはじめたものです。その当時の仕様をかなりの程度引き継いでいる(あるいは、引きずっている)ようです。例えば、“あのenvironの仕様”も、貧弱なCPUと少量のメモリ環境下では納得がいくものです。

しかしそれにしても、なんでそのままなの? と疑問に感じます。どうもこれは、Mizarコミュニティの性格によるのではないか、と思えます。ソフトウェアは、コミュニティの性格を色濃く反映するものですから。

2014年の岡崎裕之さんのスライドによると、2013年時点ですでに5万2千の定理がMMLライブラリに含まれていたそうです。この膨大な定理群を書いた人々に関しては:

  • 延べ200名を超える著者

とあります。えっ? 200? 「延べ」がどういう勘定か分からないですが、個人の数が300を超えることはありえないでしょう。多めで300人としても、一人平均173定理を書いています。仮に「80:20の法則」が成立するなら、60人ほどのアクティブメンバーが一人平均700個弱の定理を書いていることになります。

要するにMizarコミュニティはあまり大きくないのです。40年以上という時間方向の蓄積により、MMLという巨大なライブラリを構築したわけです。今風の、例えばNode.jsのnpmリポジトリのように、世界中のコントリビューターにより短期間で生成された大規模ライブラリとは全く性格が異なります。

Mizarシステムのソースコードは非公開(バイナリ配布)で、システムとMMLライブラリの開発を主導している組織である Association of Mizar Users (ポーランド語 Stowarzyszenie Uzytkownikow Mizara; http://mizar.org/sum/)も、事実上はビアリストーク大学(ポーランド)、アルバータ大学(カナダ)、信州大学の有志で構成されているようです。

小さく閉じたコミュニティ内であれば、「難しいけど頑張れ」は通用します。一子相伝とは言わないまでも徒弟制度的にコツを教えることが出来ます。ひょっとすると、非公開の内部ツールを持っているのかも知れません。緊密な関係性と情熱があれば、精神論・根性論でさえ効果を発揮します。多少の不満があっても「まー、頑張ろう」と。また、修正しようと思ってもソースコードへのアクセスが自由でないから「まー、頑張ろう」と。

僕は、J言語のコミュニティを思い出しました。

J言語の場合は、その構文がこの世のモノならざる超変態ですから、興味を持つ人がソモソモ特殊な嗜好・指向・志向の持ち主で、コミュニティも独自の閉じた文化を持つのは必然だと思います。

しかしMizarの場合は、言語自体は(証明記述言語の範疇では)癖がなくまっとうで、書くにも読むにも楽なものです。むしろ癖が凄く難読なのは、他の証明系のタクティク言語です。Mizarはもっと世に広まってよいものだと思います。Association of Mizar Usersのミッションにも、"popularizing, propagating and promoting the Mizar language"とあります。であるなら、システムの仕様もコミュニティの在り方も、もう少し現代の傾向に合わせたほうがいいんじゃないか、と(余計なお世話ですが)考えます。

Mizarの可能性

Isabelleの高水準証明記述言語はIsarといいます。公式には"Intelligible semi-automated reasoning"のアクロニムだということですが、おそらくはMizarへのリスペクトが込められているんじゃないかと思います。実際、Isar(の設計者のウェンツェル)はMizarにかなり影響を受けています。

ウェンツェルは、Isabelle/Isar(言語)とIsabelle/PIDE(フロントエンド・ソフトウェア)が教育に有効だろうと主張しているし、その方向で頑張ってもいるようです。しかし、「ちょっと無理なんじゃないか」と僕は思います。Isabelleは(そしてもちろんCoqも)無駄に難しいからです。タクティク言語の難読さは論外ですが、高水準なIsarにしても、その意味モデルや論理的概念が難しいので、教育に使うための事前の教育で息切れするでしょう。

Mizarの難しさは、言語仕様やモデルに起因するというよりは、システムの機能が古臭すぎて多大なストレスを強いる点にあります。「難しいけど頑張れ」を「楽になるように修正する」に方向転換すれば、事態は改善されるはずです。教育を含めて一般的な用途への適用可能性は、CoqやIsabelleよりはずっと大きいでしょう。

「もったいないなーー」と感じるんですよ。"MIZAR: the first 30 years"において、「Mizarプロジェクトは、アンジェイ・トリブレッツの最高傑作」(The MIZAR project is opus magnum of Andrzej Trybulec.)と評されています。Mizarには卓越したアイデアが含まれている思います。それがあの使い勝手とは …… もったいない!

*1[追記]「動く」は言葉としてふさわしくないですね。「動かない」は「コンパイルできない」です。[/追記]

*2:カタカナ表記は https://ja.wikipedia.org/wiki/Mizar に従いました。forvoでポーランド語発音を聞いてみると、アンジェイとアンドレイの中間くらいの音みたいです。無理に書くと「アンデュェイ」とかだけど、「アンジェイ」とします。

*3:現在の実装言語はfree pascal

トラックバック - http://d.hatena.ne.jp/m-hiyama/20161209

2016-12-08 (木)

証明検証系Mizarを試してみる

| 12:40 | 証明検証系Mizarを試してみるを含むブックマーク

Mizarは証明検証系です。形式的な証明記述言語とその処理系という括りではCoqIsabelleの仲間ですが、対話的ではないので使い勝手はだいぶ違います。とりあえずインストールして使ってみましょう。

内容:

  1. インストール
  2. 使ってみる
  3. 感想

インストール

Mizarのオフィシャルサイトは:

信州大学の日本語ページもあります。

信州大学のアーカイブから、自分の環境に応じたバイナリをダウンロードします。

Windowsの場合、現時点(2016年12月)ではmizar-8.1.04_5.33.1254-i386-win32.exeが最新のバイナリです。このファイルは単なる自己解凍形式のZIPファイルです。

例えば次のようにしてZIPファイルを展開します(シェルはbash)。

$ mkdir mizar-install-tmp

$ cd mizar-install-tmp

$ mv ../mizar-8.1.04_5.33.1254-i386-win32.exe .

$ ./mizar-8.1.04_5.33.1254-i386-win32.exe

  ナニヤラカニヤラ

$ ls -1
./
../
abstr.zip
install.bat*
license
mizar-8.1.04_5.33.1254-i386-win32.exe*
mizbib.zip
mizdb1.zip
mizdoc.zip
mizsys.zip
mizutil.zip
mizxml.zip
mmlfull.zip
prel.zip
readme.txt
unzip.exe*

$

ZIPを展開すると、さらにいくつかのZIPファイルと実行ファイルと文書ファイルが現れます。このなかのinstall.batを実行すればいいわけですが、えっらく古臭いインストール方法ですね。

CoqもIsabelleもインストーラーはモダンで作業は非常に簡単でした。Coqのインストールについて「WindowsへのCoqのインストール」に顛末を書いてますが、Coq本体ではなくてProof Generalに手間取ったからです。

それに比べると、インストールがバッチファイルって …… 念のためにMizarインストーラーであるinstall.batの中身を読んでみました; 引数に与えられたディレクトリパスに対してファイルを展開・コピーするだけです。デフォルトのディレクトリはc:\mizarです。

install.batのメッセージ文言を切り出してみると:

The Mizar system ver. 8.1.04 installation is now completed.

Make sure the line:  %1;
is in your path. For example, to run any of the PC Mizar programs
or utilities from anywhere on your system, your AUTOEXEC.BAT file
could contain a path like the following:
   PATH %1;
and
   SET MIZFILES=%1

AUTOEXEC.BATって、いつの時代の話だよ? 2016年の時点で、このスクリプトを使い続けている点で少し不安になったりします。

こういう古いスタイルのバッチファイルだと、パスに空白や'/'が混じっていたり名前の大文字小文字でトラブったりするので注意したほうがいいでしょう。このバッチファイルによるコピーにはかなり時間がかかります。

先のメッセージ文言にもあったとおり、環境変数を自分で設定しなくてはいけません。Mizarをインストールしたディレクトリを環境変数PATHに加えて、同じディレクトリを環境変数MIZFILESにセットします。

使ってみる

信州大学がMizarプロジェクトに参加しているので、日本語の資料があります。Mizarの概要を知るには、

日本語PDFマニュアル『Mizar 講義録』は、

Mizarを使うには、ワーキングディレクトリにサブディレクトリ構造が必要ということなので、次のようなサブディレクトリを作ります。

$ mkdir mizar-test

$ cd mizar-test/

$ mkdir text dict prel

$ ls
./  ../  dict/  prel/  text/

$

Mizarの記述単位をアーティクルと呼び、ファイル拡張子は.mizです。今作ったtextサブディレクトリに.mizファイルを置くようです。Mizarアーティクル(.miz)を書いたら、mizfというコマンド(Windowsでの実体はバッチファイル)で処理します。

スライド http://mizar.org/cicm_tutorial/mizar.pdf の45ページにあった次のコードを試してみます。

reserve i,j,k,l,m,n for natural number;
i+k = j+k implies i=j;
proof
  defpred P[natural number] means
    i+$1 = j+$1 implies i=j;
  A1: P[0]
  proof
    assume B0: i+0 = j+0;
    B1: i+0 = i by INDUCT:3;
    B2: j+0 = j by INDUCT:3;
    hence thesis by B0,B1,B2;
  end;
  A2: for k st P[k] holds P[succ k]
  proof
    let l such that C1: P[l];
    assume C2: i+succ l=j+succ l;
    then C3: succ(i+l) = j+succ l by C2,INDUCT:4
    .= succ(j+l) by INDUCT:4;
    hence thesis by C1,INDUCT:2;
  end;
  for k holds P[k] from INDUCT:sch 1(A1,A2);
  hence thesis;
end;

mizfコマンドはバッチファイルですから、PowerShellかcmd.exeからの実行が無難です(僕は、「Windowsのcmd.exeとbashのどちらでも実行できるバッチファイルの書き方」の方法でbashからも実行してますが。)

 mizar-test > mizf .\text\test.miz
Make Environment, Mizar Ver. 8.1.04 (Win32/FPC)
Copyright (c) 1990-2015 Association of Mizar Users

**** 2 errors detected

 mizar-test >

エラーメッセージは、text/test.mizファイル内にコメントとして埋め込まれます。以下の「::>」の行です。ウーンン、タグジャンプが使えないので辛い。

reserve i,j,k,l,m,n for natural number;
::>   *212,213
i+k = j+k implies i=j;
proof
  defpred P[natural number] means
    i+$1 = j+$1 implies i=j;
  A1: P[0]
  proof
    assume B0: i+0 = j+0;
    B1: i+0 = i by INDUCT:3;
    B2: j+0 = j by INDUCT:3;
    hence thesis by B0,B1,B2;
  end;
  A2: for k st P[k] holds P[succ k]
  proof
    let l such that C1: P[l];
    assume C2: i+succ l=j+succ l;
    then C3: succ(i+l) = j+succ l by C2,INDUCT:4
    .= succ(j+l) by INDUCT:4;
    hence thesis by C1,INDUCT:2;
  end;
  for k holds P[k] from INDUCT:sch 1(A1,A2);
  hence thesis;
end;
::>
::> 212: "environ" expected
::> 213: "begin" missing

environとbeginが必要だ、ってことらしい。先頭にenvironとbeginと書いた2行を挿入。

 mizar-test > mizf .\text\test.miz
Make Environment, Mizar Ver. 8.1.04 (Win32/FPC)
Copyright (c) 1990-2015 Association of Mizar Users

-Vocabularies  [   1]
-Constructors  [   1]
-Requirements  [   1]
-Registrations [   1]
-Notations     [   1]

Verifier based on More Strict Mizar Processor, Mizar Ver. 8.1.04 (Win32/FPC)
Copyright (c) 1990-2015 Association of Mizar Users
Processing: .\text\test.miz

Parser   [  29 *12]   0:00
MSM      [  25 *16]   0:00
Analyzer [  26 *16]   0:00
Checker  [  26 *16]   0:00
Time of mizaring: 0:00

 mizar-test >

うまくいったのか? lsしてみると、やたらにイッパイファイルがあります。

 mizar-test > ls text | %{ $_.name}
test.aco
test.ano
test.atr
test.cho
test.dct
test.dcx
test.ecl
test.eno
test.ere
test.err
test.evl
test.fil
test.frm
test.frx
test.idx
test.log
test.miz
test.msx
test.nol
test.par
test.prf
test.ref
test.sgl
test.vcl
test.wsx
test.xml

 mizar-test >

元ファイル1個に付き25個のファイルが生成されますが、すべて内部的に使用するものだとか。test.mizを見たら、エラーメッセージは残っています。

::>
::> 140: Unknown variable
::> 203: Unknown token, maybe an illegal character used in an identifier
::> 306: Attribute symbol expected
::> 330: Unexpected end of an item (perhaps ";" missing)
::> 371: "]" expected
::> 396: Formula expected

その後しばらくいじったみたのですが、どうもうまくいきません。色々な文書を見ても概念や構文の説明ばっかりで動く例がないのですよ。疑似コードやスニペットだけで、驚くほど実サンプルがない!

チュートリアル https://www.cs.ru.nl/~freek/mizar/mizman.pdf (54ページの文書)によると、Mizarのenviron部をキチンと書くのは難しいようです。

The most difficult part of writing Mizar is finding what you need in the MML which is the name of the Mizar Mathematical Library.


Mizarを書くときに一番難しいところは、MML(Mizar Mathematical Library)のなかから、必要な(インポートすべき)アーティクルを特定することだ。

It is hard to get the environment of a Mizar article correct.


Mizarアーティクルのenviron部を正しく書くのは難しいぞー。

MML(Mizar Mathematical Library)は膨大なファイル群からなるライブラリです。その内容や相互関係を把握して、適切にインポートするのは確かにシンドそうです。「難しいぞ」「頑張れよ」って書いてあるだけで、ノウハウもツールも示してません(泣)。

感想

Mizarは1973年から開発が続いています。80年代からはじまったCoq, Isabelleよりさらに古い言語/システムです。歴史が長いシステムであっても、最近の傾向を取り込んでいたり斬新なもの(Isabelle/jEditとか)もありますが、Mizarは20世紀で時間が止まってしまったような印象を受けます。

「動くサンプルコードがない」といいましたが、MMLライブラリという膨大なサンプルがあるとも言えます。MMLの資産はさすがに凄いなと思います。が、MMLをブラウズしたり検索するツールは見当たりません。ツールや手法に関する論文はあるけど動くツールがなかったりします(例:MML Query)。インターネット上に公開されたオンラインツールもたいていはリンク切れ。本家サイトさえも貧弱で安定してないようです。なにから何まで今風じゃなくて、MS-DOSの時代にタイムスリップしたみたい。

でも、証明記述の可読性が高いのは本当で、構文の設計は優れたものだと思います。CoqやIsabelleとは比べものにならないくらい読みやすいです。それだけに、ソフトウェアシステムとしての時代遅れ感が残念です。

2016-12-05 (月)

モノイド圏の随伴性を“豊饒圏の圏”の随伴性に持ち上げる: 計画編

| 16:17 | モノイド圏の随伴性を“豊饒圏の圏”の随伴性に持ち上げる: 計画編を含むブックマーク

テンパリー/リーブ圏とカウフマンのスケイン関係式」において、「たぶん成立するだろう」みたいなことを幾つか書いています。そのひとつに次の随伴性があります。

  • k-LinCat(Link(C), D) ¥stackrel{¥sim}{=} Cat(C, U(D))

ここで、k-LinCatk-線形圏の圏です。Link(-)は単なる圏からk-線形圏を作る関手で、集合の線形化(自由ベクトル空間を作る操作)をホムセットごとに適用して、圏全体を線形化します。Uは、すべてのホムセットのk-線形構造を忘れる忘却関手です。

この形を見ると、F:SV, G:VS が随伴関手対 F -| G のとき、次の随伴関手対が作れそうな気がします。(この記事の本文と記法を合わせるために、C, Dはローマン体です。)

  • V-Cat(F(C), D) ¥stackrel{¥sim}{=} S-Cat(C, G(D))

ここで、V-CatS-Catは、豊饒圏の圏です。F:S-CatV-Cat と G:V-CatS-Cat は、モノイド圏のあいだの関手F, Gを、“豊饒圏の圏”のあいだの関手に持ち上げたものです。

上記の“持ち上げられた随伴性”はいかにも成立しそうです。が、実際に確認しようとしたらヤッパリめんどくさい。とりあえず、“持ち上げられた随伴性”を示す手順について考えてみます。

内容:

  1. 言葉と記号の約束
  2. 素朴なアイデア
  3. 超巨大な圏
  4. 様々な圏を整理する
  5. 手順(予定)

言葉と記号の約束

後で使う言葉と記法について以下にダラダラと書き連ねます。

S, Vなどのイタリックの文字はモノイド圏を表すとします。モノイド圏のあいだの関手としてはモノイド関手を想定します。ただし、モノイド関手には幾つかの種類があります。

  1. 厳密モノイド関手(strict monoidal functor)
  2. タイト・モノイド関手(tight monoidal functor, 強モノイド関手(strong monoidal functor)と呼ぶことが多い)
  3. ラックス・モノイド関手(lax monoidal functor)
  4. 反ラックス・モノイド関手(oplax monoidal functor, ラックス・余モノイド関手(lax comonoidal functor)とも呼ぶ)

最近僕は、強モノイド関手の代わりにタイト・モノイド関手と呼んでいます。形容詞「強」は他で使われるので重複や混乱を避けたいからです。モノイド圏と各種のモノイド関手については、次の記事を参照してください。

Sがモノイド圏のとき、S = (S, ×, I, α, λ, ρ) でSのモノイド圏構造を表すとします。各種の律子α, λ, ρは特に必要なければ省略し、S = (S, ×, I) とも書きます。

Xは集合として、C:X×X→|S|, γ:X×X×X→Mor(S), ι:X→Mor(S) の四組を C = (X, C, γ, ι) のように書くことにして、Cが特定の条件を満たすときS-豊饒圏S-enriched category)と呼びます。集合Xを|C|と書けば、C = (|C|, C, γ, ι)、あるいは|C|を省略して C = (C, γ, ι) とも書きます。Cが満たすべき特定の条件については、次の記事を参照してください。

S-豊饒圏を考えるとき、モノイド圏S豊饒化ベース圏(enriching category, base category)と呼びます。

この記事では、豊饒化ベース圏はS, Vなどのイタリック体で書きますが、豊饒圏はイタリックではなくてC, Dなどのローマン体で書くことにします。結合γ、恒等ιなどが「どの豊饒圏のものか?」を明示したいなら、γC, ιCのような上付き添字にします。下付きは、γCa,b,c:C(a, b)×C(b, c)→C(a, c) のように使います。特に必要でない限りは上付き添字は省略します。

CとDがS-豊饒圏のとき、CからDへのS-豊饒関手S-enriched functor)は f:C→D のように小文字で書きます。射と紛らわしい、って? 豊饒圏では射は存在しないんですよ。Cのホム対象はSの対象ですが、Sの対象が集合とは限らないので、“ホムセットの要素”としての射は(一般には)存在しないのです。

豊饒圏のあいだの豊饒関手fは、f:|C|→|D| という集合のあいだの写像と、a, b∈|C| で添字付けされたSの射の族 fa,b:C(a, b)→D(f(a), f(b)) in S からなります。f(a)の形のときは対象のあいだの写像、fa,bの形に書いたときはホム対象(Sの対象)のあいだの射の意味とします。豊饒関手が満たすべき条件はいずれ述べる機会があるでしょう(今は割愛します)。

S-豊饒圏を対象としてS-豊饒関手を射とする圏をS-Catと書きます。S-Catは、モノイド圏Sを豊饒化ベース圏とする豊饒圏の圏です。一部、定義を省略(先延ばし)したところもありますが、以上で、圏としてのS-Catは定義できました。

自然変換のS-豊饒版もあります。C, DがS-豊饒圏、f, g:C→D がS-豊饒関手のとき、S-豊饒自然変換S-enriched natural transformation) j::f⇒g:C→D を定義できます。S-豊饒自然変換まで考えると、S-Catは単なる圏ではなくて2-圏となります。S-Catを圏と考えるか、それとも2-圏と考えるかは場合・状況によりけりです。

素朴なアイデア

我々が示したいことは、F:SV, G:VS がモノイド圏のあいだの随伴関手対のとき、FとGを豊饒圏の圏V-Cat, S-Catまで持ち上げた関手 F:S-CatV-Cat, G:V-CatS-Cat が再び随伴関手対になることです。

特別なケースとして、S = Set, V = Vectkで、Fは自由ベクトル空間を生成する関手、Gはベクトル空間にその台集合を対応させる忘却関手とします。このとき、F -| G (FとGは随伴関手対)なので、上記の命題が成立すれば、F -| G となります。F:Set-CatVectk-Cat は普通の圏からk-線形圏を作る関手、G:Vectk-CatSet-Catk-線形圏の線形構造を忘れて単なる圏とみなす関手です。

Set-Catは普通の(小さい)圏の圏なのでCatと同じです。また、Vectk-Catk-LinCatk-線形圏の圏)と書いて、F = Link, G = U と置き換えれば、随伴性は次の形でも書けます。

  • k-LinCat(Link(C), D) ¥stackrel{¥sim}{=} Cat(C, U(D))

これは、「テンパリー/リーブ圏とカウフマンのスケイン関係式」で仮定した命題そのものです。

さて、上記の“随伴性の持ち上げ”はどうやったら示せるでしょうか? 随伴性をニョロニョロスタイルで書いてみましょう。関手の図式順結合と自然変換の横結合は*で書くことにして、ε::IdS→F*G:SS を随伴の単位、η::G*F⇒IdV:VV を随伴の余単位とします。このとき、ニョロニョロ関係式(snake relation)は次の2つの等式となります。(「;」は自然変換の図式順縦結合です。)

  • (ε*F);(F*η) = F
  • (G*ε);(η*G) = G

これはニョロニョロ図で表現できますが、図は後で挙げます。

もし、F, G以外に ε::IdS-Cat→F*G:S-CatS-Cat と η::G*F⇒IdV-Cat:V-CatV-Cat がうまく定義できて、しかも縦結合「;」と横結合「*」が(-)☆で保存されるなら、次の等式が成立するはずです。

  • *F);(F) = F
  • (G);(η*G) = G

つまり、 S-Cat, V-Cat, F, G, ε, η が随伴性を定義することになります。これは求める結果に他なりません。

となると、対応 (-) |→ (-) を構成して、それが縦結合/横結合を保存することを示せば随伴性の持ち上げは出来るわけです。

超巨大な圏

前節の素朴なアイデアが正しいなら、あとは計算問題となります。手間はかかっても、順番に定義と計算をこなしていけばいいでしょう。しかし、圏のサイズの問題があります。それを説明するため、以下に、F -| G を表すストリング図の一部を示します。

このストリング図は“どこに”に描かれているのでしょう? 図に現れるS, V, F, G, ε, ηなどがどこに所属するのか? と聞いても同じです。答は「モノイド圏の圏」ですが、自然変換も登場するので、「モノイド圏を対象とする2次元の圏」と言うほうが正確です -- 随伴性は2次元の圏で定義されるべきものです。

「モノイド圏を対象とする2次元の圏」には、モノイド圏としてのSetVectkも入ります。「モノイド圏を対象とする2次元の圏」は大きな圏も対象に含むことになるのです。このような超巨大な圏をとても大きな圏(very large category)と呼ぶことにします。ここで考えるとても大きな「モノイド圏を対象とする2次元の圏」をMonCATと書くことにします。MonCATの射としてどのようなモノイド関手を取るか? という問題はありますが、今は気にしないことにします(いずれ決める)。

さて、(-)がうまく定義できたとすれば、(-)で移された先でニョロニョロ関係式が成立します。その一部をストリング図で表すなら次です。

すべてに☆が付いた形です。ここで、SとはS-Catのことで、VV-Catです。

この☆付きのストリング図は“どこに”に描かれているのでしょう? この図は、Set-Cat = CatVectk-Cat = k-LinCat を対象として含む圏のなかの図のはずです。つまり、とても大きな「豊饒圏の圏の圏」のなかに描かれているのです。☆付きストリング図を描く場所となる「豊饒圏の圏の圏」をEnrCatCATと記すことにします。

EnrCatCATは超巨大で正体不明です。そもそも、EnrCatCATなんて存在するのでしょうか? こんなものを考えることが許されるのでしょうか? ちょっと不安ではありますが、存在しない/考えちゃダメと言われると話が先に進まないので、とりあえず「それは在る」と思うことにします。

EnrCatCATの対象は、「豊饒圏の圏」なので2次元の圏です(豊饒自然変換が2次元の射)。2次元の圏を対象に持つ圏は3次元の構造を持つことが出来ます。つまり、EnrCatCATは3次元の圏です。ただし、今回は2次元の射まであれば十分なので、EnrCatCATの2次元部分まで考えれば間に合いそうです。

随伴性を持ち上げるための対応 (-) |→ (-) は、“とても大きな2次元の圏MonCAT”から“とても大きな2次元の圏EnrCatCAT”への2次元構造を保つ対応となります。この対応(-)をEnrCatとも書くことにします。EnrCat:MonCATEnrCatCAT, EnrCat(-) = (-) です。

様々な圏を整理する

このテの問題を扱う際の困難は「ややこしい」ことです。使用する用語と記法に注意しないと、すぐさま混乱して何がなんだか分からなくなります。

とりあえず議論に登場する圏を列挙しておきます(下の表)。モノイド圏の次元を(1+α)としているのは、2次元の圏の極めて特殊なケース(対象が1つ)とみなせるからです。

圏(の記号) 種別 次元 大きさ ホムセットの大きさ 親の圏
Set モノイド圏 1+α 大きい 小さい MonCAT
Vectk モノイド圏 1+α 大きい 小さい MonCAT
S, V モノイド圏 1+α 大きい 小さい MonCAT
MonCAT 厳密2-圏 2 とても大きい大きい -
Cat 厳密2-圏 2 大きい 小さい EnrCatCAT
k-LinCat 厳密2-圏 2 大きい 小さい EnrCatCAT
C, D 豊饒圏 1 小さい - S-Cat
S-Cat 厳密2-圏 2 大きい 小さい EnrCatCAT
EnrCatCAT 厳密3-圏 3 とても大きい 大きい -

太字は圏の固有名詞で、太字以外は変数です。Set, Vectkは自己豊饒圏ですが、ここでは自己豊饒構造は考えないことにします。SetVectkは大きい圏なので、自己豊饒構造を考えても Set-Cat = Cat, Vectk-Cat = k-LinCat には入らないのです(Cat, k-LinCat小さい圏の圏だから)。

次にそれぞれの圏のセル(構成素)の呼び名を表にまとめておきます。

圏(の記号) 0-セル 1-セル 2-セル
Set 集合 写像 -
Vectk ベクトル空間 線形写像 -
S, V 対象 -
MonCAT モノイド圏 モノイド関手 モノイド自然変換
Cat 小さい圏 関手 自然変換
k-LinCat 小さい線形圏 線形関手 線形自然変換
C, D 集合の要素 - -
S-Cat 小さい豊饒圏 豊饒関手 豊饒自然変換
EnrCatCAT 豊饒圏の圏 2-関手 2-自然変換

それ以外のセルと結合(圏の演算)を表す記号は以下のようにします。

圏(の記号) 0-セル 1-セル 2-セル 縦結合 横結合
Set A, B f, g - ; ×
Vectk V, W f, g - ; ¥otimes
S, V A, B,V, W f, g - ; ×, ¥otimes
MonCAT S, V F, G α, β ; *
Cat C, D F, G α, β ; *
k-LinCat C, D F, G α, β ; *
C, D a, b - - - -
S-Cat C, D f, g j, k ; *
EnrCatCAT S-Cat, V-Cat X, Y Φ, Ψ ; *

手順(予定)

もし、素朴なアイデアが正しいなら、次の手順でモノイド圏のあいだの随伴性を“豊饒圏の圏”のあいだの随伴性に持ち上げられるはずです。

  1. モノイド圏Sに対して、S = S-Cat を定義する。
  2. モノイド関手 F:SV に対して、F:SV を定義する。
  3. モノイド自然変換 α::F⇒G:SV に対して、α::F⇒G:SV を定義する。
  4. (F*G) = F*G を示す。
  5. (α;β) = α を示す。
  6. (α*β) = α を示す。

ニョロニョロ・スタイルで書いた随伴性は、等式的な主張なので、対応(-)が等式的な主張を保存するなら、(-)で行った先でも随伴性を主張できるだろう、という目論見です。

素朴なアイデア/楽観的な目論見ですから、途中で何か問題が生じない保証はありません。とはいえ、命題の形はいかにもありそうだし、1/3くらい計算してみたところ、うまくいっているみたいなので期待は持てます。残りの計算をする体力・気力が問題だけど。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20161205

2016-11-30 (水)

高次圏の下部構造を箙〈えびら〉で表現してみる

| 15:27 | 高次圏の下部構造を箙〈えびら〉で表現してみるを含むブックマーク

Cが2次元の圏であって、対象、射、2-射(2-セル)を持っているとします。このとき、2-射を忘れて対象と射だけを考えることに何の問題もありません。Cを通常の(1次元の)圏とみなせます。

では、対象を忘れて射と2-射だけを考えたいときはどうでしょう。射の集合と2-射の集合を単純に取り出しただけでは圏にはなりません。次元が低い構成素を削り落とすには何らかの工夫が必要です。

そんな工夫のひとつとして、高次圏の台となる構造(下部構造)を、高次の箙〈えびら〉を使って表現してみます。高次の箙は、高次圏(higher category, n-category)を記述する便利な言葉を提供します。

内容:

  1. 反射的箙
  2. 反射的箙の別な定式化
  3. 半反射的箙と概反射的箙
  4. 高次圏と高次箙
  5. 共端対とホム箙
  6. 実例:小さい圏の圏
  7. まとめと展望

反射的箙

(quiver)とは、「多重辺と自己ループ辺を許す有向グラフ」という長ったらしい名前に対する別名です。(この言葉を使うことにした動機は「形容詞「複」「多」と箙〈えびら〉」参照。)

箙をQとして、頂点の集合を|Q|0, アロー(有向辺)の集合を|Q|1とします。s, t:|Q|1→|Q|0写像として、Q = (|Q|0, |Q|1, s, t) が箙です。満たすべき公理(条件)は特にありません。

上記の(|Q|0, |Q|1, s, t)に加えて、写像 i:|Q|0→|Q|1 があって次を満たすとき、(|Q|0, |Q|1, s, t, i)を反射的箙(reflexive quiver)と呼びます。

  • i;s = id|Q|0
  • i;t = id|Q|0

反射的箙は、圏から結合(composition)を除いた構造になります。a∈|Q|0に対するi(a)は恒等射に相当します。「反射的」の由来は、同値関係などの反射律に多少似てるからですが、言葉を気にする必要はありません。

圏の場合と同様に、a, b∈|Q|0に対するアローセットをQ(a, b)と書きます。f∈Q(a, b) を f:a→b in Q とも書きます。

反射的箙の別な定式化

Aを集合として、構造(A, ‖, ◁, E)を考えます。ここで、

‖は共端関係*1、◁は隣接関係と呼びます。f‖g は「fとgは共端」、f◁gは「fはgに(この順で)隣接している」と読みます。

次の公理を仮定します。

  1. ‖はA上の同値関係
  2. f‖f', g‖g', f◁g ならば、f'◁g'
  3. x∈E ならば、x◁x (自分と隣接している)
  4. x, y∈E, x‖y ならば、 x = y
  5. 任意のfに対して、x◁f となる x∈E がある。
  6. 任意のfに対して、f◁y となる y∈E がある。

これは、反射的箙の別定義になります。

与えられた(A, ‖, ◁, E)に対して、(|Q|0, |Q|1, s, t, i)を次のように定義します。

  1. |Q|0 := E
  2. |Q|1 := A
  3. s(f) := εx.(x◁f かつ x∈E)
  4. t(f) := εx.(f◁y かつ y∈E)
  5. i:|Q|0→|Q|1は、E⊆A の包含埋め込み。

s, tの定義に使っている εx.(…) は、「…であるようなx」と読みます。詳しくは「イプシロン計算ってなんですかぁ? こんなもんですよぉ」を見てください。sとtが写像としてwell-definedなことは、公理からすぐ出ます。i;s = id, i;t = id も定義から出ます。

(|Q|0, |Q|1, s, t, i)から(A, ‖, ◁, E)を作るには、

  1. A := |Q|1
  2. f‖g :⇔ s(f) = s(g) かつ t(f) = t(g)
  3. f◁g :⇔ t(f) = s(g)
  4. E := i(|Q|0) (iによる像集合)。

(A, ‖, ◁, E)に関する公理も簡単に確認できます。

半反射的箙と概反射的箙

反射的箙と同じ構造 (A, ‖, ◁, E) で、公理を弱めたものを考えます。

  1. ‖はA上の同値関係
  2. f‖f', g‖g', f◁g ならば、f'◁g'
  3. x∈E ならば、x◁x (自分と隣接している)
  4. x, y∈E, x‖y ならば、 x = y

アローfの両端にEに属する自己隣接アローが決まることを要求していません。圏で言えば、恒等射の存在を要求しないことに相当します。弱めた公理を満たす構造を半反射的箙(semi-reflexive quiver)と呼ぶことにします。半反射的箙では、Eが空になることも許されます。

(A, ‖, ◁, E)が反射的箙なら、もちろんこれは半反射的箙でもあります。Aを任意の集合として、Aに対して、(A, ‖, ◁, E) を次のように定義すると半反射的箙になります。

  • a, b∈A なら、a, bが何でも a‖b
  • どんな a, b∈A でも、 a◁b とはならない
  • Eは空集合

さて、これから n≧0 に対してn-概反射的箙(n-almost reflexive quiver)というものを定義します。n-概反射的箙は、次の構成素を持ちます。

  1. 0≦ j ≦n に対して集合 |Q|j
  2. |Q|j上の半反射的箙構造 (|Q|j, ‖j, ◁j, Ej)。
  3. 0≦ j ≦(n - 1) に対して写像 sj, tj:|Q|j+1→|Q|j
  4. 0≦ j ≦(n - 1) に対して写像 ij:|Q|j→|Q|j+1

sj, tj, ijは次の関係を満たします。

  1. sj;tj-1 = tj;tj-1
  2. tj;sj-1 = sj;sj-1
  3. ij;sj = id
  4. ij;tj = id

さらに次も満たすとします。

  • j≧1 ならば、(|Q|j, ‖j, ◁j, Ej) は反射的箙であり、sj-1, tj-1, ij-1 によって作られる反射的箙構造と同じである。

最後の条件を詳しく言うと:

  • f‖jg ⇔ sj-1(f) = sj-1(f) かつ tj-1(f) = tj-1(f)
  • f◁jg ⇔ tj-1(f) = sj-1(g)
  • Ej = ij-1(|Q|j-1)

(|Q|0, ‖0, ◁0, E0) だけが例外的で、反射的箙であることは保証されません。

今までの定義内で出てきた上限値nがなくて、任意のj≧0に対して上記の構造が定義されているときは、∞-概反射的箙と呼びます。

[追記]

n-概反射的箙Qの0次元部分である|Q|0上に半反射的箙構造(|Q|0, ‖0, ◁0, E0) を要求してますが、実際に必要なのは共端関係だけです。したがって、半反射的箙構造を同値関係だけに弱めても、応用上は差し障りがないかも知れません。

[/追記]

高次圏と高次箙

Cをn-圏とします。n-圏の定義は色々ありますが、とりあえず次のことを仮定します。

  1. 0≦ k ≦n に対して、Cのk-射(k-セル、k-アロー)の集合が決まっている。Cのk-射の集合を|C|kとする。特に、|C| = |C|0
  2. a∈|C|k(0< k ≦n)なら、dom(a), cod(a)∈|C|k-1 である。
  3. a∈|C|k(0≦ k <n)なら、ida∈|C|k+1 である。

これは、n-圏Cがn-概反射的箙を決めることを示しています。あるいは、n-圏の台構造がn-概反射的箙であるとも言えます。

n-圏Cが決めるn-概反射的箙をもう少しハッキリと記述しておきましょう; |C|k上で定義されたdom, codは dom(k-1), dom(k-1):|C|k→|C|k-1 と書くことにします。下付き添字の番号が(k - 1)である点に注意してください。|C|k上で定義されたidは、id(k):|C|k→|C|k+1 とします。

s, t, iの代わりにdom, cod, idを使うので、今後は文字iを番号に使うことを許します。

念のために、dom, cod, idが満たす等式を再度書いておくと:

  1. dom(i);cod(i-1) = cod(i);cod(i-1)
  2. cod(i);dom(i-1) = dom(i);dom(i-1)
  3. id(i);dom(i) = Id|C|i
  4. id(i);cod(i) = Id|C|i

ここで、id(i)は箙の構造を定義する写像で、Id|C|iは“i-射の集合|C|i”の上の恒等写像です。

n-圏Cの対象の集合|C|0は単なる集合なので、(|C|0, ‖0, ◁0, E0) は自明な方法で定義しておきます。つまり、

  1. A, B∈|C|0 ならば、A‖B。
  2. A, B∈|C|0 ならば、A◁B ではない。

0< i ≦n に対する(|C|i, ‖i, ◁i, Ei) は、dom, cod, idから自動的に決まります。

n-圏Cから決まるn-概反射的箙も同じ記号Cで表します。n-概反射的箙Cは、k-射の集合(k = 0, 1, ..., n)と、3×n個の写像から構成されます。

n-概反射的箙Cに対して、その1-シフトは、|C|0を捨てて、番号を付け直した(n - 1)-概反射的箙です。Cの1-シフトをC[1]と書いて、シフトしたdom, cod, idは、dom[1], cod[1], id[1]とします。

  • 0≦ i ≦ (n -1) に対して、(C[1])i = Ci+1
  • 0≦ i ≦ (n -1) に対して、(dom[1])(i) = dom(i+1)、(cod[1])(i) = cod(i+1)、(id[1])i = id(i+1)

この定義で、C[1]はn-概反射的箙になります。|C[1]|0 = |C|1上の(‖, ◁, E)構造は反射的箙になりますが、反射的箙は半反射的箙なので問題ありません。

Cがn-概反射的箙のとき、0≦ k ≦n に対してk-シフトを次のように定義できます。

  • C[0] := C
  • C[k] := (C[k-1])[1]

C[k]は(n - k)-概反射的箙になります。C[k]が、Cのk次元未満のセルを捨てた構造です。

共端対とホム箙

通常の圏Dにおいて、A, B∈|D| に対するホムセットD(A, B)は大変に便利な概念です。高次圏に対してもホムセットを定義しましょう。

Cはn-圏だとして、対応するn-概反射的箙も同じCで表します。0≦ k <n として、a, b∈|C|k とします。同じ次元(k)の射は共端かどうかを判定できます。a‖kbのとき、(a, b)をk-共端対と呼びます。

  • k = 0 のときは、a‖0b は|C|0上の関係として決まる。
  • k > 0 のときは、a‖kb は dom(k-1)(a) = dom(k-1)(b) かつ cod(k-1)(a) = cod(k-1)(b) のこと。

a, bがk-共端対のとき、C(a, b)を定義できます。C(a, b)は、(n - k - 1)-概反射的箙になるので、aからbへのホム箙と呼びます。C(a, b)は高次箙なので、(n - k)個の集合 |C(a, b)|0, ..., |C(a, b)|n-k-1 と各次元のdom, cod, idで構成されます。これらの構成素を定義していきます。

準備として、X⊆|C|j(0≦ j <n)に対して X#⊆|C|j+1 を定義します。

  • X# = {a∈|C|j+1 | dom(j)(a)∈X かつ cod(j)(a)∈X }

(X#)# = X## = X#2, ((X#)#)# = X### = X#3 のようにも書きます。

さて、C(a, b)の定義です。C(a, b)に付随するdom, cod, idをdom', cod', id' とします(これ以上の添字は煩雑なので)。

  • |C(a, b)|0 = {x∈|C|j+1 | dom(j)(x) = a かつ cod(j)(x) = b}
  • |C(a, b)|i := (|C(a, b)|0)#i
  • dom'(i) := (dom(k+i)の|C(a, b)|i+1への制限), cod'(i) := (cod(k+i)の|C(a, b)|i+1への制限), id'(i) := (id(k+i)の|C(a, b)|iへの制限)。

以上により、C(a, b)は、(n - k - 1)-概反射的箙になります。

実例:小さい圏の圏

n = 2, C = Cat の場合を考えてみます。

  • |Cat|0 = (すべての(小さい)圏の集合)
  • |Cat|1 = (すべての関手の集合)
  • |Cat|2 = (すべての自然変換の集合)
  • dom(0), cod(0), id(0) は、関手のdom, cod, id
  • dom(1), cod(1), id(1) は、自然変換のdom, cod, id

ホム箙は二種類考えることができます。A0B に対するCat(A, B)と、F‖1G に対するCat(F, G)です。

A, B を小さい圏として、(2 - 0 - 1)-概反射的箙Cat(A, B)を定義しましょう; A0B は無条件に成立するので、1-概反射的箙Cat(A, B)を定義できます。

  • |Cat(A, B)|0 = {F∈|Cat|1 | dom(0)(F) = A かつ cod(0)(F) = B}
  • |Cat(A, B)|1 = (|Cat(A, B)|0)# = {α∈|Cat|2 | dom(1)(α), cod(1)(α)∈|Cat(A, B)|0 }

F, G を関手として、(2 - 1 - 1)-概反射的箙Cat(F, F)を定義しましょう; F‖1G ならば、0-概反射的箙Cat(F, G)を定義できます。

  • |Cat(F, G)|0 = {α∈|Cat|2 | dom(1)(α) = F かつ cod(1)(α) = G}

2種のホム箙の対象集合(0-射の集合)を簡略化した記法で書けば:

  • |Cat(A, B)|0 = Functor(A, B)
  • |Cat(F, G)|0 = NatTran(F, G)

まとめと展望

球体(globe)ベースで定義されたn-圏(高次圏)から結合演算を取り除いてしまうと、n-概反射的箙になります。逆に言うと、n-概反射的箙は、n-圏を定義するための土台となる構造です。

n-概反射的箙では、k-シフトにより低次元のセルを捨てることと、任意の共端対に対するホム箙を取り出すことが出来ます。シフトの結果もホム箙も再び概反射的箙になります。したがって、シフトとホム箙抽出の操作は、組み合わせたり繰り返したりできます。

n-概反射的箙のあいだの準同型射を定義すれば、n-概反射的箙の圏n-AReQを構成できます。k-シフトは、(-)[k]:n-AReQ→(n-k-1)-AReQ という関手となります。また、n-概反射的箙を∞-概反射的箙に拡張する関手 n-AReQ→∞-AReQ も定義できます。

n-概反射的箙の概念に基いて、n-圏(高次圏)に関する記述法をもう少し整理できるんじゃないか、と考えています。

*1:英語ではparallel(平行)ですが、共端のほうが意味が伝わると思います。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20161130

2016-11-25 (金)

簡易版:図から作ったモノイド圏のテンパリー/リーブ線形表現

| 11:31 | 簡易版:図から作ったモノイド圏のテンパリー/リーブ線形表現を含むブックマーク

テンパリー/リーブ圏とカウフマンのスケイン関係式」で述べた状況は、もっと簡単な例でも確認できるので、簡単な例も紹介します。ブレイド図の代わりにアミダ図を使います。

アミダ図は、“あみだくじ”でお馴染みの次のような図です。

横棒の部分を次のように交差に置き換えると、ブレイド図と似た図形になります。

ブレイド図と違うのは、交差に上下(手前と奥)の区別がないので、一種類の交差しかないことです。この一種類の交差を適当に配置した図がアミダ図です。絵を描くときは、交差を横棒のまま描いてもかまいません。以下、交差をXで表すことにします。

アミダ図を上下に並べることで結合(composition)、左右に並べることでモノイド積を定義すると、アミダ図の全体は厳密モノイド圏(strict monoidal category)になります。この圏の対象は自然数の全体Nです。モノイド圏なので、紐(線)の伸縮や交替律(interchange law)による上下ズラシに起因する違いは無視します。

こうしてできた厳密モノイド圏を AmiDiag = (AmiDiag, ¥otimes, 0) とします。モノイド積¥otimesは、対象(自然数)では足し算で、射であるアミダ図では左右併置です。

テンパリー/リーブ圏とカウフマンのスケイン関係式」ではブレイド図の圏BrDiagを使ったのですが、代わりにアミダ図の圏AmiDiagを使うと話が簡単になります。

ブレイド図のときと同じように、テンパリー/リーブ圏への線形表現を考えます。表現のターゲットとなるテンパリー/リーブ圏は、係数体をR、サークル乗数を-2にします。サークル乗数の選び方は「そうするとうまくいくから」です。複素数の計算は不要なので係数体は実数にしました(Qでもかまいません)。

線形表現 F:AmiDiagTL(R, -2) は次のように定義します。

  • F(1) = 1 (対象の生成元での値)
  • F(X) = H + I2 (射の生成元での値)

Hは∪;∩のこと、I2はid2で縦の二本棒です。これだけ決めれば、あとはFが厳密モノイド関手であることから全域的に拡張できます。

アミダ図のあいだにも、(対称化した)ライデマイスター/アルチン同値関係〜RAを定義できて、この同値関係で割り算(ホムセットごとに商集合を作成)すれば、置換の圏Permと圏同値になります。AmiDiag/〜RA ¥stackrel{¥sim}{=} Perm

上で定義した線形表現 F:AmiDiagTL(R, -2) は、圏AmiDiag上の同値関係〜RAをイコールに移す(計算しましょう)ので、結果的に、置換の圏のテンパリー/リーブ線形表現 PermTL(R, -2) を与えます。

ブレイド図に関わる概念とアミダ図に関わる概念の対応関係は次のとおりです。

ブレイド図 アミダ図
モノイド圏 BrDiag AmiDiag
圏の生成元 B+とB- Xだけ
同値関係 ライデマイスター/アルチン同値 対称化されたライデマイスター/アルチン同値
対応する群 ブレイド群 置換群(対称群)
TLの係数体 C R
TLのサークル乗数 1 -2
スケイン関係式の係数 ωとω' 1と1

AmiDiagは簡単です。簡単な分、面白みに欠けるのですが、試したり遊んだりするときの負担が少ないのが良いと思います。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20161125

2016-11-24 (木)

「量子と古典の物理と幾何@名古屋」の話題

| 15:36 | 「量子と古典の物理と幾何@名古屋」の話題を含むブックマーク

ここで何を話そうかな、ってことですが:
僕は谷村先生の「物理学者のための圏論入門」の直後なので、圏論入門を補足する実例を紹介するつもりです。少数(ひとつかふたつ)の事例・例題に沿って、ストリング図の使い方を説明します。

選ぶ実例によって話の内容は変わりますが、その実例を選ぶ際の基本方針は決めています。

  1. ストリング図を話題にしたいので、(当たり前ですが)ストリング図が効果的に使える例。
  2. 少ない予備知識で理解できる例。特定分野(コンピュータ科学やら物理やら)の知識を要求せずに、圏に関しても定義くらい知っていればいい例。
  3. 通常の圏を拡張・一般化した概念が含まれる例。

すべての条件を満足する例を探すのは難しそうですが、できるだけこの基準に沿うようにしよう、ということです。

最後の条件である「通常の圏を拡張・一般化した概念」についてちょっと説明しておきます。

通常の圏を拡張する方法には以下のようなものがあります。先に言っておきますが、箇条書きの後に簡単な説明を付けますが、そこに出てくる難しげな用語は気にしないで流し読みしてください。

  • 豊饒化
  • 内部化
  • 高次化
  • 弱化
  • 多重化
  • 他にもある(関手圏、スパンの圏、etc.)

豊饒化とは、圏のホムセットを、集合から何らかの圏(豊穣化ベース圏; enriching category)の対象に替えることです。例えば、ホムセットをベクトル空間に替えれば、ベクトル空間の圏で豊饒化した圏ができます -- 係数体がKのとき、K-線形圏と呼んだりします。

内部化とは、何らかの圏(外部圏、環境圏)のなかで圏対象を作ることです。例えば、圏の圏Catのなかで圏対象=内部圏を作ると二重圏(double category)になります。

高次化は、2次元以上の射を追加することです。“射のあいのだ射”、“射のあいだの射のあいだの射”などを考えます。2-圏や双圏は2次元の圏です。

弱化とは、圏の条件となる結合律や単位律を、等式から何らかの同値関係へと弱めることです。モノイド圏のモノイド積は、一種の結合演算ですが、その結合律や単位律は等式としては(一般には)成立しません。法則が、等式から同型・同値に弱められています。

多重化とは、射の項数(アリティ)を増やすことです。入力項数を1からnにすると複圏(オペラッド)になります。出力項数も増やすと多圏になります。

これらの拡張方法は互いに独立ではありません。キッチリとは分類できない例がいくらでもあります。圏の圏Catを使って豊饒化すると、それは高次化した圏の例にもなります。内部圏として定義したニ重圏も、高次な圏の一種です。モノイド圏や双圏では弱化も起きています。


通常の圏論もよく知らないのに“圏の拡張”とか言われてもなー」と思う方もいるでしょうが、圏論を使おうとすると、割と早い段階で拡張せざるを得なくなるんですよ。

実は、ストリング図という絵(picture/diagram/graphics)を使うことは、「通常の圏=1次元の圏」ではあまり意味がないんです。ストリング図は平面に描くのですが、平面には左右方向と上下方向のふたつの方向がありますよね。それぞれの方向に圏の演算を対応させます。圏の演算といえば結合(composion; 合成)ですが、もし結合だけならふたつの方向は要らないです。

ふたつの方向を使うということは、結合以外に第二の演算を考えることです。第二の演算は、モノイド圏のモノイド積(monoidal product)であったり、2-圏/双圏の横結合(horizontal composition)であったりします。ストリング図を使う状況は、必然的に第二の演算を持つ圏を扱う状況、別な言い方をすると2次元的構造を持つ圏を扱う状況なんです。

圏が高次元化する現象は容易に起きるのですが、高次の圏の扱いは難しいです。その難しさを視覚的プレゼンテーションにより軽減してくれるのがストリング図です。ストリング図を使うと、テキスト記号による計算や証明が劇的に簡素化されることがあります(いつでもうまくいくわけじゃないけど)。

この劇的な効果が(適切な例により)うまく伝わるといいんだけど …

2016-11-22 (火)

テンパリー/リーブ圏とカウフマンのスケイン関係式

| 21:10 | テンパリー/リーブ圏とカウフマンのスケイン関係式を含むブックマーク

だいぶむかし -- 2008年6月、テンパリー/リーブ代数を話題にしたことがあります。

テンパリー/リーブ代数への最初の言及は2006年かな↓

明日(2016年勤労感謝の日)、テンパリー/リーブ圏の話をする機会があるので、昔を思い出してちょっと計算してみました。2008年の計算の続きと整理みたいなものです。予備知識に関しては、2008年当時のid:hiroki_fさんによる解説があります。

時間がなかったので、様子見の計算をチョロチョロしただけですが、だいたいの様子を記しておきます。

内容:

  1. 言葉と記法
  2. カウフマン圏
  3. 圏の線形化
  4. イデアルによる商線形圏
  5. テンパリー/リーブ圏の構成
  6. ブレイド図の圏
  7. カウフマンのスケイン関係式
  8. ブレイド図の圏の線形表現
  9. スケイン関係式とライデマイスター/アルチン同値関係
  10. 計算結果の解釈

言葉と記法

  1. しばしばテンパリー/リーブ図(Temperley-Lieb diagram)と呼ばれる“あのテの図”を、ここではカウフマン図(Kauffman diagram)と呼びます。図式的な表現をはじめたのはカウフマンだからです。「あのテの図」に関しては、冒頭に挙げた過去記事参照。
  2. カウフマン図の輪をサークル(円)と呼びます。(ループと呼ぶことが多いです。)
  3. カウフマン図のサークルはスカラーに置き換えて計算しますが、そのスカラーをサークル乗数と呼ぶことにします。(以前はループ乗数と呼んでいました。ループ変数とかループ因子と呼ぶこともあるようです。)
  4. kが可換体*1で、δ∈k として、δをサークル乗数とするテンパリー/リーブ圏(Temperley-Lieb category)をTL(k, δ)と書きます。可換体(スカラー体)kが了解済みならTLδと略記します。さらにδも了解済みなら単にTLと書きます。
  5. ここでは、サークル乗数δをパラメータとしてTLδと書きますが、サークル乗数とは別なパラメータを使うこともあるので注意してください。
  6. テンパリー/リーブ圏TLのエンドセットTL(n, n)は、圏の結合を乗法とする代数(多元環)となるので、これをテンパリー/リーブ代数(Temperley-Lieb algebra)と呼びます。TLA(n) := TL(n, n) とします。ひとつのテンパリー/リーブ圏内に、n = 0, 1, 2, ... でパラメトライズされた可算無限個のテンパリー/リーブ代数TLA(n)が含まれます。

今回は、係数を複素数k = C)として、「1の三乗根ω」を使った“カウフマンのスケイン関係式”を計算で確認します。

テンパリー/リーブ圏TL(k, δ)を定義するために、事前にカウフマン圏という圏を定義して、カウフマン圏の複素線形化として目的のテンパリー/リーブ圏を構成することにします。

カウフマン圏

M = (M, ・, e) をモノイドとします。M上の対合(involution)とは、次の性質を持つ写像 (-)-:M→M のことです。

  1. (a-)- = a
  2. (a・b)- = b-・a-
  3. e- = e

Mが可換モノイドなら、(a・b)- = a-・b- でもかまいません。Z = (Z, +, 0) に対して、n- := -n とすると対合になります。C×を0を除いた複素数として、C× = (C×, ・(掛け算), 1) とすると、z- = (1/zの共役) は対合になります。C×の場合、共役だけ/逆数だけでも対合になりますし、z- = z でも対合です。

以下、M = (M, ・, e, (-)-) は対合を持つ可換モノイドとします。今後は、Mの要素をギリシャ文字で書くことにします。

カウフマン図は上から下に向かって描き、カウフマン図の結合は、上下に並べて表現します。カウフマン図KとLのこの順での結合をK;Lで表します。カウフマン図の結合の具体例を次に挙げます。

モノイドMの要素δを選んで固定します。このδはサークル乗数です。モノイドMの任意の要素αとカウフマン図Kの組(α, K)を考えます。Kがサークルを持つとき、Kからサークルを1個取り除いたカウフマン図をK'とします。このとき、(α, K)と(αδ, K')は同値だとします。この同値関係*2で割った商集合を考えて、(α, K)を含む同値類を単にαKと書きます。商集合のなかでは、同値関係がイコールになるので:

  • αK = (αδ)K'

特に、

  • K = 1K = (1δ)K' = δK'

下に、サークルを乗数δに直す具体例を挙げます。

αKの形のカウフマン図をM-係数付きカウフマン図と呼びましょう。上記の定義から、“図Kのなかのサークル”と“係数αに含まれるδ因子”は相互に変換可能です。

δをサークル乗数とするM-係数付きカウフマン図を射とする圏をKauf(M, δ)と書いて、(M-係数の)カウフマン圏(Kauffman category)と呼ぶことにします。カウフマン圏の対象類は、自然数の全体 {0, 1, 2, ...} です。カウフマン圏のエンドセットはカウフマン・モノイド(Kauffman monoid)です。

カウフマン圏では、2つのカウフマン図を左右に並べることでモノイド積(テンソル積)を入れられます。空なカウフマン図がモノイド単位です。また、カウフマン図を180度回転することで双対を定義します。結合/モノイド積/双対と、M-係数のスカラー乗法との関係は次のようです。モノイド積を¥otimes、双対を(-)*で表しています。

  • (αK);(βL) = (αβ)(K;L)
  • (αK)¥otimes(βL) = (αβ)(K¥otimesL)
  • (αK)* = (α-)(K*)

双対を考えるために、Mに対合を要求しました。双対が不要ならMの対合も不要です。

圏の線形化

kを可換体として、Vectkk-ベクトル空間の圏とします。Vectkで豊饒化された圏をk-線形圏k-linear category)とも呼びます。k-線形関手、k-線形自然変換なども、Vectk豊饒化の枠組で定義します。

Cを任意の圏として、Cからk-線形圏を作ることができます。次のようにします。

  1. CのホムセットC(A, B)ごとに、自由k-ベクトル空間Link(C(A, B))を作る。ここで、Link(-)は自由k-ベクトル空間を作る操作。
  2. 圏の結合 C(A, B)×C(B, C)→C(A, C) をk-線形に拡張して、Link(C(A, B))¥otimesLink(C(B, C))→Link(C(A, C)) を作る。
  3. すると、ホムベクトル空間をLink(C(A, B))とするようなk-線形圏ができる。

テンソル積空間を使わなくても、結合を Link(C(A, B))×Link(C(B, C))→Link(C(A, C)) という双線形写像だと定義しても同じことです。

このようにして作ったk-線形圏をLink(C)と書くことにします。ホムベクトル空間に関して:

  • (Link(C))(A, B) = Link(C(A, B))

ホムセットがホムベクトル空間に変わっただけで、対象はもとの圏の対象をそのまま使っていることに注意してください。Link(C)の対象がベクトル空間だとは(一般には)言えません。

Dk-線形圏のとき、ホムベクトル空間のk-線形構造を忘れてしまえばただの圏となります。この忘却関手をUとすると、U:k-LinCatCat となります。ここで、k-LinCatk-線形圏の圏、Catは圏の圏です。安全のために、小さい圏の範囲で考えています。が、大きな圏でもたぶん大丈夫でしょう。

k-線形化する関手 Link:Catk-LinCat と、k-線形構造を忘れる関手 U:k-LinCatCat は随伴ペアになっています。

  • k-LinCat(Link(C), D) ¥stackrel{¥sim}{=} Cat(C, U(D))

¥stackrel{¥sim}{=}の左右を関手圏と考えて、¥stackrel{¥sim}{=}を圏同値と解釈しても随伴関係は成立します。

イデアルによる商線形圏

Dk-線形圏として、J⊆Mor(D) とします。ここで、Mor(D)は、Dの射全体の集合です。J∩D(A, B) をJ(A, B)と書きます。定義から、J(A, B)⊆D(A, B)。

Jがイデアルであるとは次を満たすことです*3

  1. J(A, B)はD(A, B)の部分ベクトル空間。
  2. 任意の f∈D(X, A) と h∈J(A, B) に対して、f;h∈J(X, B)。
  3. 任意の g∈D(B, Y) と h∈J(A, B) に対して、h;g∈J(A, Y)。

J(A, B) = D(A, B) と J(A, B) = {0A,B} はいずれもイデアルになります。

k-線形圏DDイデアルJに関して、新しい圏D/Jを作れます。次のようにします。

  1. |D/J| := |D|
  2. (D/J)(A, B) := D(A, B)/J(A, B) (商ベクトル空間)
  3. 結合(composition)と恒等射(identity)はうまいこと定義する。

「うまいこと」を詳しく述べませんが、Jがイデアルであることからうまいこと定義できます。

商線形圏の事例として、セットイド豊饒圏について述べます。集合に同値関係が載った構造をセットイド(setoid、亜集合)と呼び、セットイドを対象として、同値関係を保存する写像を射とする圏をSetoidとします。圏Setoidは、集合の直積をモノイド積として対称モノイド圏だと考えます。

いま、CSetoid豊饒圏だとします。つまり、C(A, B)はセットイドです。ホムセットイドC(A, B)上の同値関係を〜A,Bとします。が、たいていの場合、下付きのA,Bは省略します。

D := Link(C) と置きます。CDに埋め込めば、CDの広い部分圏*4だとみなせます。f, g∈C(A, B)で、f〜g であるf, gにより f - g と書けるD(A, B)の要素から生成された部分ベクトル空間をJ~(A, B)とします。そして、J~(A, B)をすべて寄せ集めた作ったDの射の集合をJとします。

JDイデアルになります。したがって、商線形圏D/Jを作れます。一方で、(C/〜)(A, B) := C(A, B)/〜A,B と定義して圏C/〜を作れます。これらのあいだには、次の圏同値が成立します。

  • (Link(C))/J ¥stackrel{¥sim}{=} Link(C/〜)

この同値はk-線形な同値です。ホムベクトル空間ごとに、次のようなベクトル空間の同型を導きます。

  • Link(C(A, B))/J(A, B) ¥stackrel{¥sim}{=} Link(C(A ,B)/〜A,B) in Vectk

テンパリー/リーブ圏の構成

圏のk-線形化とイデアルによる商線形圏の準備ができたので、これらを使ってテンパリー/リーブ圏を構成できます。

C×を0を除いた複素数として、z- = (1/zの共役) とすれば、(C×, ・(掛け算), 1, (-)-) は対合を持つ可換モノイドとなります(実際には可換群になってます)。δを非零複素数として、Kauf(C×, δ) を定義できます。δをサークル乗数とするカウフマン圏です。このカウフマン圏は、非零複素数によるスカラー乗法を持ちますが、線形構造を持つわけではありません。

Kaufδを複素線形化しましょう。LinC(Kaufδ)を作ります。これで、C-線形圏ができました。LinC(Kaufδ) は長たらしいので、LKδ(linearlized Kauffman)と略記します。δを省略することもあります。

Kaufδの射である非零複素係数付きカウフマン図は、LKδのホムベクトル空間の基底になります。ホムベクトル空間の基底とみなした係数付きカウフマン図は、《αK》のようにギュメで囲むことにします。

LKの射、つまりホムベクトル空間のベクトルXは、

  • X = Σii《αiKi》)

のような一次結合の形で書けます。ここで、ξi, αiは非零複素数です。番号iは適当な範囲で動かします。

非零複素数αとカウフマン図Kに対して、α《K》 - 《αK》 の形のベクトルで生成されるホムベクトル空間の部分ベクトル空間をすべて寄せ集めてJとします。Jはイデアルになります。例えば、α《K》, 《αK》∈LK(A, B)、《βL》∈LK(B, C) とすると:

  (α《K》 - 《αK》);《βL》
= (α《K》);《βL》 - 《αK》;《βL》
= α《βK;L》 - 《α(βK;L)》

なので、J(A, C)に入ります。

このイデアルJでホムベクトル空間達を割り算すれば、商ベクトル空間では、等式 α《K》 = 《αK》 が成立します。要するに商ベクトル空間では、カウフマン圏におけるスカラー乗法と、線形化した後のスカラー乗法がシームレスに計算可能だ、ということです。この事実を利用すると、LK/Jの射Xを、サークルを持たないカウフマン図Kiを使って

  • X = Σii《Ki》)

の形に書けます。この形は、図からサークルを除去した標準形(正規形、既約形)となります。

今作ったLKδ/Jがテンパリー/リーブ圏TLδです。

  • TLδ := LKδ/J = (LinC(Kaufδ))/J

ブレイド図の圏

はじめての圏論 中間付録B:アミダとブレイド」で定義したブレイド図の圏を考えます。ブレイド図は、真っ直ぐな紐と以下の2つの交差から結合(縦に並べる)とモノイド積(横に並べる)で作られる図です。(2つの交差のどっちを正にするかは好みの問題です。)対象は自然数(横木上の点の数)です。

ブレイド図の圏をBrDiagとして、正負の交差を B+, B-:2→2 in BrDiag とします。「はじめての圏論 中間付録B:アミダとブレイド」で注意したように、ブレイド図は“みたままの図形”でイソトピー(に相当する同値関係)による同一視はしてません。したがって、結合/モノイド積すると交差が増える一方で、可逆射は恒等射だけです。

通常ブレイドと言うと、B+;B- = id2 などを仮定します。この状況を記述するために、圏BrDiagSetoid-豊饒圏としましょう。

BrDiagのホムセットBrDiag(n, n)ごとに(n ≠ m ならBrDiag(n, m)は空なので考える必要はない)、ライデマイスターII移動とライデマイスターIII移動により生成される同値関係を考えます。この同値関係をアルチン関係式とも呼ぶので、ここではライデマイスター/アルチン同値関係(Reidemeister-Artin equivalence relation)と呼び、記号 〜RA で表すことにします。以下で、¥otimesはモノイド積、Iはid1のことです。

  1. B+;B-RA B-;B+RA id2
  2. (I¥otimesB+);(B+¥otimesI);(I¥otimesB-) 〜RA (B-¥otimesI);(I¥otimesB+);(B+¥otimesI)

二番目のライデマイスターIII移動は次の図で表されます。

なお、ライデマイスターIII移動の記述にはいくつか変種があります。ここでは、手前の正の交差の奥にある紐を左右に動かしています。

BrDiagは、完全に組み合わせ的に定義できますが、BrDiag上の〜RAは、ブレイドの幾何的な定義におけるイソトピー同値に相当します。例えば、次のイソトピー変形は、組み合わせ的ライデマイスターII移動を2度行う操作に対応します。

以下では、ブレイド図の圏BrDiagには、同値関係〜RAを一緒に考えてセットイド豊饒圏とみなします。圏のk-線形化で述べた事実により、次が成立します。

  • (Link(BrDiag))/JRA ¥stackrel{¥sim}{=} Link(BrDiag/〜RA)
  • Link(BrDiag(n, n))/JRA(n, n) ¥stackrel{¥sim}{=} Link(BrDiag(n, n)/〜RA)

カウフマンのスケイン関係式

カウフマンのブラケット多項式というもの(ここではその内容に踏み込まない)を定義するとき、次のような不思議な関係式を使うんですよ。

僕は何のことだかサッパリ分かりませんでした。今でも分かってないです。ともかくも、図形にスカラー係数を付けた一次結合のあいだの等式をスケイン関係式(skein relation)と呼ぶので、これは一種のスケイン関係式です。以下、カウフマンのスケイン関係式として参照します。

上記一番目の等式では、サークルを付け加えるとスカラー(-A2 - A-2)が外に出るので、(-A2 - A-2)をサークル乗数とみなせ、ということらしいです。二番目は、ブレイドの生成元がテンパリー/リーブ射(TLの射)と何らかの意味で同値だと言っているようです。

… … ウーム、わからん。

ちょっと解釈を変えて、ブレイド図の圏BrDiagからテンパリー/リーブ圏TLへの関手の定義だとみなしましょう。この解釈なら、(天下りの誹りを免れないが)関手の定義としてハッキリとした意味を与えられそうです。以下でやってみます。

ブレイド図の圏の線形表現

Cを任意の圏として、Vk-線形圏とします。CからVへの関手をCk-線形表現k-linear representation)と呼びます。CVがモノイド積を持つときは、線形なモノイド関手をk-線形表現とします。以下では、モノイド積は厳密モノイド積だけを考えます。

この言葉遣いが、通常の「線形表現」と矛盾しないことを確認しましょう。Mをモノイド(あるいは群)として、Mの線形表現は、圏とみなしたMからVectkへの関手となります。k係数行列圏Matkへの関手なら行列表現となります。よって、上記の「圏の線形表現」は、モノイド/群の線形表現/行列表現の拡張となっています。

複素係数テンパリー/リーブ圏TLδは、C-線形モノイド圏です。したがって、ブレイド図の圏BrDiagからTLδへの線形モノイド関手はC-線形表現です。線形表現 F:BrDiagTLδ があれば、それをBrDiagC-線形化圏にまで拡張した LinC(BrDiag)→TLδ が定義できます。

さて、カウフマンのスケイン関係式を使って線形表現 F:BrDiagTLδ を具体的に定義しましょう。次の図が参考になります。

*5

複素定数Aとしては「1の三乗根ω」を使います。ω = (-1 + √(-3))/2 です。-(ω-2 + ω2) = 1 なので、サークル乗数は1とします。サークルは単に消してしまっていいわけです。

なお、スケイン関係式に登場した定数Aとサークル乗数δのあいだの関係は、

  • δ = c(A-n + An)

を使うようです。今回のケースでは、c = -1, n = 2 です。Aとδの関係が何に由来するか、僕は知りません。やってみると結果オーライではありますが。

線形表現Fを露骨に書き下すために、もう少し記号の約束をします: キャップ形、カップ形のカウフマン図を∩、∪で表します。∩:0→2, ∪:2→0 in Kaufδ です。カウフマン圏Kaufδはテンパリー/リーブ圏TLδに埋め込めるので、∩:0→2, ∪:2→0 in TLδ ともみなせます。

H := ∪;∩ : 2→2 in TLδ と置きます。また、id2, id3をI2, I3とも書きます。それと、ω' = (-1 - √(-3))/2 とします。ω'はωの逆数であり共役でもあります。

以上の記号の約束のもとで、C-線形表現 F:BrDiagTL1 を次のように定義します。

  • 対象nについては、F(n) := n
  • F(B+) := ωH + ω'I2
  • F(B-) := ω'H + ωI2

これだけ定義すれば、Fが(厳密な)モノイド関手であることからBrDiag全体に拡張できます。拡張の指導原理となる法則は:

  • F(idn) = idF(n) = idn
  • F(n + m) = F(n) + F(m) (対象のモノイド積は足し算)
  • F(X;Y) = F(X);F(Y)
  • F(X¥otimesY) = F(X)¥otimesF(Y)

ブレイド図の圏BrDiagには、ライデマイスター/アルチン同値関係〜RAがあります。線形表現関手Fは、ライデマイスター/アルチン同値関係とどう関わるでしょうか? それを次節で探ります。

スケイン関係式とライデマイスター/アルチン同値関係

とりあえず、次の4つの値を計算しましょう。

  1. F(B+;B-)
  2. F(B-;B+)
  3. F(I¥otimesB+);(B+¥otimesI);(I¥otimesB-)
  4. F((B-¥otimesI);(I¥otimesB+);(B+¥otimesI))


ここから先の計算では、テンパリー/リーブ圏TLでの結合は単に併置でも書くことにします。併置が図式順結合であることに注意してください。

  F(B+;B-)
= F(B+)F(B-)
= (ωH + ω'I2)(ω'H + ωI2)
= ωω'HH + ωωHI2 + ω'ω'I2H + ω'ωI2I2
= H + ω'H + ωH + I2
= (1 + ω' + ω)H + I2
= I2

途中で、ω, ω'に関する次の等式を使っています。

  • ωω' = ω'ω = 1
  • ωω = ω'
  • ω'ω' = ω
  • 1 + ω' + ω = 0 (ω' + ω = -1)

また、

  • HH = H;H = H (δ = 1 なので)
  • HI2 = H;I2 = H
  • I2H = I2;H = H
  • I2I2 = I2;I2 = I2

同じように計算すると、F(B-;B+) = I2 なので、

  • F(B+;B-) = F(B-;B+) = F(id2)

計算を続けるにあたって、X;Y を [X, Y] と書いていいことにします。カンマは優先順位が低いセミコロン(圏の結合)として使います。id1 = I, id2 = I2, id3 = I3 と書いて、「圏論勉強会:3点テンパリー/リーブ代数の掛け算九九」で導入した次の記号も使います。

掛け算の表は次のとおり。

ただし、↑の表は δ = 2 のものですから、δ = 1 に読み替えてください。

では計算します。

  F((I¥otimesB+);(B+¥otimesI);(I¥otimesB-))
= [F(I)¥otimesF(B+),
   F(B+)¥otimesF(I),
   F(I)¥otimesF(B-)]
= [I¥otimes(ωH + ω'I2),
   (ωH + ω'I2)¥otimesI,
   I¥otimes(ω'H + ωI2)]
= [ ωW + ω'I3,
   [ωU + ω'I3,
    ω'W + ωI3]]
= [ ωW + ω'I3,
    UW + ωωUI3 + ω'ω'I3W + I3I3]
= [ ωW + ω'I3,
    R + ωωU + ω'ω'W + I3]
= ωWR + WU + ω'WW + ωWI3 + ω'I3R + ωI3U + I3W + ω'I3I3
= ωW + L + ω'W + ωW + ω'R + ωU + W + ω'I3
= ω'I3 + ωU + (ω + ω' + ω + 1)W + ω'R + L
= ω'I3 + ωU + ωW + ω'R + L

複素数ω, ω'の計算の他に、I¥otimesH = W, I¥otimesI2 = I3 などのカウフマン図のテンソル積計算もしています。

  F((B-¥otimesI);(I¥otimesB+);(B+¥otimesI))
= [F(B-)¥otimesF(I),
   F(I)¥otimesF(B+),
   F(B+)¥otimesF(I)]
= [(ω'H + ωI2)¥otimesI,
   I¥otimes(ωH + ω'I2),
   (ωH + ω'I2)¥otimesI]
= [[ω'U + ωI3,
    ωW + ω'I3],
    ωU + ω'I3]
= [ UW + ω'ω'UI3 + ωωI3W + I3I3,
    ωU + ω'I3]
= [ R + ω'ω'U + ωωW + I3,
    ωU + ω'I3]
= ωRU + ω'UU + WU + ωI3U + ω'RI3 + UI3 + ωWI3 + ω'I3I3
= ωU + ω'U + L + ωU + ω'U + ω'R + U + ωW + ω'I3
= ω'I3 + (ω + ω' + ω + 1)U + ωW + ω'R + L
= ω'I3 + ωU + ωW + ω'R + L

以上の計算から次が言えます。

  • F((I¥otimesB+);(B+¥otimesI);(I¥otimesB-)) = F((B-¥otimesI);(I¥otimesB+);(B+¥otimesI))

計算結果の解釈

あー疲れた。時間もない。あとは急ぎ足で、何を計算したのかを解釈してみます。細部を確認してないので、大雑把な話です。

線形表現 F:BrDiagTL(C, 1) をカウフマンのスケイン関係式に基づいて定義すると、「ブレイド図の圏BrDiagをライデマイスター/アルチン同値関係で割った圏BrDiag/〜RAを、テンパリー/リーブ圏TL1に埋め込めるよ」というのが今回の話のエッセンスです。

前節の計算から、X 〜RA Y ならば F(X) = F(Y) が言えます。X 〜RA Y であるX, Yから作った X - Y という形のベクトル達は、イデアルJRAを生成します。F(X - Y) = F(X) - F(Y) = 0 であることから、イデアルJRAは、線形表現Fの核(kernel)に入ります。

というわけで JRA ⊆ Ker(F) は言えてます。逆向きの包含 Ker(F) ⊆ JRA もたぶん確認できるでしょう。普通の線型代数と同様な準同型定理が成立するなら(大丈夫そう)、(LinC(BrDiag))/JRA ¥stackrel{¥sim}{=} (LinC(BrDiag))/Ker(F) ¥stackrel{¥sim}{=} Im(F) が言えます。Im(F)は、k-線形関手Fの像である部分圏を表します。

(LinC(BrDiag))/JRAはLinC(BrDiag/〜RA)と同一視可能なので、LinC(BrDiag/〜RA)とIm(F)も同一視できます。これは、ブレイド図達をライデマイスター/アルチン同値関係で割ったモノから張ったベクトル空間達は、テンパリー/リーブ圏のなかにスッポリ入り込むことを意味します。この埋め込みが、カウフマンのスケイン関係式から作られた線形表現Fで実現されるわけです。

希望的観測で詰めの甘い話をしてますが、だいたいはこんなストーリーだと思います。

*1可換環でも議論できますが、割り算が出来たほうが便利なので体とします。

*2:正確には、関係 (α, K)〜(αδ, K') から生成された最小の同値関係。

*3:モノイド積(テンソル積)に関する条件を付けることもありますが、ここではモノイド積を考慮しません。

*4CDの広い部分圏(broad subcategory, wide subcategory)であるとは、|D| = |C| のことです。

*5:画像: https://arxiv.org/pdf/0910.2974v1.pdf より

2016-11-14 (月)

モンスター・小林優香選手

| 11:37 | モンスター・小林優香選手を含むブックマーク

ガールズケイリンの小林優香選手

*1

こっ、この太もも、筋肉のかたまり、とんでもないパワーが出そうだ。こりゃ無敵なわけだ。

今年は怪我や手術で欠場が多かったようですが、2016-11-09の西日本新聞のニュースによると、久留米F1で復帰とのこと。近況成績では「1着、1着、1着」。やはりツオイ。すげー。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20161114

2016-11-12 (土)

言葉の問題だと片付けたがる人々

| 14:53 | 言葉の問題だと片付けたがる人々を含むブックマーク

「ネイティブ広告ハンドブック」という語がなんか目立っていたので、これ何だろう? と思って、境治〈さかい・おさむ〉さんという方の記事

をチラ読みしました。『ネイティブ広告ハンドブック』という本(冊子)の文章がヘタッピで貶〈けな〉されているけど内容は良いよ、ということらしい。別に変なことも書いてないけど、それがどうした?問題の所在が分からない。

どうも、問題は「文章がヘタッピ」とかではなかったようです。

ウンギャー! 「蹴鞠おじさん」達の言動が醜悪すぎるわ。蹴鞠おじさんの一人・高広伯彦さん曰く:

  • 僕に「メディア」の話させたらながくなりますよ?
  • マクルーハンって知ってますか?

ゲゲゲ、ここまで来るとまるで漫画で、スノビズムの標本みたいな人だね。

境治さんは、本の文章(表現、言葉)が貶されているという短絡的認識で本と著者達を擁護してますが、なんでそんな解釈になっちゃうんだろう? 文章自体をそこまで問題にする人なんて、そんなにいませんよ。

僕を大いに怒らせた長谷川秀夫さんにしろ、その少し前の長谷川豊さんにしろ、「言葉が至らなかった」「表現が不適切であった」と弁明や謝罪をしているけど、それは論点をズラしているだけ。

長谷川/長谷川/境の各氏とも、詭弁の技法として論点をズラしているというより、本気で「表現法を批難された」と思っているみたい。「なんでそんな解釈になっちゃうんだろう?」の答は、「認識の枠組がそういう構造になっている」ということで、どうにもならないでしょうね。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20161112