このブログの更新は X(旧Twitter)アカウント @m_hiyama で通知されます。
Follow @m_hiyama

ご連絡は上記 X アカウントに DM にてお願いします。

[参照用 記事]

カリー化、内部ホム、カックンカックンのストリング図

モノイド閉圏、トレース付きモノイド圏、コンウェイ圏(不動点オペレーター付きデカルト圏)は、モノイド圏にカリー化、トレース、不動点というオペレーターを載せた構造です。これらの圏の計算では、ストリング図を使うのが便利です。

このブログでは、図式の描画に園部さんの XyJax(Xy-pic の MathJax 版)を使っています。XyJax は可換図式には非常に便利で、ペースティング図もなんとか描けます。が、ストリング図には向いていません。向いてないけど、カリー化を無理して描いてみます。(トレースと不動点は、いずれまた。)

記事内で使う文字の色については「文字の色の約束(再確認)」を参照してください。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\u}[1]{\underline{#1} }
%\newcommand{\o}[1]{\overline{#1} }
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{-} }
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\T}[1]{ \text{#1} }
\newcommand{\op}{\mathrm{op} }
\newcommand{\id}{\mathrm{id} }
%\newcommand{\pto}{\nrightarrow} % proarrow to
%\newcommand{\dto}{\looparrowright} % dependent to
%\newcommand{\hto}{\rightsquigarrow} % hetero to
%\newcommand{\parto}{\supset\!\to}
%\newcommand{\twoto}{\Rightarrow}
%\newcommand{\C}{\mathop{;}} % Composition
\newcommand{\lhom}{ \multimap}
\newcommand{\rhom}{\mathop{\style{display: inline-block; transform: rotate(180deg)}{\multimap}} }
`$

内容:

カリー化と内部ホム

$`\cat{C} = (\cat{C}, \otimes, \mrm{I})`$ を、対称性は仮定しないモノイド圏だとします。

「カリー化」や「指数」という言葉は、デカルト圏(正確にはデカルト・モノイド圏)の場合に使いますが、ここではデカルト圏じゃなくても「カリー化」「指数」を使います。デカルト圏と非デカルト圏で言葉づかいを変えても別にいいことないので。

次のホムセット同型が成立するとき、$`X`$ は、$`A`$ と $`C`$ の内部ホム対象〈internal hom object〉または指数対象〈exponential object〉と呼びます。

$`\quad \cat{C}(A\otimes B , C) \cong \cat{C}(B, X) \In \mbf{Set}`$

$`X`$ を、$`[A, C]`$ と書くことが多いですが、ここでは $`A \lhom C`$ と書きます。つまり:

$`\quad \cat{C}(A\otimes B , C) \cong \cat{C}(B, A\lhom C) \In \mbf{Set}`$

たまたま選んだ $`A, B, C`$ に対して同型が成立しているだけでは面白くないので、$`(A\otimes \hyp)`$ という関手の左随伴関手が $`(A \lhom \hyp)`$ になる状況を考えます。これは次のように書けます。

$`\T{For }A \in |\cat{C}|\\
\quad \cat{C}(A\otimes \hyp, \hyp) \cong \cat{C}(\hyp, A \lhom \hyp) \In [\cat{C}^\op \times \cat{C}, \mbf{Set}]
`$

この書き方は、反変・共変の二項関手〈双関手〉達の関手圏 $`[\cat{C}^\op\times \cat{C}, \mbf{Set}]`$ における同型=自然同型です。詳しくは「省略したら分かるわけない: 随伴関手対を例に」を参照してください。

ロリポップ記号 '$`\lhom`$' (LaTeX では \multimap)は、もともとは線形論理の含意〈線形含意 | linear implication〉として使われていた記号ですが、ストリング図を写し取る“象形文字”として便利です(後述)。

$`\cat{C}`$ に対称性は仮定してなかったので、$`(A\otimes \hyp)`$ とは別に $`(\hyp\otimes B)`$ という関手とその左随伴関手も考える必要があります。その場合は次のように書きます。

$`\T{For }B \in |\cat{C}|\\
\quad \cat{C}(\hyp\otimes B, \hyp) \cong \cat{C}(\hyp, \hyp \rhom B) \In [\cat{C}^\op \times \cat{C}, \mbf{Set}]
`$

随伴系〈adjoint system | adjunction〉(「省略したら分かるわけない: 随伴関手対を例に // 随伴関手対」参照)を定義する自然同型〈可逆自然変換〉(の成分)を次のように書きます。

$`\T{For }A, B, C \in |\cat{C}|\\
\quad \mrm{LCurry}^A_{B, C} : \cat{C}(A\otimes B, C) \to \cat{C}(B, A \lhom C) \In \mbf{Set}\\
\quad \mrm{LUnCurry}^A_{B, C} : \cat{C}(B, A \lhom C) \to \cat{C}(A\otimes B, C) \In \mbf{Set}\\
\quad \mrm{RCurry}^B_{A, C} : \cat{C}(A\otimes B, C) \to \cat{C}(A, C \rhom B) \In \mbf{Set}\\
\quad \mrm{RUnCurry}^B_{A, C} : \cat{C}(A, C \rhom B) \to \cat{C}(A\otimes B, C) \In \mbf{Set}
`$

上の式に出現する関数〈写像 | 集合圏の射〉や対象を次のように呼びます。

  • $`\mrm{LCurry}^A_{B, C}`$ : 左カリー化〈left Currying〉
  • $`\mrm{LUnCurry}^A_{B, C}`$ : 左反カリー化〈left unCurrying〉(左カリー化の逆関数)
  • $`\mrm{RCurry}^B_{A, C}`$ : 右カリー化〈right Currying〉
  • $`\mrm{RUnCurry}^B_{A, C}`$ : 右反カリー化〈right unCurrying〉(右カリー化の逆関数)
  • $`A \lhom C`$ : 左内部ホム対象〈left internal hom object〉 または 左指数対象〈left exponential object〉
  • $`C \rhom B`$ : 右内部ホム対象〈right internal hom object〉 または 右指数対象〈right exponential object〉

これらのカリー化(の仲間達)と内部ホム(の仲間達)を図示することが今回の話題です。

対象と恒等射をワイヤーで表す

ストリング図では、ワイヤーで対象を表し、ノード(ボックスや丸いオダンゴ)で射を表します。ワイヤーは恒等射を表すこともあります。

以下の図は、「ボブ・クック教授による、対称とは限らないモノイド閉圏における絵の描き方」からの再掲です。

これは、対象でもあり(ときに)恒等射でもあるワイヤーの描き方です。左から $`A \otimes B`$(モノイド積 | テンソル積)、$`A \lhom B`$(左内部ホム)、$`A \rhom B`$(右内部ホム)です。

ロリポップ記号 $`\lhom,\; \rhom`$ は前節に出てきました。ロリポップ記号で繋がれた二本のワイヤーが逆向きな点に注意してください。「逆行する2本のワイヤーがロリポップで繋がる」という描画が、内部ホムやカリー化をうまく表現します。

バエズ〈John C. Baez〉は、ロリポップを留め金〈clasp〉と呼んでました。バエズ自身が描いた「ラムダ計算のベータ変換」の絵は次のようです(「バエズとステイのロゼッタストーン論文と現代のヒエログリフ」から再掲)。

逆行する2本のワイヤーを“留め金”で繋いでいます。

$`f: A\otimes B \to C \In \cat{C}`$ に対する $`\mrm{LCurry}^A_{B, C}(f)`$ と $`\mrm{RCurry}^B_{A, C}(f)`$ は次のように描きます(「モノイド閉圏、オダンゴ、留め金、池袋」より再掲)。

これを、なんとか XyJax で描いてみます。

なんとかして描く

$`\mrm{LCurry}^A_{B, C}(f)`$、とりあえず頑張ってみます。

$`\quad \xymatrix{
{} \ar[drr]_A
&{}
&{}
&{} \ar[dl]^B
\\
{}
&{}
& *++[o][F]{f} \ar[d]^C
&{}
\\
{}
&{\cdot} \ar@{-}[r] \ar@/^1pc/[uul]^A
&{\circ} \ar[d]^C
&{}
\\
{}
&{} \ar[u]^A
&{}
&{}
}
`$

ウーム、頑張ってはみたものの:

内部ホム〈指数〉のワイヤーを「逆行する2本のワイヤーを留め金〈ロリポップ〉で繋ぐ」のは諦めて、一本の下向き矢印で描くことにします。

$`\quad \xymatrix{
{} \ar[dr]_A
&{}
&{} \ar[dl]^B
\\
{}
& *++[o][F]{f} \ar[d]^C
&{}
\\
{}
&{\lhom} \ar[d]^{A\lhom C} \ar@/^1pc/[uul]^A
&{}
\\
{}
&{}
&{}
}
`$

左上ベンドがカックンなのは我慢しましょう。カックンが気になるってのもありますが、レイアウトが複雑になると、逆方向・斜め方向に走るワイヤーがむしろ邪魔になることもあります。次の描画法で回避することにします。

$`\quad \xymatrix{
{\#1} \ar[dr]_A
&{}
&{} \ar[dl]^B
\\
{}
& *++[o][F]{f} \ar[d]^C
&{}
\\
{\#1}
&{\lhom} \ar[d]^{A\lhom C} \ar[l]^A
&{}
\\
{}
&{}
&{}
}
`$

ここで $`\#1`$ は番号です。同じ番号の端点は繋ぐという目印です。自然演繹の証明図(の含意導入)では同じように番号で対応箇所を示す方法が使われます。

象形文字

$`\mrm{LCurry}^A_{B, C}(f)`$ という書き方は正確ですが煩雑です。代わりに $`{^\cap f}`$ という略記が便利です。この書き方は、短いだけでなく、左上にベンド(曲がり)があるストリング図のイメージを写し取っています。ベンドがカックンな様子を写し取るなら $`{^\wedge f}`$ がいいかも知れません。

$`{^\wedge f}`$ と $`f^\wedge`$ は、ベンドがカックンなストリング図の象形文字として使えるでしょう。

$`{^\wedge f} : B \to A \lhom C\\
\quad \xymatrix{
{} \ar[dr]_A
&{}
&{} \ar[dl]^B
\\
{}
& *++[o][F]{f} \ar[d]^C
&{}
\\
{}
&{\lhom} \ar[d]^{A\lhom C} \ar@/^1pc/[uul]^A
&{}
\\
{}
&{}
&{}
}
`$

$`f^\wedge : A \to C \rhom B\\
\quad \xymatrix{
{} \ar[dr]_A
&{}
&{} \ar[dl]^B
\\
{}
& *++[o][F]{f} \ar[d]^C
&{}
\\
{}
&{\rhom} \ar[d]^{C\rhom B} \ar@/_1pc/[uur]_B
&{}
\\
{}
&{}
&{}
}
`$