ヤコビ微分圏：下部構造としての芯付きラムダ圏 - 檜山正幸のキマイラ飼育記 (はてなBlog)

昨日の記事「快適な微分計算のための圏と微分公式」の最後の節でヤコビ微分圏に触れました。ヤコビ微分圏は、2年以上前（2017年春）に考えたけど、チョット書いただけでソレッキリでした。

ヤコビ微分圏：はじまり

2017年の記事の続き（ヤコビ微分圏第2回）を書きます。ヤコビ微分圏の下部構造である圏について述べます。

内容：

微分圏の下部構造
芯付きラムダ圏：動機と由来
デカルト構造と半加法構造
半加法芯付きデカルト圏の実例
芯付きラムダ構造
芯付きラムダ計算

関連する記事：

微分圏の下部構造

微分圏〈differential category〉または微分付き圏〈cateogry with differentiation〉とは、圏論的微分作用素である微分コンビネータ〈differential combinator〉を備えた圏です。微分コンビネータを載せる前の圏は、微分圏の下部構造と言えるでしょう。下部構造の圏も構造を持ちます。下部構造の圏の構造により、微分圏の性質も変わってきます。

現在、最もよく知られた微分圏はブルート／コケット／シーリー〈Richard Blute, Robin Cockett, Robert Seely〉によるデカルト微分圏〈Cartesian differential category〉でしょう（原典は下の論文）。

Title: Cartesian differential categories (2008 - 2009)
Authors: R.F. Blute, J.R.B. Cockett, R.A.G. Seely
Pages: 52p
URL: http://www.tac.mta.ca/tac/volumes/22/23/22-23abs.html

デカルト微分圏の下部構造は、デカルト左加法圏〈Cartesian left additive category〉です。

まず、左加法圏〈left additive category〉とは、次の性質を持つ圏です。

ホムセットが可換モノイド構造を持つ。
射のプレ結合〈pre-composition〉で足し算（可換モノイド演算）とゼロ（可換モノイドの単位元）が保存される。

射の結合を図式順、記号はセミコロンで書くと、左加法性は次の等式で表されます。

f;(g + h) = f;g + f;h
f;0 = 0

左加法圏は、可換モノイドで豊饒化されているわけではないので注意してください*1。

さて、問題のデカルト左加法圏〈Cartesian left additive〉は、デカルト圏であって左加法圏でもある圏です。

デカルト左加法圏は、我々にお馴染みの微分計算を行う舞台としてはあまり自然ではありません。例えば、X⊆Rⁿ, Y⊆R^m を2つの開集合とするとき、C^∞(X, Y) が足し算とゼロを持つとは限りません。

お馴染みの微分計算を微分圏として定式化するなら、デカルト左加法圏とは違った構造を持つ下部構造を採用すべきだと思うのです。

芯付きラムダ圏：動機と由来

微分計算を行う前に知っておいたほうがいい概念には何があるでしょうか？おそらく、次の事項でしょう。

線形代数
ラムダ計算
位相の初歩

位相の初歩とは、「ベクトル空間の位相と、ベクトル空間の開集合のあいだの連続写像」の知識のことです。

微分圏の下部構造としては、線形計算（線形代数の計算）とラムダ計算ができて、開集合と連続写像の概念を持つような圏が良いでしょう。ヤコビ微分圏は、そのような下部構造の上に、ヤコビアンに相当する微分コンビネータを載せたものです。

とりあえず、位相は抜きにして*2、線形計算とラムダ計算をミックスした計算ができる圏を考えましょう。そのような圏の名称として、「ヤコビ微分圏：はじまり// 準半加法圏など」では「準半加法圏〈qusi-semiadditive category〉」「閉準半加法圏〈closed qusi-semiadditive category〉」という奇妙な名前を提案しています -- 過去記事を読めば、名称に悩んでいる様子がうかがえるでしょう。

