モノイドに関する淡中再構成定理がだいたいどんなものかを述べます。そして、淡中再構成定理の証明の特徴を述べます。証明の特徴は、長いけど無技巧〈trickless〉で淡々としていることです。この記事内では定義を書いてないので雰囲気だけですが、淡中再構成定理のベースとなる命題達も紹介します。$`\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\u}[1]{ \underline{#1} }
\newcommand{\id}{ \mathrm{id}}
\newcommand{\op}{ \mathrm{op}}
\newcommand{\In}{ \text{ in }}
\newcommand{\hyp}{\text{－} }
%\newcommand{\EQV}{\mathrel{\overset{\sim}{\equiv}} }
`$
内容：
ハブ記事：
淡中再構成定理とは
モノイドに関する淡中再構成定理〈Tannaka reconstruction theorem〉の主張〈ステートメント〉は次のようなものです； モノイド $`M`$ が与えられたとき、$`M`$ から“とある手続き”により作られたモノイド $`\widetilde{M}`$ は、もとの $`M`$ と同型である（下）。
$`\quad M \cong \widetilde{M} \In \mbf{Mon}`$
もちろん、“とある手続き”が問題となります。ひとつポイントとなるのは、淡中再構成が、モノイドの表現の圏を経由していることです。$`M`$ の表現達からなる圏 $`\mrm{Repr}(M)`$ と忘却関手 $`\mrm{U}: \mrm{Repr}(M) \to \mbf{Set}`$ を素材としてモノイド $`\mrm{Tann}(\mrm{Repr}(M), U)`$ が作られ、それが $`\widetilde{M}`$ です。
$`\quad \widetilde{M} := \mrm{Tann}(\mrm{Repr}(M), U)`$
淡中再構成の手順は、表現の圏の構成（前段）と、圏と忘却関手からのモノイドの構成（後段）の二段階に分けることができます。
$`\quad \xymatrix@C+1pc{
M \ar@{|->}[r]^-{\mrm{Repr}(\hyp)} \ar@{|->}@/_2pc/[rr]_{\text{淡中再構成} }
& {\mrm{Repr}(M) \text{ with }\mrm{U} } \ar@{|->}[r]^-{\mrm{Tann}}
& \widetilde{M}
}`$
もとのモノイドが未知でも、表現の圏（と忘却関手）さえ分かれば、そこから $`\mrm{Tann}`$ を使ってモノイドを絞り出せるんだ、とも言えます。
モノイドではなくて群の場合でも、同じ手順で淡中再構成が行えます。環やホップ代数の淡中再構成では、話が複雑になります。
長大無技巧な証明
淡中再構成定理の証明では、天啓のヒラメキやトリッキーな技〈わざ〉は一切出てきません。定義から直ちに導けるような簡単な命題と単純な計算を淡々と積み上げていくだけです。準備段階である補題を示すステップは短く単純です。しかし、補題達を積み上げる過程は長くなります。
これといった技巧は使わず、簡単な命題と単純な計算を延々と積み上げるタイプの証明を長大無技巧な証明〈long and trickless proof〉と呼ぶことにします。淡中再構成定理の証明は、典型的な長大無技巧な証明です。
長大無技巧な証明では、「オオーッ」と感嘆・感動するようなことは何もないので、面白くないかも知れません。圏論の定理では、面白みのない無技巧な証明が多いような気がします。2008年4月に書いた記事「自己関手の圏とモナド // 余談：圏論は、ほぼ計算だけ」で次のように書いています：
圏論は、抽象的な印象を受けます（事実、まー抽象論と言っていいでしょう）が、定義を理解したら（いや、理解できなくても）、あとは計算するだけです。僕はモノグサなので、計算の手間を嫌って他の手段で理解しようと試みたりしますが、結局我慢して計算するハメになります。教訓としては、四の五の言ってないで計算するほうがいいと思います。
記法管理と単純計算術
ヒラメキやトリックが出てこない長大無技巧な証明では、記法管理〈notation management〉と単純計算術〈simple calculation skills〉が重要になります。
ひとつひとつは単純な概念でも、長大な積み上げ過程を経るとそれなりに複雑になります。組み合わさって複雑化した概念を律儀に書き表すとだいぶ煩雑なものになります。例えば、最初の節の $`\widetilde{M}`$ の定義を律儀に書き表すと次のようになります。
$`\quad \widetilde{M} := \mrm{End}_{[\mrm{LeftRepr}_{\mbf{Set}}(M), \mbf{Set}]_{\mbf{CAT}} }( \mrm{Und}_{\mrm{LeftRepr}_{\mbf{Set} }(M) }: \mrm{LeftRepr}_{\mbf{Set}}(M)\to \mbf{Set} )`$
これは鬱陶しい！ 略記を使ってスッキリさせます。
$`\quad \widetilde{M} := \mrm{End}_{M^{\wedge \vee}}( \mrm{U}_{M} )`$
スッキリしました。スッキリするのはいいのですが、スッキリさせるために、いつどのような略記を使ったのかを帳簿管理しなければなりません。これは、シリーズ最初の記事「モノイドと群の淡中再構成 1/n // 省略系列と補完系列」で述べた、記法の省略系列と補完系列をキッチリ管理すること-- 記法管理です。
さて、前節で引用した過去記事の言葉「圏論は、ほぼ計算だけ」の「計算」は、ヒラメキやトリックを必要としない愚直な単純計算術です。実際に使われる計算体系は、関手のラムダ計算です。通常「ラムダ計算」と言うと、それは関数の計算術ですが、それを関手（や自然変換）に拡張した計算体系です。関数計算と関手計算のあいだには、以下の表のような対応があります。
| 関数計算 | 関手計算 |
|---|---|
| 集合 | 圏 |
| 関数集合 | 関手圏 |
| 多変数関数 | 多項関手 |
| カリー化 | カリー化 |
| 高階関数 | 高階関手 |
高階関数とは、引数として関数を受け取ったり、戻り値として関数を返すような関数でした。同様に、高階関手〈higher-order functor〉は、引数として関手や自然変換を受け取ったり、戻り値として関手や自然変換を返すような関手です。高階関手の計算、すなわち関手のラムダ計算は必須なスキルです。
淡中再構成の基礎部分
淡中再構成定理の長大無技巧な証明は、次の3つの部分に分けることができるでしょう。
- 圏の一般論からの準備
- 米田の補題と米田埋め込み
- モノイド（と群）の表現に関する準備
まだ定義してない用語を使ってしまって概要を述べましょう。圏の一般論からは、次のような命題を準備します。
- 2つの充満忠実な関手の結合は、充満忠実である。（これは簡単。）
- 自己射モノイド割り当て〈endmorphism monoid {assignment | assigning}〉$`\mrm{End}_{\hyp}`$ は、プロファイルが $`\mbf{Cat}\to \mrm{Fam}(\mbf{Mon}) `$ である関手となる。
- 関手 $`F`$ が充満忠実なら、$`\mrm{End}_F`$ は、ファイバーごとに同型な〈isomorphic-on-fibers〉ファミリー射〈family morphism | morphism between families〉となる。
米田埋め込みに関する命題達は：
- 米田埋め込みは、共変な充満埋め込み関手（対象上で単射な充満忠実関手）となる。
- 余米田埋め込みは、反変な充満埋め込み関手となる。
- 米田埋め込みの後に余米田埋め込みを結合した二階米田埋め込みは、反変な充満埋め込み関手となる。
- 評価関手〈{evaluation | evaluator} functor〉は、米田埋め込みで余表現される。
評価関手のカリー化として淡中変換*1を定義すると、次が言えます。
- 淡中変換と二階米田埋め込みは同じものである。
- 二階米田埋め込みは充満埋め込み関手なので、淡中変換も充満埋め込み関手である。
- 特に、淡中変換は充満忠実である。
これらの圏論的な命題達と、モノイド（と群）の表現に特有な幾つかの定義と事実を組み合わせると、淡中再構成の手順と同型性が得られます。長めの積み上げ過程をたどりますが、まったく無技巧〈trickless〉です。
そしてそれから
「高階関手の計算、すなわち関手のラムダ計算は必須なスキルです」と言ったので、次は（たぶん）関手のラムダ計算の話です。過去に何度か、関手のラムダ計算を散発的に話題にはしてますが、まとまってないからな。
*1:別な文脈では、ゲルファント変換〈Gelfand transform〉と呼ばれます。圏論版のゲルファント変換が淡中変換です。
