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

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

サイトと層の大きさやら作り方やら

3日前に書いた記事「ビッグサイト微分幾何と自然変換の上付き添字」で「ビッグサイト」という言葉を使ったのですが、この言葉の典拠はnLab項目です。

nLabには、他にラージサイト、スモールサイト、リトルサイトの項目もあります。

しかし、形容詞ラージ/スモール/ビッグ/リトルは、すべてが大きさを分類しているわけではありません。ラージ/スモールは圏のサイズの分類なので、サイトに対してもその意味を変えずに使っています。ビッグ/リトルは、サイズとは全然別な話で、圏の対象Xを特定したときの“Xのサイト”の作り方の違いです。

これらの概念の違いをハッキリさせるために、単なるサイトとインデックス付きサイトを区別して説明します。

内容:

サイト

サイト〈site〉とは、被覆系を備えた圏のことです。圏C上の被覆系〈coverage〉についての詳細はnLabを見てください。だいたいの雰囲気はここで説明します。

適当な添字集合 I に対する、Cの射のインデックス族 {fi:Ui→U | i∈I} を考えます。これは、Uを余ボディ〈cobody〉とする多重余スパン〈multi-cospan | 複余スパン〉です。あるいは、離散圏とみた I からの関手 i \mapsto Ui を余底面とする余錐です。Uは余錐の余頂点です。

無闇といっぱいある上記のごときインデックス族のなかで、被覆〈covering {family}? | cover〉と呼ばれるインデックス族が特定されているとします。被覆に対しては、Uを(共通の)ターゲット〈target〉と呼ぶようです -- 余ボディ、余頂点、台対象とかでも良さそうですけど。各 Ui→ U in C は被覆の成分〈component〉と呼びましょう。行列の成分、自然変換の成分と同じ用法です。

Cの対象Xに対して、Xをターゲットとする被覆の全体を Cov(X) とします。Cの対象に対する割り当て X \mapsto Cov(X) が満たすべき性質(公理)は、nLab項目を見てください。Cが引き戻し〈pullback〉で閉じていれば簡単な記述になります。が、多様体の圏Manは引き戻しで閉じてません。

被覆系はグロタンディーク位相の一般化です。ただし、単なる圏/単なる被覆系だと一般的過ぎるので、圏と被覆系に条件を付けて使うことが多いです。

サイトSを次のように書きます。

  • S = (CS, CovS)

CSは圏で、CovSはその上の被覆系です。

例によって記号の乱用で、

とも書きます。

(C, Cov), (D, Cov) が2つのサイトとして、関手 F:CD が被覆系に対して整合性〈協調性〉を持つなら、サイトの準同型、あるいはサイト射〈site morphism〉になります。そして、サイトとサイト射からなる圏Siteを形成します*1

C = (C, Cov) がサイトのとき、反変関手 F:CopD が層である条件を記述できます。別な言い方をすると、サイトとは層の定義域〈始圏〉となれる圏です。

インデックス付きサイト

インデックス付きサイトの定義の前に、まずは典型例を挙げます。Top位相空間の圏とします。X∈|Top| に対して、Open(X) をXの開集合の集合とします。部分集合の包含関係を射とみなして Open(X) は圏になります。f:U→V in Open(X) とは、U⊆V のことです。Open(X) の射の族 {fi:Ui→U | i∈} が被覆だとは、普通の意味で被覆になっていることだとします。以上の定義で、各Xごとに Opne(X) はサイトになります。

φ:X→Y in Top連続写像だとすると、φから、Open(Y)→Open(X) という逆向きの写像が誘導されます。この写像を Open(φ) または(略記として) φ* と書きます。φ* は圏としての構造も被覆系の構造も保存する(被覆を被覆に送る)ので、サイト射になります。

一般に、圏Cからサイトの圏Siteへの反変関手 S:CSiteインデックス付きサイト〈indexed site〉と呼びます。Open:TopSite はインデックス付きサイトの例です。

Topへの忘却関手Uを持つ圏Cでは、UとOpenを結合してインデックス付きサイトを構成できます。例えば、U:ManTop を忘却関手として、M \mapsto Open(U(M)) はMan上のインデックス付きサイトになります。

C上のインデックス付きサイト S = S[-] (別に意味はないが、習慣に従い角括弧)があるとき、|C| でインデックス付けられたD値の層の族 FX:S[X]opDインデックス付きD-層〈indexed D-sheaf〉と呼びます。インデックス付きD-層に、これ以上の条件はありません。

サイズ

サイト S = (C, Cov) があるとき、台の圏Cのサイズによって、サイトのサイズも分類します。

  • Cが小さい〈{スモール | small}である〉とき、サイトSは小さい。
  • Cが大きい〈{ラージ | large}である〉とき、サイトSは大きい。
  • Cがやせている〈{シン | thin}である〉とき、サイトSはやせている。
  • Cが太っている〈{ファット | fat}である〉とき、サイトSは太っている。

「太っている」は「やせている」の否定なので、少なくともひとつのホムセットは二元以上を持ちます。

インデックス付きサイト S:CSite に関しては:

  • すべてのS[X]が小さいとき、インデックス付きサイトS[-]は小さい。
  • 少なくともひとつのS[X]が大きいとき、インデックス付きサイトS[-]は大きい〈小さくはない〉。
  • すべてのS[X]がやせているとき、インデックス付きサイトS[-]はやせている。
  • 少なくともひとつのS[X]が太っているとき、インデックス付きサイトS[-]は太っている〈やせてはいない〉。

層に関するサイズ形容詞は、層の定義域〈始圏〉のサイズをそのまま使います。サイトC上の層 F:CopD に関して:

  • Cが小さいとき、層Fは小さい
  • Cが大きいとき、層Fは大きい
  • Cがやせているとき、層Fはやせている。
  • Cが太っているとき、層Fは太っている。

インデックス付き層 FX:S[X]→D に関して:

  • すべてのS[X]が小さいとき、インデックス付き層F(-)は小さい。
  • 少なくともひとつのS[X]が大きいとき、インデックス付き層F(-)は大きい〈小さくはない〉。
  • すべてのS[X]がやせているとき、インデックス付き層F(-)はやせている。
  • 少なくともひとつのS[X]が太っているとき、インデックス付き層F(-)は太っている〈やせてはいない〉。

ビッグサイトとリトルサイト

Cがサイトのとき、対象A上のオーバー圏 C/A に自然に入るサイト構造(被覆系)をビッグサイト〈big site〉と呼びます(nLab項目参照)。

この意味の「ビッグ」はサイズとは関係ないので、小さいサイト〈スモールサイト〉Cに対してビッグサイト C/A を作ることもできます。なんか奇妙ですが、行きがかり上しょうがないですね。

ビッグサイトは、理論上は単純な形をしてますが、実際の計算に使うには便利ではありません。そこで、計算の手間が少ないリトルサイト〈little site〉を定義したくなります。しかし、一般的・抽象的にリトルサイトを定義するのはけっこう難しそうです(nLab項目参照)。

具体的なインデックス付きサイトとして、開集合(の集合)で定義されるインデックス付きサイトがリトルサイトであることは認めていいでしょう。サイズ的にも、小さくやせたインデックス付きサイトになります。このタイプのサイト(インデックス付きサイト)を開集合リトルサイト〈open-set little site〉と呼ぶことにします。

多様体の圏Manを考えましょう。大きなサイトであるMan上には、C(-) や Ω(-) のような大きな層〈large sheaf〉があります。オーバー圏 Man/Mビッグサイト構造を入れ、その上のビッグ層(インデックス付き層)を考えることができます。それとは別に、開集合リトルサイト Open(-) を定義でき、リトル層(インデックス付き層)も構成できます。

Man上の層は、通常は開集合リトルサイト(インデックス付きサイト)上のリトル層(インデックス付き層)として定義されます。しかし、大きな層〈ラージ層〉とビッグ層(インデックス付き層)も一緒に考えたほうが見通しが良くなりそうです。つまり、次の三種類の層をその相互関係を考慮すべきかと。

  1. 大きなサイトMan上の大きな層
  2. 大きなサイトManから誘導されるビッグサイト上のビッグ層(インデックス付き層)
  3. 開集合リトルサイト上のリトル層(インデックス付き層)

大きなサイト/層とビッグなサイト/層を積極的に使うことをモットーにした微分幾何ビッグサイト微分幾何です。モットー以上の内容は現状たいしてありませんが(苦笑)。

*1:実を言うと、Siteの作り方を僕はよく分かってないのですが、頑張れば作れるでしょう。

バンドルと層の記法 まとめ