概念は変えませんが、命名の方針は変えることにします。我々が扱う圏は、デカルト圏Cと、Cの部分デカルト圏Aのペア (C, A) で、様々な構造を持つものです。部分圏Aが半加法圏のとき、CはAより弱い構造（単なるデカルト構造）しか持たないので、「準半加法圏」という呼び方をしたのですが、発想を逆にします。

ペア (C, A) のAを芯〈core〉と呼ぶことにして、(C, A) は、内部に芯Aを抱えたデカルト圏Cと考えます。よって (C, A) は芯付きデカルト圏〈cored Cartesian category〉です。芯は付加構造（例えば、半加法構造）を持つかも知れません。その付加構造に応じて、ナントカ芯付きデカルト圏（例えば、半加法芯付きデカルト圏）と呼ぶことにします。こうすると、芯の構造を取り替えても命名に困りません。

ヤコビ微分圏の下部構造では、ラムダ計算を可能とするメカニズムが必要とされます。そのようなメカニズム（構造）をラムダ構造〈lambda structure〉と呼ぶことにします（詳細は後述）。芯付きデカルト圏がラムダ構造を持つなら、芯付きラムダ圏〈cored lambda category〉と呼びましょう。デカルト閉圏Cは、自明な芯（C自身）を考えて、芯付きラムダ圏となります。

2017年時点からの名称の変更は次のようになります。

準半加法圏 → 半加法芯付きデカルト圏（より一般には、芯付きデカルト圏）
閉準半加法圏 → 半加法芯付きラムダ圏（より一般には、芯付きラムダ圏）

この記事で、半加法芯付きデカルト圏／半加法芯付きラムダ圏を順次段階的に定義していくことにします。必要に応じて、一般的な芯付きデカルト圏／芯付きラムダ圏にも触れます。

デカルト構造と半加法構造

圏Cは、モイド的に定義された〈monoidally defined〉デカルト圏〈Cartesian category〉であるとします。つまり、C = (C, ×, 1, λ, ρ, α, σ) と（記号の乱用で）書けます。各構成素の意味は：

× はモノイド積双関手 (×):C×C→C
1 はモノイド単位対象 1∈|C|
λ は左単位律子自然変換 λ::(1×-)⇒Id_C:C→C
ρ は右単位律子自然変換 ρ::(-×1)⇒Id_C:C→C
α は結合律子自然変換 α::((-×-)×-)⇒(-×(-×-)):(C×C)×C→C×(C×C)
σ は対称性自然変換 σ::(×)⇒Σ*(×):C×C→C

律子〈一貫性自然同型〉に関しては「律子からカタストロフへ」を参照、Σはフリップ（二項の入れ替え）関手で、'*'は関手の図式順結合記号です。これらの構成素達は対称モノイド圏の公理を満たし、モノイド積対象 A×B がAとBの（極限としての）直積を与えます。モノイド単位対象1は終対象になっています。

Cの部分圏Aは、Cのデカルト構造をそのまま受け継いで部分デカルト圏になります。それだけではなくて、Cの直積 × がAでは双積になるとします。つまり、× をAに制限すると直和〈余直積〉にもなります。

Aの直和を $\oplus$ と書くことにすると、それは × と一致するので、 $\oplus$ = × がほんとに（等式として）成立します。終対象1は、Aのなかでは始対象にもなっています。

1はAではゼロ対象（始対象でもあり終対象でもある対象）なので、0 = 1 と書きたくなりますが、0はCの始対象（もしあれば）のために取っておきます。＋もCの直和の記号に予約します。（が、当面は、Cの直和と始対象は考えません。）

記号	意味
×	CとAで共通の直積
$\oplus$	$\oplus$ = × 、Aでは直和でもある
1	Cの終対象、Aではゼロ対象
+	Cの直和（あれば）
0	Cの始対象（あれば）

この約束の欠点は、1 $\oplus$ A $\stackrel{\sim}{=}$ A のようになるので、1 + a = a との類似で不自然に感じることです。1を、ときにはゼロとみなしてください。

モノイド積としての双積を持つ圏が半加法圏〈semiadditive category〉でした。半加法圏については次の記事で述べています。

半加法圏（モノイド双積圏）では、余対角 ∇_A:A $\oplus$ A→A と、始対象（ゼロ対象）からの唯一射 θ_A:1→A が、A上の可換モノイド構造を定義します。対象の可換モノイド構造から、ホムセットの可換モノイド構造が誘導され、結果的に半加法圏は可換モノイドで豊饒化されます。

A上では、直積と直和が一致してますが、Cに直和が存在するとは限らず、存在しても双積になることは保証されないので、半加法構造＝双積構造による対称性・双対性は、Aにおいてだけ有効なものです。

以上に述べた、デカルト圏 C = (C, ×, 1, λ, ρ, α, σ) と部分デカルト圏である半加法圏 A = (A, $\oplus$ , 1, λ, ρ, α, σ) のペア (C, A) を、半加法芯付きデカルト圏〈semiadditive cored Cartesian category〉と呼びます。半加法構造を持つ部分デカルト圏Aは、(C, A) の半加法芯〈semiadditive core〉です。

半加法芯付きデカルト圏の実例

前節で抽象的に定義した半加法芯付きデカルト圏の実例を挙げます。

デカルト圏Cを、ノルムベクトル空間の開集合を対象として、そのあいだの連続写像を射とする圏とします。

X∈Obj(C) ⇔ (Xは、とあるノルムベクトル空間Vの開集合、X = V でも、X = 空集合でもよい)
f∈C(X, Y) ⇔ (fは、開集合Xから開集合Yへの連続写像)
射の結合は、連続写像の結合〈合成〉。
恒等射は、恒等写像。

通常の集合の直積を × とすると、X⊆V、Y⊆W の直積 X×Y は、ノルムベクトル空間 V×W の開集合になります（直積位相を考えて）。また、連続写像の直積は次のように定義できます。

For f:X→X', g:Y→Y', x∈X, y∈Y,
(f×g)(x, y) = (f(x), f(y)) ∈X'×Y'

1 = {0} を単位対象として、λ, ρ, α, σ も通常通りに定義すると、(C, ×, 1, λ, ρ, α, σ) は（具体的な）デカルト圏になります。

Cの部分デカルト圏Aは：

V∈Obj(C) ⇔ (Vは、ノルムベクトル空間)
f∈A(V, W) ⇔ (fは、連続線形写像)
射の結合は、連続線形写像の結合〈合成〉。
恒等射は、恒等写像。

デカルト構造はCからそのまま受け継げば、(A, ×, 1, λ, ρ, α, σ) はCの部分デカルト圏になります。直積は、ノルムベクトル空間の直和でもあるので、(A, ×, 1, λ, ρ, α, σ) は、× = $\oplus$ として半加法圏（モノイド双積圏）になります。

芯付きラムダ構造

芯付きデカルト圏 (C, A) 上でラムダ計算を可能とするために、芯付きラムダ構造を定義しましょう。この節では、芯Aに特別な追加構造（例えば半加法構造）を仮定しません。自明な芯による芯付きデカルト圏 (C, C) でもかまいません -- この場合は、デカルト圏C上のラムダ構造になります。

芯付きラムダ構造の定義では、非関手的／非自然な手法を使います。事前に、「ヤコビ微分圏：はじまり // ヤコビ微分圏の動機」の「下部構造が面白い。」「非関手的・非自然な手法が活躍する。」に目を通しておくとよいかも知れません。

芯付きラムダ構造は次の構成素からなります。

芯内部ホム〈core internal hom〉： Obj(A)×Obj(A)→Obj(A) という写像。(A, B) $\mapsto$ [A, B] と書く。
左評価射〈core left evaluation morphism〉： Obj(A)×Obj(A)→Mor(C) という写像。(A, B) $\mapsto$ (lev_A,B:A×[A, B]→B in C) と書く。
右評価射〈core right evaluation morphism〉： Obj(A)×Obj(A)→Mor(C) という写像。(A, B) $\mapsto$ (rev_A,B:[A, B]×A→B in C) と書く。

幾つかの注意事項を以下に：