一覧にまとめておきます。随時、修正・追加があるでしょう。\newcommand{\hyph}{\mbox{-}}
\newcommand{\ul}[1]{ \underline{#1} }

内容:

  • Man -- (なめらかな)多様体の圏

バンドルの圏:

  1. C-Bdl[-] -- Man上の、ファイバーがCの構造を持つバンドルの、インデックス付き圏
  2. Bdl = Man-Bdl[-] -- Man上の{ファイバー}?バンドルのインデックス付き圏
  3. Vect-Bdl[-] -- Man上のベクトルバンドルのインデックス付き圏
  4. Alg-Bdl[-] -- Man上の代数〈多元環〉バンドルのインデックス付き圏
  5. Grp-Bdl[-] -- Man上の群バンドルのインデックス付き圏
  6. G-Prin-Bdl[-] -- Man上のG-主バンドルのインデックス付き圏
  7. X-Triv-C-Bdl[-] -- Man上の、ファイバーがXである自明バンドルのインデックス付き圏(各圏は単対象)

層の圏:

  1. C-Sh[-] -- Man上の、値がCである層の、インデックス付き圏
  2. Sh[-] = Set-Sh[-] -- Man上の{集合}?層のインデックス付き圏
  3. CRng-Sh[-] -- Man上の可換環層のインデックス付き圏
  4. Mod-Sh[-] -- Man上の加群層のインデックス付き圏
  5. Alg-Sh[-] -- Man上の代数〈多元環〉層のインデックス付き圏
  6. Grp-Sh[-] -- Man上の群層のインデックス付き圏

平坦化した圏:

関手

接関手:

  • T : ManVectBundle

ラージサイトとしてのMan上の層:

  1. SA = {\mathscr A} = C = Ω0 : ManopCRng -- 構造{可換環}?層
  2. Ω = Ω1 : ManopMod -- {1次の}?微分形式加群
  3. Ω : ManopAlg -- 微分形式代数層(掛け算は微分形式の外積
バンドルとバンドル射

バンドル:

  • 正式: E = (Etot, N, πE)
  • 乱用: πE:E→N または π:E→N
  • 略式: E over N

バンドル射:

  • 正式: f = (ftot, fbase) : E→F
  • 乱用: f = (f, φ) :E→F または f = (f:E→F, φ:N→M)
  • 略式: (f over φ) :E→F または f:E→F over φ:N→M
バンドルの演算

添字のNは、底空間多様体

演算名 演算記号 被演算項 演算結果
ファイバー積  \underset{N}{\times} バンドル バンドル
直和〈ホイットニー和〉  \underset{N}{\oplus} ベクトルバンドル ベクトルバンドル
テンソル  \underset{N}{\otimes} ベクトルバンドル ベクトルバンドル
双対  (\hyph)^{\underset{N}{\ast}} ベクトルバンドル ベクトルバンドル
外積〈ウェッジ積〉  \underset{N}{\wedge} ベクトルバンドル ベクトルバンドル
内部ホム  hom_N(\hyph, \hyph) \:\mbox{or}\: lin_N(\hyph, \hyph) ベクトルバンドル ベクトルバンドル
内部双線形射集合  bilin_N(\hyph, \hyph) ベクトルバンドル バンドル
内部エンド  end_N(\hyph) ベクトルバンドル 代数バンドル
内部アイソ  iso_N(\hyph, \hyph) ベクトルバンドル バンドル
内部オート  aut_N(\hyph) \:\mbox{or}\: gl_N(\hyph) ベクトルバンドル 群バンドル
k次外積空間  \Lambda^k_N(\hyph) ベクトルバンドル ベクトルバンドル
k次テンソル空間  tens^k_N(\hyph) ベクトルバンドル ベクトルバンドル
外積代数  \Lambda_N(\hyph) ベクトルバンドル 代数バンドル
テンソル代数  tens_N(\hyph) ベクトルバンドル 代数バンドル
フレーム  frame_N(\hyph) ベクトルバンドル バンドル
バンドルの移動
  • For F over M, φ:N→M,
    φ#F over N -- 引き戻されたバンドル
  • For E over N, φ:N→M invertible,
    φ#E = (φ-1)#E over M -- 前送りされたバンドル
セクション
  • s:N→E section
  • t:N→F section over φ:N→M
セクション空間と層
  • Γ(E) または ΓN(E)
  • ΓN(F/φ)
  • ΓN(U, E) := Γ(E|U)
  • ΓN(-, E) on N -- N上の層
層の演算

原則として、

  1. 中置演算子記号は、バンドルと同じ記号を使う。
  2. 演算の名前は、バンドルと同じ綴に下線を引く。(書体を変えるのは手書きでは辛いので。)
  3. 表にはないが、外部ホムは、語先頭文字を大文字にする。例: \ul{Iso}_A(\hyph, \hyph)

例外は、外積空間/外積代数

添字のAは、加群層の係数可換環層。

演算名 演算記号 被演算項 演算結果
直積  \times 集合層 集合層
直和  \underset{A}{\oplus} 加群 加群
テンソル  \underset{A}{\otimes} 加群 加群
双対  (\hyph)^{\underset{A}{\ast}} 加群 加群
外積  \underset{A}{\wedge} 加群 加群
内部ホム  \ul{hom}_A(\hyph, \hyph) \:\mbox{or}\: \ul{lin}_A(\hyph, \hyph) 加群 加群
内部双線形射集合  \ul{bilin}_A(\hyph, \hyph) 加群 集合層
内部エンド  \ul{end}_A(\hyph) 加群 代数層
内部アイソ  \ul{iso}_A(\hyph, \hyph) 加群 集合層
内部オート  \ul{aut}_A(\hyph) \:\mbox{or}\: \ul{gl}_A(\hyph) 加群 群層
k次外積加群  \Omega^k_A(\hyph) 加群 加群
k次テンソル加群  \ul{tens}^k_A(\hyph) 加群 加群
外積代数  \Omega^{\bullet}_A(\hyph) 加群 代数層
テンソル代数  \ul{tens}_A(\hyph) 加群 代数層
フレーム  \ul{frame}_A(\hyph) 加群 集合層
層の移動
  • For B on M, φ:N→M,
    φ-|B on N -- 引き戻された層
  • For A on N, φ:N→M,
    φ|-A on M -- 前送りされた層

融通無碍か曖昧模糊か

この記事で使う概念・記法は「ベクトルバンドル射の逆写像: 記法の整理をかねて」にあります。ただし、ベクトルバンドルFのxによる引き戻しは x#F にします。

気付いた、というか、あらためて「そうなんだな」と思ったこと; 次の4種類のモノが区別されないことが多いよね。

  1. f : E→F over x:|E|→|F| ベクトルバンドルのあいだの射(準同型写像
  2. f* : Γ(E)→Γ(F/x) セクション空間のあいだの写像
  3. f : Γ(E)→Γ(x#F) セクション空間のあいだの写像、バンドルを引き戻して
  4. f ∈ Γ(hom(E, x#F)) 内部ホムバンドルのセクション

f : E→F を基準にして、適当に飾り記号を付けて区別したけど、同じ記号の使い回し(オーバーロード)で区別しない/できない、あるいは逆に、まったくの別物として扱って関連性が見えないことも。

これらのモノのあいだに1:1対応があるのは事実ですが、同じモノではないので、同一視してしまうと色々と混乱が生じます。関連を付けないのもマズイです。

慣れていれば、1:1対応を積極的に利用して、異なる世界を縦横無尽に行き来しながら議論ができるでしょう。融通無碍/変幻自在の境地とでも申しましょうか。

しかし、慣れてない人には曖昧模糊/五里霧中。

はい、四字熟語、たくさん使ってみました。

ビッグサイト微分幾何と自然変換の上付き添字

ビッグサイト」と言えば東京ビッグサイト

*1

ではなくて、次のnLab項目を参照してください。

nLab項目は一般的な設定で説明していますが、特定状況下で具体的なビッグサイトを利用する話をします。利用目的は微分幾何のためです。

Manをなめらかな多様体の圏とします。Manのなかで話をするので、以下、形容詞「なめらかな」は省略します。Manのなかでなにかすることを、大ざっぱに微分幾何〈differential geometry〉と呼ぶことにします。

j:N→M in Man開埋め込み〈open embedding〉だとは、次のことだとします。

  1. jの像 j(N)⊆M は、Mの開集合になっていて、Nとj(N)は(jにより)位相的に同型である。
  2. 任意の p∈N に対して、接写像のファイバー Tpj:TpN→Tj(p)M は線形同型写像である。

一番の条件を満たしても、二番を満たすとは限りません。例えば、N = {x∈R | -1 < x < 1}, M = R を二つの多様体とみなして、j(x) = x3 とすると、一番の条件を満たしますが、x = 0 で二番の条件を満たしません。

開埋め込みの全体はManの部分圏になるので、それを OEMan とします。M∈|Man| に対して、オーバー圏 OEMan/M を(nLabの定義と少し違いますが)Mのビッグサイト〈big site〉と呼びます。一方、Mの開集合の全体に包含順序を考え、それを圏とみなしたもの Open(M) を、Mのスモールサイト〈small site〉リトルサイト〈little site〉と呼びます*2

ビッグサイトもリトルサイトも圏です。「サイト」と呼ばれるのは、被覆に関する構造を持つからですが、そこは割愛します。

リトルサイトをビッグサイトに標準的に埋め込むことができます。ビッグサイトに同値関係を入れてリトルサイトを再現することもできます。したがって、リトルサイトとビッグサイトは大差ないことになります。しかし、ビッグサイトのほうが話が簡単になることがあるので「ビッグサイトを積極的に使おう」というスローガンのもとの微分幾何ビッグサイト微分幾何〈big-site differential geometry〉です。

ビッグサイト微分幾何を試みるにあたって、些細な、しかし気になる問題があります。説明します。

F:ManopC を、Man上の反変関手とします。Fから、OEMan/MopC が自然に誘導されます。誘導された関手を FM:OEMan/MopC とします。具体例を挙げると、M  \mapsto C(M) は ManopCRng という可換環の圏への反変関手なので、CM:OEMan/MopCRng が誘導されます。

F, G:ManopC はふたつの反変関手、α::F⇒G は自然変換とします。誘導されたふたつの反変関手 FM, GM:OEMan/MopC のあいだに、誘導された自然変換も存在します。誘導された自然変換を αM::FM→GM と書くのが自然でしょう。

しかし、αM という書き方は普通 αM:F(M)→G(M) という成分の意味で使います。困った。成分の書き方のほうを変えます。自然変換αのM成分は、αM:F(M)→G(M) にします。

すると、

  • For j∈|OEMan/Mop|,
    FMj:FM(j)→GM(j) in C

と書けます。記号の乱用で、j:N→M in OEMan/Mop を単にNと書けば、

  • FMN:FM(N)→GM(N) in C

です。

具体例を挙げると; M \mapsto Ω(M) を(1次の)微分形式の空間を対応させる反変関手とします。C(M) と Ω(M) を一旦R-ベクトル空間とみなすと、外微分作用素 d は、

  • d:C⇒Ω:ManopR-Vect

特定の多様体Mと、特定の開埋め込みNに関する外微分作用素 d の成分は:

  • dMN:CM(N)→ΩM(N) in R-Vect

これは、記号の乱用を含むので、正確には次の可換図式になります(自然変換の成分は上付き添字!)。

\require{AMScd}
\begin{CD}
C^{\infty}(N)        @>{d^N}>>  \Omega({N}) \\
@A{C^{\infty}(j)}AA             @AA{\Omega(j)}A \\
C^{\infty}(M)        @>{d^M}>>  \Omega(M)
\end{CD}

ここで、C(j), Ω(j) は層の制限写像になっています。この可換図式は、外微分作用素が制限写像と整合することを意味します。

言いたかったことは:

  1. リトルサイトの代わりにビッグサイトを使いたい。
  2. 自然変換の成分添字を上付き添字に変更したい。

*1:https://www.cruisebe.com/tokyo-big-sight-japan の案内写真

*2:[追記]https://ncatlab.org/nlab/show/little+site を見ると、スモールサイトよりリトルサイトのほうが良さそうです。「リトル vs ビッグ」「スモール vs ラージ」という対比ですね。[/追記]

偏微分記号の逆数形式: 瓢箪から駒

昨日、行きがかり上 \frac{\partial x}{\partial} という記号を導入しました。偏微分の記号 \frac{\partial }{\partial x} の分母と分子をひっくり返したものです。

誰かこの記号を見たことありますか? (見たことある方は教えてくださいませ。)

\frac{\partial x}{\partial}\frac{\partial }{\partial x} の“逆”なのですが、偏微分作用素としての逆ではありません線形代数的な逆です。

数・関数・行列などの掛け算記号を省略せずに、一律にドットで書きます(これ、重要!)。Haskellのセクション記法を借りて、左からaを掛ける写像を (a・)、右からaを掛ける写像を (・a) と書きます(これも重要)。偏微分作用素を含んだ行列の計算を次のように決めます。


\frac{\partial} {\partial x} =
\begin{bmatrix}
 \frac{\partial} {\partial x^1} &
 \frac{\partial} {\partial x^2} &
 \cdots &
 \frac{\partial} {\partial x^n}
 \end{bmatrix}
\:\\
v =
 \begin{bmatrix}
 v^1 \\
 v^2 \\
 : \\
 : \\
 v^n
 \end{bmatrix} \\

として、掛け算は:


\:\:\:\: \frac{\partial} {\partial x}\cdot v\\
= \begin{bmatrix}
 \frac{\partial} {\partial x^1} &
 \frac{\partial} {\partial x^2} &
 \cdots &
 \frac{\partial} {\partial x^n}
 \end{bmatrix}
\cdot
 \begin{bmatrix}
 v^1 \\
 v^2 \\
 : \\
 : \\
 v^n
 \end{bmatrix} \\
=  \frac{\partial} {\partial x^1}\cdot v^1 +
\frac{\partial} {\partial x^2}\cdot v^2 + \cdots +
\frac{\partial} {\partial x^n}\cdot v^n

クドイですが、ドットは掛け算です。偏微分作用素としての作用ではありません。通常は、誤解を避けるために左から関数を掛け算します(掛け算記号なし)。しかしそうすると、お馴染みの行列計算のルールと整合しません。

この計算は多様体上の座標近傍(座標写像 x の定義域)U上でも意味を持ちます。掛け算する写像 (\frac{\partial}{\partial x}\cdot) は、次のようなベクトルバンドル写像を定義します。

  • RnU→TM|U over U

ここで、RnU はファイバーがRn(要素は縦一列の行列だと思う)であるU上の自明ベクトルバンドル、TM|UはMの接ベクトルバンドルのUへの制限です。底空間U上で考えているので over U と書いてます。

この写像はファイバーごとに可逆、全体としても可逆なので、逆写像を持ちます。それを (\frac{\partial x}{\partial}\cdot) と書くと約束します。

  • (\frac{\partial x}{\partial}\cdot) : TM|URnU over U

バンドル写像 (\frac{\partial x}{\partial}\cdot) は、セクション空間の写像を誘導するので、同じ記号で表します(オーバーロード)。

  • (\frac{\partial x}{\partial}\cdot) : Γ(TM|U)→Γ(RnU) over U

これだけのことです。

まだ一日しか使ってませんが、 \frac{\partial x}{\partial} って、メチャクチャ便利なんじゃないのかな。例えば、xからyへの局所座標の取り替えに伴う接ベクトル場Vの成分表示の変換公式は次のように書けます。([追記]等式を修正して別な形を「あるいは」の後に追加。[/追記]


\:\:\: \frac{\partial y}{\partial}\cdot V =
(\partial t)_x \cdot
(\frac{\partial x}{\partial}\cdot  V) \\
\mbox{where} \\
\:\:\: t = y\circ x^{-1}

あるいは、


\:\:\: \frac{\partial y}{\partial}\cdot V =
\frac{\partial y}{\partial x} \cdot
(\frac{\partial x}{\partial}\cdot  V)

これ、すごく自然で簡潔です。ええんちゃう(似非関西弁)。

あらためてシミジミと感じたことは:

  • 演算子記号を無闇と省略するのは良くない*1非常に良くない。
  • 演算子記号を省略すると、次のような演算が区別できなくなる。
    1. 微分作用素としての作用
    2. 様々な掛け算〈乗法〉
    3. 写像に関する適用と結合〈合成〉

因習に囚われずに、適度な演算子記号/関数記号をちゃんと入れれば、分かりやすさはだいぶ改善されます。

[追記 date="翌日"]
だいぶ分かった。ちょっと考えて、  \frac{\partial x}{\partial } = dx かと思ったのですが、そうではないですね。 \frac{\partial x}{\partial} は、 dx とも  \frac{\partial}{\partial x} とも違うナニモノカです。

 \frac{\partial}{\partial x}微分作用素 dx微分形式」ということをすっかり忘れて、純粋に線形代数の文脈で考えると、

  •  (\frac{\partial}{\partial x})^{-1} = dx^\ast

が成立します。ここで、右肩マナナスイチは逆線形写像、右肩アスタリスクは双対線形写像です。この等式の解釈には微妙なところ(コベクトルとフォームを同一視するか区別するか)がありますが、肝心なのは、線形代数だけで考えることです。

記号の約束として、

  •  \frac{\partial x}{\partial} := (\frac{\partial}{\partial x})^{-1}

ユークリッド空間では、線形写像としての \partial が意味を持つので、

  •  \frac{1}{\partial} := \partial^{-1}

部分可逆な t:Rn⊇→Rn に関して次の等式も成立します。あくまで、線形代数のなかでの等式です。

  •  \frac{\partial t}{\partial} = \partial t \cdot \frac{1}{\partial} = \partial t \cdot \partial^{-1}

ここで、\partial t はtのヤコビ行列で、ナカグロ〈センタードット〉は、反図式順で書いた“線形写像(または行列)の結合(または掛け算)記号”です。

さらにシミジミと感じたことは:

  • 微積分の議論と線形代数的な議論をゴチャゴチャにしないで、必要なら分離して議論する。

[/追記]

*1:[追記]関手と自然変換の計算に出てくる演算子記号とか // 酷い話」で、関手の縦結合も横結合も演算子記号を省略して並置で書く、という例を紹介しました。当然に、解釈も計算もできなくなります。「二項演算を並置で書く」が許されるのは演算ひとつまでです! 一緒に使う二つ以上の演算に対して「並置で書く」ルールを適用するのは極悪ですが、実際に存在するのが腹立たしい。[/追記]

なんだこれ? 奇妙な微分公式

取り急ぎのメモ。この記事で使う概念・記法は「ベクトルバンドル射の逆写像: 記法の整理をかねて」、「微分幾何におけるヤコビ行列の書き方: 因習の擁護」あたりに書いてあります。

すべては「なめらかな世界」で考えます。NとMは多様体で f:N→M は写像とします。x:N⊇U→Rn, y:M⊇V→Rm は局所座標、f(U)⊆V だとします。どうでもいいけど、多様体の名前 N, M と次元 n, m が一致するようにしました(気持ちいい)。

微分幾何におけるヤコビ行列の書き方: 因習の擁護 // 多様体間の写像のヤコビ行列」で述べたことから、1≦ i ≦n, 1≦ j ≦m に関して  \frac{\partial (y^j\circ f)}{\partial x^i} は、U上の関数として意味を持ちます。これらn×m個の関数達を行列の形に組んで、それを  \frac{\partial (y \circ f)}{\partial x} と書きましょう。つまり、

  •  (\frac{\partial (y \circ f)}{\partial x})^j_i =  \frac{\partial (y^j\circ f)}{\partial x^i}

 \frac{\partial (y \circ f)}{\partial x} は、U上で定義された行列値関数〈行列場〉、または関数係数〈関数成分〉の行列です。用語の乱用で単に「行列」とも呼びます。

さて、 \frac{\partial (y \circ f)}{\partial x} という行列は次のよう書けます*1


\:\:\: \frac{\partial (y \circ f)}{\partial x} = \frac{\partial y}{\partial}(f) \cdot \frac{\partial f}{\partial x}

 \frac{\partial y}{\partial} は書き間違いではありません。これの意味は  \frac{\partial} {\partial y} の“逆”です。これが表題の奇妙な微分公式

この微分公式が奇妙に見えるのは、記号の決め方がテキトーだからかも知れません。書き方・見え方は置いといて、意味を説明します。

 \frac{\partial f}{\partial x} は、 \frac{\partial f}{\partial x^i} 達を横に並べた一行行列〈関数の横タプル〉です。その成分の定義は:

  •  \frac{\partial f}{\partial x^i} := (\partial_i( f \circ x^{-1} ))\circ x

 \frac{\partial f}{\partial x} の一点 p∈U⊆M での値は、hom(Rn, Tf(p)TM) (内部ホム・ベクトル空間)に入ります。v∈Rnに対する値は次のように計算されます。

  •  \frac{\partial f}{\partial x}(p)\cdot v = \sum_{i=1}^n \frac{\partial f}{\partial x^i}(p)\cdot v^i \:\in T_{f(p)}M

ドットは、関数/関数値の掛け算です。微分作用と区別するために掛け算記号は書くことにします。行列の掛け算記号も省略せずにドットを使います。

 \frac{\partial f}{\partial x} は、ベクトルバンドル hom(RnN, f#TM) のU上のセクションだとみなせます。

  •  \frac{\partial f}{\partial x} \in \Gamma_N(U, hom({{\bf R}^n}_N, f^{\#}TM))

ここで、RnN はファイバーがRnの自明なベクトルバンドル、f#TM は接ベクトルバンドルの引き戻しです。

 \frac{\partial y} {\partial} は、 \frac{\partial} {\partial y} の“逆”と言いましたが、 \frac{\partial} {\partial y} =
\begin{bmatrix}
 \frac{\partial} {\partial y^1} &
 \frac{\partial} {\partial y^2} &
 \cdots &
 \frac{\partial} {\partial y^m}
 \end{bmatrix}
を次のように解釈します。

  •  \frac{\partial} {\partial y} \in \Gamma_M(V, iso({{\bf R}^m}_M, TM))

 \frac{\partial} {\partial y} は(局所的な)フレームの場ですが、それは内部アイソバンドルのセクションと思えます。このセクションは、点ごとに逆を取れます。それを  \frac{\partial y}{\partial} と書きました(奇妙だけどツジツマはあっていると思う)。

 \frac{\partial y}{\partial}(f) は、U上に引き戻したモノで、U上のセクションになります。

  •  \frac{\partial y}{\partial}(f) \in \Gamma_N(U, f^{\#}(iso(TM, {{\bf R}^m}_M)))

バンドルを少し大きく取り直して、次のように思ってもかまいません。

  •  \frac{\partial y}{\partial}(f) \in \Gamma_N(U, hom(f^{\#}TM, {{\bf R}^m}_N))

以上の設定で、行列の掛け算が意味を持つようになり、くだんの奇妙な微分公式が確認できます*2(勘違いでなければ)。

*1:[追記] \frac{\partial y}{\partial}(f) は、fによる引き戻しを意味します。が、この書き方を他でも使うと誤解される危険があるので、 (\frac{\partial y}{\partial})_f が良いかと思っています。[/追記]

*2:[追記]たまたま使ってみた偏微分記号の逆数形式は、予想以上に「使えるヤツ」みたいです。「偏微分記号の逆数形式: 瓢箪から駒」参照。[/追記]

一点での接ベクトルをハッキリさせよう: 三種類の定義

多様体の一点での接ベクトルを定義する方法が幾つかあります。微分作用素としての定義は以前述べました。その他の方法二種類も記しておきます。

内容:

三種類の接ベクトルの定義

この記事に出てくる多様体写像は、すべてなめらかだとします(いちいち「なめらかな」と書きません)。Mはn次元の多様体で、p∈M とします。

点pにおける接ベクトルの定義として、主に、次の三種類が使われます。

  1. 座標依存方式
  2. 曲線方式
  3. 微分作用素方式

好みと目的により使い分けるので、三種類のあいだに優劣はありません。僕の好みは微分作用素方式なので、それについては「微分ライプニッツ法則に支配されている」シリーズで述べています。

微分作用素方式の接ベクトルの定義を要約すれば、

  • TpM := Der(CGerm(M, p)/R, R)

です。記号の意味は:

  1. TpM は、点pにおける接ベクトル空間
  2. Der(A/K, B) は、可換環K上の相対可換環 A/K と B/K があるときの、AからBへのK-導分の全体からなる A/K-加群
  3. CGerm(M, p) は、多様体M上の点pにおける関数ジャームのR-相対可換環
  4. R = R/R は、Rを自明にR-相対可換環と考えたもの

この定義には代数的準備が要るので、とっつきにくく回りくどい印象は否めません。

残り二つの方式を要約すると、

  • TpM := (Rn×CentChart(M, p))/~JE (座標依存方式)
  • TpM := CentCurve(M, p)/~VE (曲線方式)

です。記号の意味は:

  1. CentChart(M, p) は、多様体Mの点pを中心とする中心付きチャート〈centered chart〉(後述)の集合
  2. JE は、集合 (Rn×CentChart(M, p)) 上の同値関係で、ヤコビ行列同値〈Jacobian equivalence〉(後述)
  3. CentCurve(M, p) は、多様体Mの点pを通る中心付き曲線〈centered curve〉(後述)の集合
  4. VE は、集合 CentCurve(M, p) 上の同値関係で、速度同値〈velocity equivalence〉(後述)

座標依存方式

多様体のチャートについては「古典的微分幾何・ベクトル解析のモダン化: 局所座標って何だ?」を参照してください。「チャート」と「局所座標」は同義語です。Mのチャート x は、MからRn への部分写像 x:M⊇→Rn だとします。ただし、xの定義域〈domain of definition〉はMの開集合で、像への制限(「微分幾何におけるヤコビ行列の書き方: 因習の擁護 // 用語と記法の準備:略記がたくさん」参照)x|im(x) が可逆(微分同相)です。次の略記を許します。

  • x-1 := (x|im(x))-1 (略記)

チャート x の定義域であるMの開集合を ddef(x) と書きます。M⊇ddef(x) \cong im(x)⊆Rn微分同相)です。

以上の設定で、三つ組 (v, p, x) ∈Rn×M×Chart(M) を考えます。三つ組 (v, p, x) が次の条件を満たすとき、座標依存方式における「点pにおける接ベクトル」だとします。

  1. p∈ddef(x)
  2. x(p) = 0 (0∈Rn

この条件を満たす三つ組 (v, p, x) を、v@p/x (v at p by x)と書くことにします。

v@p/x の定義をわずかに簡略にするために、中心付きチャートを導入しましょう。中心付きチャート〈centered chart〉とは、(p, x)∈M×Chart(M) で次の条件を満たすものです。

  1. p∈ddef(x)
  2. x(p) = 0 (0∈Rn

pをxの中心〈center〉と呼びます。pを中心とする中心付きチャートの全体を CentChart(M, p) とします。すると、

  • v@p/x = (v, (p, x)) ∈Rn×CentChart(M, p)

とみなせます。

x, y∈Chart(M) に対して、y\circx-1 は部分写像としての逆(すぐ上で略記として定義)と部分写像としての結合(結合できるところだけ結合)で定義します。すると:

  • y\circx-1:Rn⊇→Rn (部分写像として部分可逆)

特に、 x, y∈CentChart(M, p) ならば、y\circx-1 は原点の周りの開集合で定義されるので、ヤコビ行列〈導関数〉と“ヤコビ行列の原点での値”〈微分係数〉も定義されます。(ヤコビ行列のもう少し詳しいことは「微分幾何におけるヤコビ行列の書き方: 因習の擁護 // ヤコビ行列」参照。)

  • J(y\circx-1):Rn⊇→Mat(n, n) (Mat(n, n) はn次正方行列の集合)
  • J|0(y\circx-1) = (J(y\circx-1))(0) ∈Mat(n, n)

以上でヤコビ行列の定義ができたので、集合 Rn×CentChart(M, p) 上の同値関係 ~JE を定義します。v@p/x ~JE w@q/y とは次の条件を満たすことです。(JE は Jacobian equivalence から。)[追記]以下で、w = (J|0(y\circx-1))v と書いてあったところを w = (J|0(y\circx-1))v に修正しました。右肩の'◁'は、逆行列です。逆写像との混同を避けるために'◁'を使いました。[/追記][さらに追記]気の迷いでした。もとに戻しました。「反変ベクトル」とかいう言い方に惑わされて混乱・錯乱することが僕はあります。[/さらに追記]

  1. p = q
  2. w = (J|0(y\circx-1))v (並置は行列の掛け算、vは縦に書く)

JE が実際に同値関係であるためには、次が必要です。

  1. v@p/x ~JE v@p/x
  2. v@p/x ~JE w@q/y ならば、w@q/y ~JE v@p/x
  3. v@p/x ~JE w@q/y かつ w@q/y ~JE u@r/z ならば、v@p/x ~JE u@r/z

一番目は自明、二番目は逆関数微分公式から、二番目は合成関数〈関数の結合〉の微分公式から出ます。

先程、v@p/x を「点pにおける接ベクトル」だと言いましたが、正確には「点pにおける接ベクトルの代表元」で、ほんとの接ベクトルは、商集合 Rn×CentChart(M, p)/~JE の要素です。

伝統的な接ベクトルの定義で、「実数のタプルであって、座標変換に対してナンタラカンタラ」というスタイルのがありますが、これは、JE(ヤコビ行列同値)の同値類を接ベクトルと呼ぼう、と言っているわけです。

曲線方式

実数の開区間から多様体Mへの写像曲線〈curve | path〉と呼びます。実数変数を時間変数とみると、(質点の)運動〈motion〉と呼んだほうが適切な気がします。(が、「曲線」を使います。)

曲線αの定義域が、正実数εを使って (-ε, ε) と書けるとき、αを中心付き曲線〈centered curve〉と呼ぶことにします。中心とは0(基準時刻)のことです。さらに、α(0) = p であるような中心付き曲線の全体を CentCurve(M, p) とします。

集合 CentCurve(M, p) 上の同値関係 ~VE を定義します。α ~VE β とは次の条件を満たすことです。(VE は velocity equivalence から。)

  • 適当な中心付きチャート x∈CentChart(M, p) があって、J|0(x\circα) = J|0(x\circβ)

ここで、x\circα, x\circβ は、もとの定義域より小さくなるかもしれませんが、時刻0(実数)の周りの開区間で定義されています。よって時刻0でのヤコビ行列は定義されます。ここでのヤコビ行列は縦の一列行列なのでRnの要素と同一視可能です。

この定義には「適当な中心付きチャート x」が含まれるので、xのとり方に依らずに α ~VE β かどうかが決まることを示す必要があります。

  • とある中心付きチャートxについて α ~VE β ならば、別な中心付きチャートyについても α ~VE β 。

同値関係を定義する(真偽を決定する)段階では中心付きチャートを使いますが、その選び方は何でもいいので、同値関係の定義自体は選んだチャートに依存しません。

さらに、~VE が実際に同値関係であるためには、次が必要です。

  1. α ~VE α
  2. α ~VE β ならば、β ~VE α
  3. α ~VE β かつ β ~VE γ ならば、α ~VE γ

適当な中心付きチャートを選んで計算すればよいので、~JE のときと同様に、ユークリッド空間の微分計算に帰着されます。

曲線方式の接ベクトルとは、一点pを通る曲線達の同値類となります。同値類を決める同値関係は「点pでの速度ベクトルが等しい」と定義されます。速度ベクトルとは接ベクトルなので循環しているように思えますが、「点pでの速度ベクトルが等しい」の定義をユークリッド空間に持ち込んでしまうので循環はしていません。

相互関係

今回、座標依存方式と曲線方式を説明し、微分作用素方式は過去の記事で説明したので、三種類の方式を紹介し終わりました。しかし、それぞれをバランバランに定義しただけで、相互関係は述べていません。

三種類の定義が同値であることはそれほど難しくはないでしょう。どの方式であっても、接ベクトルはチャートによって成分表示ができます。同じ成分表示どうしが互いに対応するような写像を作れば、((Rn×CentChart(M, p))/~JE) \cong (CentCurve(M, p)/~VE) \cong Der(CGerm(M, p)/R, R) を示せます。

参照した過去記事:

  1. 古典的微分幾何・ベクトル解析のモダン化: 局所座標って何だ?
  2. 微分はライプニッツ法則に支配されている 3/3: 領域導分と接ベクトル場
  3. 接ベクトル場の定義:補遺
  4. 微分幾何におけるヤコビ行列の書き方: 因習の擁護

モノイド閉圏: カリー化からニョロニョロまで

昨日の記事「ラムダ計算の自然性とお絵描き」で、ラムダ計算を行える〈do lambda calculus〉環境としてのモノイド閉圏を紹介しました。モノイド閉圏はカリー化を持ちます。カリー化に関わる素材と法則があれば、そこから指数随伴系〈テンソル・ホム随伴系〉を構成できます。

この記事では、カリー化から出発して、随伴系 -- つまりニョロニョロ等式を満たす2-圏的構造を構成してみます。

内容:

随伴系の指標

随伴系〈adjunction | adjoint system〉の指標を書いてみます。指標については「構造とその素材の書き表し方」を参照してください。

signature Adjunction in CAT {
  sort A
  sort B
  operation F:AB
  operation G:BA
  two-operation η::A^⇒F*G:AA
  two-operation ε::G*F⇒B^:BB

  equation snake-1::: (η*F^);(F^*ε) = F^ :: F⇒F:AB
  equation snake-2::: (G^*η);(ε*G^) = G^ :: G⇒G:BA
}

まず、1行目の 'in CAT' で、この指標を考える場所は(小さいとは限らない)圏の圏 CAT だと分かります。CATは2-圏なので、対象(sort)、射(operation)以外に2-射(two-operation)があります。そして、随伴系の法則として3-射である等式(equation)があります。コロンの個数が射の次元に一致しています(sort=0-射=対象=圏、operation=1-射=射=関手、two-operation=2-射=自然変換、equation=3-射=自然変換の等式)。後置のカレット記号('^')は、“恒等”を作る演算子として使っています。A^ は圏Aの恒等関手、F^ は関手Fの恒等自然変換など。使っている二項演算子記号については、「関手と自然変換の計算に出てくる演算子記号とか // 今後使う予定の演算子記号」を参照してください。

この指標に出てきた2つの等式(snake-1とsnake-2)がニョロニョロ等式〈snake {equation | relation | identity | law}〉です。"snake"を「ニョロニョロ」と訳しはじめた経緯は次の記事を参照。

随伴系のインスタンスΣがあるとして、「構造とその素材の書き表し方」の標準的記法を使えば次のように書けます。

  • Σ = (Σ.A, Σ.B, Σ.F, Σ.G, Σ.η, Σ.ε)

随伴に関する注意事項」に従って書けば:

  • Σ = (Ση, Σε : ΣF -| ΣG, ΣF:ΣAΣB)

ここで、インスタンスΣを示す修飾子は左肩に付けています。右の上下添字は他の目的に使う可能性があるからです。後で、この書き方に近い記法を使います。

指数随伴系

モノイド閉圏Cの特徴は、対象 A∈|C| ごとに指数随伴系〈テンソル・ホム随伴系〉が存在することです。対象Aに対する随伴系を Σ[A] と書きましょう。Σ[A]の構成素に付ける添字はAだけにします。つまり、次のように書きます。

  • Σ[A] = (Aη, Aε : AF -| AG, AF:AAAB)

さらに次の約束をします。

  1. AF は、無名ラムダ変数やHaskell風セクション記法を使って直接書く。AF = (-\otimesA) = (\otimesA)
  2. AG も同様。AG = [A, -]
  3. Aが何であっても AA = AB = C であり、Cは了解されているので省略する。

結局、対象Aに対する指数随伴系Σ[A]は、

  • Σ[A] = (Aη, Aε : (\otimesA) -| [A, -])

指数随伴系Σ[A]の存在を示すには、単位Aηと余単位Aεを定義して、それらがニョロニョロ等式を満たすことを示せばいいわけです。

が、いきなりニョロニョロ等式は難しいことがあるので、カリー化同型写像 ΛX,AY:C(X\otimesA, Y)→C(X, [A, Y]) からボトムアップで指数随伴系を組み上げることが多いでしょう。ここでもボトムアップ・アプローチを採用します。

カリー化と反カリー化の対称性

ラムダ計算では、カリー化〈ラムダ抽象〉、エバル〈evaluator〉*1、ベータ変換等式を主に扱います。反カリー化は積極的には扱いません。しかしここでは、カリー化と反カリー化を対等に対称的に扱います。カリー化Λの逆写像Λ-1、つまり反カリー化をΓと書くことにします。

カリー化/反カリー化に関わる概念(まだ説明してない)を表にまとめておきます。説明は後述します。\newcommand{\id}{\mbox{id}}

カリー化 反カリー化
写像 Λ 写像 Γ
エバル ev インス ins
ベータ変換等式 イータ変換等式
ラムダベント \overset{\lambda}{\cap} ガンマベント \underset{\gamma}{\cup}
余単位 ε 単位 η
テンソリング後結合 ホミング前結合
\epsilon = \Gamma(\id_{[A, X]})  \eta = \Lambda(\id_{X \otimes A})

Cの対象 X, A, Y の三つ組ごとに、カリー化/反カリー化のペアが与えられていて、次は成立していると仮定します。

  1. ΛX,AY : C(X\otimesA, Y)→C(X, [A, Y])
  2. ΓXA,Y : C(X, [A, Y])→C(X\otimesA, Y)
  3. ΛX,AYXA,Y = idC(X\otimesA, Y)
  4. ΓXA,YX,AY = idC(X, [A, Y])

\require{AMScd}
\begin{CD}
{\mathcal C}(X \otimes A, Y) @>{\Lambda^{X, A}_Y}>> {\mathcal C}(X, [A, Y]) \\
@|                                                  @| \\
{\mathcal C}(X \otimes A, Y) @<{\Gamma^X_{A, Y}}<< {\mathcal C}(X, [A, Y]) \\
\end{CD}

二変数射と高階射

昨日述べたように、カリー化の典型事例は「二変数関数から一変数高階関数」への変換、反カリー化の典型事例は「一変数高階関数から二変数関数」への変換です。

一般的な議論でも、この典型事例の“雰囲気”を醸し出すために、「二変数射」「高階射」という言葉を使いましょう*2二変数射〈two-variable morphism | morphism of two variables〉とは、適当な対象 X, A, Y に対する X\otimesA→Y というプロファイル(域と余域)を持つ射です。そして高階射〈higher-order morphism〉は、X→[A, Y] という、余域が指数〈内部ホム〉であるプロファイルを持つ射です。

Iをモノイド圏のモノイド単位対象とすれば、どんな射 f:X→Y でも、X\otimesI→Y とみなすことができるので、二変数射だと言えます。また、X→[I, Y] という高階射とみなしてもかまいません。なので、二変数射/高階射という分類は絶対的な意味はないのですが、比喩としての心理的な効果はあり、説明には便利な言葉です。

ここから後の説明では、高階射(とみなしたい射)は、F, G などの大文字で表すことにします。例えば、カリー化Λの結果は高階射なので、G = Λ(f) のように書きます。ΓはΛの逆なので、Γ(G) = f ですね。

エバルとベータ変換等式

ラムダ計算を支配している法則は、ベータ変換等式だと言っていいでしょう。ベータ変換等式には次のモノが登場します。

  1. カリー化 Λ = ΛX,AY:C(X\otimesA, Y)→C(X, [A, Y])
  2. エバル ev = AevX : [A, X]\otimesA→X in C

エバル(evaluatorの略称)と呼ばれる特別な射によって、カリー化の逆が作れることを主張するのがベータ変換等式です。公理的な定義では、ベータ変換等式を満たすような特別な射をエバルと呼び、その存在を公理的に要請します。よって、エバルとベータ変換等式は一緒に導入されます。

次の等式がベータ変換等式〈equation of beta reduction〉で、そこに登場する射 AevXエバ〈eval | evaluator〉です。 \newcommand{\For}{\mbox{For}\:\:}\newcommand{\cat}[1]{{\mathcal {#1}}}

  • \For f : X\otimes A \to Y \:\mbox{in}\: \cat{C},\\ (\Lambda^{X,A}_Y(f)\otimes \id_A);{^A ev_X} = f

添字を省略して簡略に書けば:

  • (Λ(f)\otimesA^);ev = f (A^ はAの恒等射)

ベータ変換等式を絵で描けば次のようになります。描画の約束は「ラムダ計算の自然性とお絵描き」を参照してください

絵のなかで、小文字'λ'でマークされた部分をラムダベント〈lambda bent〉またはラムダカーブ〈lambda curve〉と呼びましょう。ワイヤー〈ストリング〉をラムダベントの形に曲げることがカリー化の実行になります。

'ε'でマークされたお団子〈ノード〉がエバルです。後で、ev = ε と別名を付けます。絵からの比喩的表現を使えば、ワイヤーAを思いっきり引っ張って真っすぐにすること〈ストレッチング〉がベータ変換です。引っ張ることにより、εが消滅し、ラムダベントは伸びます。

ベータ変換等式は、次のように解釈できます。

  •  G \mapsto (G \otimes \id_A);ev という対応は、カリー化Λの逆写像となる。

カリー化の逆写像は反カリー化Γなので、

  •  \Gamma(G) = (G \otimes \id_A);ev

という、Γの具体的な表示が得られます。Γは、idAによる右テンソリング(モノイド積の意味の掛け算)して、evを後結合〈post-composition〉してます。

  • 反カリー化Γは、テンソリングと後結合で作れる。

逆に反カリー化ありきなら、エバルは反カリー化から作れます。

  •  ev = \Gamma(\id_{[A, X]})

エバルありきから反カリー化を作っても、反カリー化ありきからエバルを作ってもかまいません。いずれにしても、ベータ変換等式が構造と状況を統制しています。

インスとイータ変換等式

カリー化ではなく反カリー化をベースにして、前節と並行的に、インスとイータ変換等式を説明します。文面は、前節のコピーを修正したものです。

イータ変換等式には次のモノが登場します。

  1. 反カリー化 Γ = ΓXA,Y:C(X, [A, Y])→C(X\otimesA, Y)
  2. インス ins = AinsX : X→[A, X\otimesA] in C

インス(inserterの略称)と呼ばれる特別な射によって、反カリー化の逆が作れることを主張するのがイータ変換等式です。公理的な定義では、イータ変換等式を満たすような特別な射をインスと呼び、その存在を公理的に要請します。よって、インスとイータ変換等式は一緒に導入されます。

次の等式がイータ変換等式〈equation of eta reduction〉で、そこに登場する射 AinsXインス〈ins | inserter〉です。

  • \For G : X \to [A, Y] \:\mbox{in}\: \cat{C},\\ {^A ins_X};[\id_A, \Gamma^{X}_{A,Y}(G)] = G

添字を省略して簡略に書けば:

  • ins:[A^, Γ(G)] = G (A^ はAの恒等射)

イータ変換等式を絵で描けば次のようになります。

絵のなかで、小文字'γ'でマークされた部分をガンマベント〈gamma bent〉またはガンマカーブ〈lambda curve〉と呼びましょう。ワイヤー〈ストリング〉をガンマベントの形に曲げることが反カリー化の実行になります。

'η'でマークされたお団子〈ノード〉がインスです。後で、ins = η と別名を付けます。絵からの比喩的表現を使えば、ワイヤーAを思いっきり引っ張って真っすぐにすること〈ストレッチング〉がイータ変換です。引っ張ることにより、ηが消滅し、ガンマベントは伸びます。

イータ変換等式は、次のように解釈できます。

  •  f \mapsto ins;[\id_A, f] という対応は、反カリー化Γの逆写像となる。

反カリー化の逆写像はカリー化Λなので、

  •  \Lambda(f) = ins;[\id_A, f]

という、Λの具体的な表示が得られます。Λは、idAによる左ホミング(内部ホムの意味の累乗)して、insを前結合〈pret-composition〉してます。

  • カリー化Λは、ホミングと前結合で作れる。

逆にカリー化ありきなら、インスはカリー化から作れます。

  •  ins = \Lambda(\id_{X \otimes A})

インスありきからカリー化を作っても、カリー化ありきからインスを作ってもかまいません。いずれにしても、イータ変換等式が構造と状況を統制しています。

随伴系の単位と余単位

前々節と前節において、「エバルとベータ変換等式」と「インスとイータ変換等式」を並行的に扱いました。二種の概念群に対称性(あるいは双対性)があることが分かるでしょう。しかし、ラムダ計算では、「インスとイータ変換等式」はあまり注目しません。言及する場合でも、関数の外延性として紹介されます。そのときは、イータ変換の絵も次のように描かれます。

この暗い写真は2009年に僕が説明しているホワイトボードです。ちなみに、ベータ変換の説明は:

ちょうど10年前ですね(どうでもいけど)。

[補足]
カリー化=ラムダ抽象はインスで表現可能で、反カリー化=ラムダ反抽象はエバルで表現可能です。絵で考えれば、カリー化=ラムダベンディング操作がインス=ηノードのホミング前結合で表現され、反カリー化=ガンマベンディング操作がエバル=εノードのテンソリング後結合で表現されることになります。この状況は次の絵等式で覚えておくと便利です。



[/補足]

さて、今回エバルとインスを並行的/対称的に扱ったのは、随伴系にスムーズに結びつけるためです。次の事実があるのです。

  • エバルは指数随伴系の余単位である。
  • インスは指数随伴系の単位である。

随伴系における記法と合わせるために、次のように別名定義します。

  • Aε = Aev
  • Aη = Ains

Aε, Aη は自然変換となり、次のプロファイルを持ちます。

  • Aε:: [A, -]\otimesA⇒C^:CC
  • Aη:: C^⇒[A, -\otimesA]:CC

対象Xでの成分を取れば:

  • AεX: [A, X]\otimesA→X in C
  • AηX: X→[A, X\otimesA] in C

Aε, Aη が実際に自然変換になることは別途証明が必要ですが割愛します。

エバル(ev = ε)とインス(ins = η)、ベータ変換等式とイータ変換等式、それら全てを使うことによって指数随伴系が構成できます。

ニョロニョロ等式

カリー化 Λ(f) を f と書くと、絵と似ていて便利です。上付き'∩'がラムダベントを表します。 \Lambda(f) = f^{\overset{\lambda}{\cap}} とかすると象形文字としての精度は上がりますが、そこまではしません。

ベータ変換等式は次のように書けます。

  • (f\otimesA^);ε = f

前節の補足説明のように、ラムダベントをηノードのホミング前結合で置き換えていいので、

  • ((η;[A^, f])\otimesA^);ε = f

結合とモノイド積に関する交代律〈interchange law〉を使うと:

  • ((η\otimesA^);([A^, f]\otimesA^);ε = f

このなかの f:X\otimesA→Y を特別に f = idX\otimesA:X\otimesA→X\otimesA (Y = X\otimesA)と置いても等式は成立します。実は、この等式が、指数随伴系のニョロニョロ等式になっています。そのことを絵で説明しましょう。

随伴系のニョロニョロ等式(の片一方)は (η*F^);(F^*ε) = F^ であり。指数随伴系では、F = (\otimesA), G = [A, -] でした。よって示すべき等式は、

  • η*(\otimesA)^;(\otimesA)^*ε = (\otimesA)^

です。絵に描けば:

対象Xでの成分を取ると:

  • X.(η*(\otimesA)^;(\otimesA)^*ε) = X.(\otimesA)^

右辺の X.(\otimesA)^ は、idX\otimesA を意味します。

右辺に注目して絵に描いてみます。

横に三段に分けて、各段のテキスト表現は:

  1. ηX;A^
  2. [A^, f]\otimesA^
  3. εX\otimesY = εY

です。これを縦方向に結合すると、

  • ηX;A^ ; [A^, f]\otimesA^ ; εY
    = (η;A^);([A^, f]\otimesA^);ε

ところが、これは先の等式から f になります。f = idX\otimesA だったので、ニョロニョロ等式が成立することが確認できました。

もうひとつのニョロニョロ等式に関しても同様にできます。

おわりに

この記事では、カリー化と反カリー化の対称性を強調しましたが、実際にはどちらか一方で十分です。例えば次の状況があったとします。

  1. Cはモノイド圏であり、二項関手 [-, -]:Cop×CC が備わっている。
  2. Cの対象 X, A, Y ごとに写像 ΛX, AY:C(X\otimesA, [A, X]) が定義されている。
  3. Cの対象 X, A ごとに特別な射 AevX:[A, X]\otimesA→X が特定さている。
  4. Λとevに関して、ベータ変換等式 (Λ(f)\otimesA^);ev = f が成立している。

ベータ変換等式から、Λの可逆性が保証され、Λ-1 := Γ, ins = Λ(idX\otimesA) と定義すれば、反カリー化/インス/イータ変換等式の議論が展開できます。

ベータ変換等式/イータ変換等式があれば、それからニョロニョロ等式は導けるので、指数随伴系が構成可能です。別な言い方をすれば、カリー化/エバル/ベータ変換等式があれば、必然的に指数随伴系(の族)は存在します。

対象Aごとの指数随伴系達がテンデンバラバラではなくて、全体として体系的に連合していることを保証するには、カリー化の自然性を確認します。

以上のセッティングが揃えば、圏C上で型付きラムダ計算を行うことができます。

*1:"eval"だから「エヴァル」がいいという話があるかも知れませんが、長年「エバル」と言ってきたのでかえって違和感あります。そもそも僕は"b"と"v"をカタカナ表記で区別する必要性を感じません。「ベクトル」でいいし、「ベトナム」でいいよ。

*2:「使いましょう」と言いながら、この記事では使っていません。が、便利な言葉だとは思うので記述を残しておきます。

ラムダ計算の自然性とお絵描き

タイトルの「自然性」は、国語辞書的な意味ではなくて、圏論の意味での自然性です。何が自然なのかというと、ラムダ計算の中核であるカリー化が自然だということです。なので、正確に言えば:

  • ラムダ計算の中核であるカリー化は、圏論的な意味で自然である。

このことを、お絵描き(ストリング図による描画)を混じえて説明します。

内容:

モノイド閉圏

ラムダ計算のセマンティクス〈モデル〉は、通常はデカルト閉圏〈Cartesian closed category〉により与えられます。しかし、もう少し一般化してモノイド閉圏〈monoidal closed category | 閉モノイド圏 | closed monoidal category〉でもラムダ計算の解釈はできます。

モノイド閉圏は、モノイド構造と整合した閉構造を持つモノイド圏です。モノイド積を持たない閉圏〈closed category〉という概念もあり、含意しか持たない論理のセマンティクスに使われたりします。ラムダ計算もモノイド積無しの閉圏で解釈するテがありますが(ときに望ましいかも)、モノイド積がないとだいぶ扱いにくく苦労するので、(型付きの)ラムダ計算の話ではモノイド積を使ってもいいと思います

モノイド閉圏には、モノイド積以外に指数〈exponential〉とか内部ホム〈internal hom〉と呼ばれる演算が要求されます。指数/内部ホムは、YA, hom(A, Y), [A, Y] などと書かれます。デカルト閉圏のときは「指数」、一般的な文脈では「内部ホム」と呼ぶ習慣のようですが、こういう区別に拘ってもしょうもないので同義語扱い「指数=内部ホム」でいいでしょう。指数/内部ホムに関しては:

モノイド積と指数を絵に描くときは、次のようにします。

圏の対象がワイヤー〈ストリング〉で、ワイヤーの並置(単に横に並べる)はモノイド積で、ワイヤーのあいだに斜め線を引くと指数です。指数の右のワイヤーは逆向き(下から上)に走ると考えると都合がいいです。

なお、ここでの描画方向は、射の結合方向が上から下、モノイド積の方向が左から右です。旗で示せば

カリー化と反カリー化

モノイド閉圏Cには、モノイド積と指数が備わっているのでした。これらの演算は、二項関手〈双関手〉になります。

  • モノイド積二項関手 (-\otimes-):C×CC
  • 指数二項関手 [-, -]:Cop×CC

モノイド積は共変-共変の二項関手、指数は反変-共変の二項関手です。ただし、どっちの変数が反変になるかは書き方に依存します*1。例えば、指数形式 XA を中置演算子記号で X^A と書くと約束すると、

  • (-^-):C×CopC

です。この記事では、XA = [A, X] とAを左に書くので、第一変数〈左変数〉に関して反変です。

Cがモノイド閉圏であるためには、次の条件が必要です。

  • 任意の対象 A∈|C| が定義する関手 (-\otimesA) と [A, -] は随伴ペアになる。

随伴を正確に記述するために、随伴系を「随伴に関する注意事項」に従って書くとすれば、次の随伴系〈adjunction | adjoint system〉があります。

  • (η, ε: (-\otimesA) -| [A, -], (-\otimesA):CC)

この随伴系を、指数随伴系〈exponential adjunction〉とかテンソル・ホム随伴系tensor-hom adjunction〉と呼びます。「テンソル・ホム」の由来は; テンソル積はモノイド積と同義に使われることがあり、ホムは内部ホム、つまり指数です。「テンソル・ホム」は「モノイド積と指数のあいだの」という形容詞です。

Cの対象 X, Y を選んで、指数随伴系が導くホムセット間同型を書けば:

  • C(X\otimesA, Y) \cong C(X, [A, Y])

この同型を与える左から右方向の写像カリー化〈currying〉と呼び、Λで書くことにします。

  • Λ:C(X\otimesA, Y)→C(X, [A, Y])

随伴系の定義より、Λには逆写像が存在します。Λ-1反カリー化〈uncurrying〉と呼びます*2

カリー化写像Λは、構文的なラムダ抽象操作に対応します。反カリー化写像Λ-1に対応する構文的な操作はラムダ反抽象とでも言えばいいのでしょうか?(呼び名は知らない)

通常の(デカルト閉圏における)ラムダ計算では、カリー化(=ラムダ抽象)は、「多変数関数の変数を減らして高階関数にする」ことだと説明されます。キャッチフレーズとしては、「カリー化は高階関数化」だと言っていいでしょう。となると、反カリー化(=ラムダ反抽象)は低階関数化だと言えるでしょう。「低階関数化」って聞いたことないけど。

  • カリー化は、多変数関数の変数を減らして、より高階な関数にする。(高階関数
  • 反カリー化は、高階関数の変数を増やして、より低階な関数にする。(低階関数化

ツジツマはあってるよね。

[補足]
fのカリー化 Λ(f) を f, f などの上付きオペレーター記号で書くことがあります。Λ, λ, ^, ∧, ∩ は形状が似ているので連想が働きます。それとは別な上付きオペレーターで、♭, # を使う流儀があります。音楽記法〈music notation〉と呼ばれ、互いに逆(または互いに双対)なオペレーターをフラットとシャープで表します。

カリー化/反カリー化でも音楽記法を使うことがあります。すぐ上の説明のごとく、カリー化が高階化なので半音上げ(高くする)でシャープを使って欲しいですね。しかし残念ながら、Λ(f) = f と書くのが習慣です。ナンダヨ、モー。
[/補足]

カリー化に関するタイトニング/スライディング

一般的な随伴系を (η, ε : F -| G, F:CD) とすると、そのカリー化(転置)同型写像は次のようになります。

  • ψXY : D(F(X), Y)→C(X, G(Y))

ホムセット間同型写像は、対象 X∈C, Y∈D ごとに決まるので ψXY と書きました。添字 X, Y を上下に振り分けたのは後の記法と合わせるためです。

随伴系の条件として、ホムセット間同型の族が存在するだけでなくて、「X, Y に関して自然である」という条件が付きます。この条件は分かりにくいし、明示的な解説も少ないです。「圏論の随伴をちゃんと抑えよう: お絵描き完全解説 // 転置と反転置の自然性」でかなり詳しく書いているので興味があれば参照してください。

ここでは、指数随伴系〈テンソル・ホム随伴系〉に関しての自然性を扱います。指数随伴系のカリー化同型写像を添字付きで書くと:

  • ΛX,AY : C(X\otimesA, Y)→C(X, [A, Y])

ΛX,AY には3つの添字(X, A, Y)がありますが、これら3つの添字(対象変数)に関する自然性が要求されます。これから、その自然性を等式と絵で表すことにします。

以下で出てくる対象と射は次です。縦に書いているのは絵に合わせてです。

\require{AMScd}
\begin{CD}
X'      @.   A' \\
@V{v}VV      @VV{p}V \\
X       @.   A \\
@.           @. \\
X \otimes A \\
@V{f}VV \\
Y \\
@.           @. \\
Y \\
@V{q}VV \\
Y' \
\end{CD}

自然性は次の3つの等式で表現できます。

タイトニング

 \Lambda^{X',A}_Y( (v\otimes id_A);f) =  v;\Lambda^{X,A}_Y(f)

絵だと、曲がったワイヤーの部分(ベント)を短く締め込んでいるいるのでタイトニング〈tightening〉と呼びます。もともとは、タイトニング/スライディングはトレースの自然性を表す言葉です(「トレース付き対称モノイド圏とはこんなモノ」参照)。

簡略なラムダ式で表すなら:

  • λa.f(v(x'), a) = (λa.f(x, a))[v(x')/x]

ここで、[v(x')/x] は、変数xにv(x')を代入するオペレーターです。

カーブに沿ったスライディング

 \Lambda^{X,A'}_Y( (id_X\otimes p);f ) =  \Lambda^{X,A}_Y(f);[p, Y]

絵だと、ノードpを曲がったワイヤーに沿って滑らしているのでカーブに沿ったスライディング〈curved sliding〉と呼びます。移動後のpは指数の内部に入ります。

簡略なラムダ式で表すなら:

  • λa'.f(x, p(a')) = Yp(w)[λa.f(x, a)/w]

ここで、Yp は [p, Y] と同じで、指数関手〈内部ホム関手〉に p, idY を渡した結果です。

真っすぐなスライディング

 \Lambda^{X,A}_{Y'}( f;q ) =  \Lambda^{X,A}_Y(f);[A, q ]

絵だと、ノードqを真っすぐに下に滑らしているので真っすぐなスライディング〈straight sliding〉と呼びます。移動後のqは指数の内部に入ります。

簡略なラムダ式で表すなら:

  • λa.q(f(x, a)) = qA(w)[λa.f(x, a)/w]

自然性をまとめてみると

タイトニング、カーブに沿ったスライディング、真っすぐなスライディングの3つの操作をまとめると次のようになります。

 \Lambda^{X',A'}_{Y'}( (v\otimes p);f;q ) =  v;\Lambda^{X,A}_Y(f);[p, q]

さらにまとまりを付けるために、Φv,pq と Φv[p, q] を次のように定義します。


\Phi^{v,p}_{q}:{\mathcal C}(X \otimes A, Y) \to {\mathcal C}(X' \otimes A', Y') \\
\Phi^{v,p}_{q}(f) := (v \otimes p);f;q \\
\:  \\
\Phi^{v}_{[p, q]}:{\mathcal C}(X, [A, Y]) \to {\mathcal C}(X', [A', Y']) \\
\Phi^{v}_{[p, q]}(g) := v;g;[p, q] \\

これらを使うと、カリー化の自然性は次のように書けます。

 \Lambda^{X', A'}_{Y'}(\Psi^{v,p}_{q}(f)) = \Psi^{v}_{[p, q]}(\Lambda^{A,X}_{Y}(f))

可換図式ならば:


\begin{CD}
{\mathcal C}(X'\otimes A', Y')  @>{\Lambda^{X', A'}_{Y'}}>> {\mathcal C}(X', [A', Y']) \\
@A{\Psi^{v,p}_{q}}AA                                        @AA{\Psi^{v}_{[p, q]}}A \\
{\mathcal C}(X\otimes A, Y)     @>{\Lambda^{A,X}_{Y}}>>     {\mathcal C}(X, [A, Y]) \\
\end{CD}

*1:左指数と右指数を区別して扱えばスッキリするのですが、対称モノイド圏では、左右を区別なしでやることが多いです。左右を区別しないほうが簡便ですが、代わりに多少の曖昧さと混乱が生じます。

*2:随伴系の一般論では、カリー化/反カリー化を転置/反転置とも呼びます。「圏論の随伴をちゃんと抑えよう // 転置と反転置」参照。

形容詞「ドブ板」

昔は平気だったことでも、今では非難の対象になることは多々あります。時代が変われば、価値観・判断基準も変わるのでしょうがないですね。

昔僕は、「これといった戦略もなく、気の利いた道具もなく、ただ力まかせに頑張る」ことを「ドカタサギョウ」と呼んでいました。「ドカタ」は、今ではポリティカルに正しくない、一種の差別語として扱われるようです。

手間を惜しまず頑張るしかない状況は実際にあるわけですが、なんて表現すればいいのでしょう?

「力押し」という言葉がありますが、あれは、潤沢な物理的パワーを持っている場合にそれを使って云々、という感じがするので「ただひたすら愚直に頑張る」感じがしないですね。

ドブ板選挙、ドブ板営業などに使われる「ドブ板」は、「これといった戦略もなく、気の利いた道具もなく、ただ力まかせに頑張る」の意味を含んでいるように思えます。「スマートではない/時代遅れな」といった否定的・侮蔑的なニュアンスで使われることもあるようですが、今のところ、「ドブ板」は差別語ではないでしょう。

単一の形容詞にしなくても別にいいのですが、「ドカ…」と口に出てしまったとき、直後に言いなおす一単語が欲しかったのです。「ド…」からの修正ならそのまま「ド…ブイタ」とできます。