芯内部ホムは、芯指数対象〈core exponential object〉とも呼びます。単に内部ホム／指数対象でもいいとしましょう。
評価〈evaluation〉と適用〈application〉は同義語なので、左適用射なども使われます。
左評価射と右評価射のどちらか一方だけで十分ですが、左右のバランスのために、両方とも入れています。
[A, B] を [A→B] または [B←A] とも書きます。左右の違いをハッキリさせるときは便利です。
今回は触れませんが、内部ホム〈指数〉と評価射の計算は絵算を使うのが楽ちんで間違いを避けられます。「非対称閉圏のカリー化：記号法を工夫すれば、右と左の混乱も解消」から参照されている記事を辿っていくと、デカルト閉圏における絵の描き方が分かるでしょう。

芯付きラムダ構造として与えられた内部ホムと左右の評価射を使って、次のような写像を定義します。' $\circ$ 'は、反図式順の射の結合記号です。

X∈|C|, A, B∈|A| に対して、
ℓΓ_X,A,B:C(X, [A→B])→C(A×X, B)
ℓΓ_X,A,B(f) = lev_A,B $\circ$ (id_A×f)
X∈|C|, A, B∈|A| に対して、
rΓ_X,A,B:C(X, [B←A])→C(X×A, B)
rΓ_X,A,B(f) = rev_A,B $\circ$ (f×id_A)

ℓΓ_X,A,Bを左反カリー化〈left uncurrying〉、rΓ_X,A,Bを右反カリー化〈right uncurrying〉と呼びます。

芯付きラムダ構造の条件（公理）として次があります。

[反カリー化の単射性] すべての X, A, B に対して、ℓΓ_X,A,B, rΓ_X,A,B は単射である。

さらに次の記号を導入します。

LC(A×X, B) = (左反カリー化 ℓΓ_X,A,B の像集合) ⊆ C(A×X, B)
RC(X×A, B) = (右反カリー化 rΓ_X,A,B の像集合) ⊆ C(X×A, B)

左右の反カリー化は単射だったので、次のような逆写像が存在します。

ℓΛ_X,A,B = (ℓΓ_X,A,B)^-1 : LC(A×X, B)→C(X, [A→B])
rΛ_X,A,B = (rΓ_X,A,B)^-1 : RC(X×A, B)→C(X, [B←A])

ℓΛ_X,A,Bを左カリー化〈left currying〉、rΛ_X,A,Bを右カリー化〈right currying〉と呼びます。

次の、集合のあいだの同型が成立します。

LC(A×X, B) $\stackrel{\sim}{=}$ C(X, [A→B])
RC(X×A, B) $\stackrel{\sim}{=}$ C(X, [B←A])

もうひとつの芯付きラムダ構造の条件（公理）は次です。

A(A×1, B) = LC(A×1, B)
A(1×A, B) = RC(1×A, B)

これは、同型ではなくてイコールです。すぐ上の同型と組み合わせると：

A(A×1, B) = LC(A×1, B) $\stackrel{\sim}{=}$ C(1, [A→B])
A(1×A, B) = RC(1×A, B) $\stackrel{\sim}{=}$ C(1, [B←A])

芯付きラムダ計算

前節で定義した芯付きラムダ構造を持つような芯付きデカルト圏、つまり芯付きラムダ圏では、ラムダ計算が可能となります。

通常のラムダ計算とさほど変わりませんが、注意すべき事は、カリー化が制限されることです。右カリー化 rΛ は、任意の C(X×Y, Z) に対して定義されているわけではなく、B, C∈|A| に対する C(X×B, C) にだけ、しかも右カリー化の定義域はホムセットの部分集合 RC(X×B, C) に制限されます。

記法を簡略にするため、f∈RC(X×B, C) の右カリー化 rΛ_X,B,C(f) を f^∩ と書きます（インデックス X, B, C の情報は落ちます）。また、右評価射 rev を中置演算子' $\cdot$ 'で書くことにします。この記法で、カリー化と反カリー化が互いに逆なことを書くと：