前層の圏における記法と計算 - 檜山正幸のキマイラ飼育記 (はてなBlog)

圏の記法はある程度整備されてますが、圏の圏や関手圏のなかの計算だと、これといった決まりごとはありません。決めておかないと不便なので、おおよその約束ごとをこの記事に書いておきます。関手圏、とくに前層の圏での計算を目的にします。

内容：

前層の圏
プロファイリングとin記法
ラムダ記法
等式とon記法
自然変換に関する等式

前層の圏

射、関手、自然変換に関する演算記号は、「関手と自然変換の計算に出てくる演算子記号とか // 今後使う予定の演算子記号」に従います。念のために再掲すると：

演算	反図式順演算子記号	図式順演算子記号
射の結合	$\circ$	;
関手の適用	丸括弧	.
関手の結合	・	*
自然変換の適用	下付き添字	.
自然変換の縦結合	$\circ$	;
関手と自然変換のヒゲ結合	・	*
自然変換の横結合	・	*

“小さな圏”の圏をCatとして、局所小〈locally small〉だが“全体としては大きいかも知れない圏”の圏をCATとします。“大きいかも知れない圏”の圏の定義は、実際には難しい（「圏のサイズとサイズによる“圏の圏”の分類」参照）のですが、深入りしないことにします。扱う圏はすべて局所小で、Cat⊆CAT, Set∈|CAT| と考えます。

圏C, Dに対する関手圏[C, D]は、CもDも小さいなら小さい圏となるので、二項（反変-共変）関手 [-, -]:Cat^op×Cat→Cat として意味を持ちます。しかし、CAT上では関手圏をうまく定義できません。局所小の条件が満たされないからです（例えば、[Set, Set]）。

Cが小さくて、D = Set のときは扱いやすいので、共変関手の関手圏[C, Set]と反変関手の関手圏[C^op, Set]は非常によく利用されます。それぞれ、余前層の圏〈category of copresheaves〉、前層の圏〈category of presheaves〉と呼ばれます。前層の圏のほうがよく出てくるので、ここでは前層の圏を扱います。

前層の圏[C^op, Set]の対象は、圏C上の前層〈presheaf on a category C〉と呼びます。C上の前層の圏をSet^{C^op}とも書きますが、上付きの入れ子になるので嬉しくない。短くPSh(C)とも書きます。手書きや印刷物ではさらに短く $\hat{\mathcal{C}}$ と書くことがあります。ここではC^♠と書くことにします。

C^♠ = $\hat{\mathcal{C}}$ = PSh(C) = Set^{C^op} = [C^op, Set]

ここでよく使う記法は、C^♠と[C^op, Set]です。Cが小さくないときは、C上の前層の圏は考えません。

プロファイリングとin記法

関手や自然変換を扱うとき、当該の関手／自然変換を“どこで”考えているかにより解釈と扱い方が変わってきます。例えば、Cを小さい圏として、関手 F:C→Set があるとき、これは「圏の圏CATの射」なのか、それとも前層の圏C^♠の対象なのか、それによって解釈と扱い方は変わります。

「“どこで”考えているか？」をハッキリさせることは、関手／自然変換のプロファイルを明確にすることです。プロファイルの明確化＝プロファイリング〈profiling〉*1とは、高次圏まで含めた圏論的実体〈categorical entity | categorical thing〉に対して、その次元と所属している区域（圏の一部分）を指定することです。プロファイルの書き方は、「圏論的宇宙と反転原理と次元付きの記法」に従います。

CATに関して、k-射の集合（0-射は対象）を挙げましょう。次元kは上付きで添えます。

|CAT|⁰ = Mor⁰(CAT) = Obj(CAT) = |CAT| = {すべての局所小な圏}
|CAT|¹ = Mor¹(CAT) = {すべての関手}
|CAT|² = Mor²(CAT) = {すべての自然変換}

つまり、次の同値が成立します。

Cは（局所小な）圏 ⇔ C∈|CAT|⁰
Fは関手 ⇔ F∈|CAT|¹
αは自然変換 ⇔ α∈|CAT|²

関手（1-射）と自然変換（2-射）には両端があるので、それも明示すると：

CAT¹(C, D) = Hom¹_CAT(C, D) = Functor(C, D) = {CからDへのすべての関手}
CAT²(F, G) = Hom²_CAT(F, G) = Nat(F, G) = {FからGへのすべての自然変換}

つまり、

FはCからDへの関手 ⇔ F∈CAT¹(C, D)
αはFからGへの自然変換 ⇔ α∈CAT²(F, G)

一般に、k-射zを z:^(k)x→^(k)y のように書きます。ここで、「:^(k)」は、セミコロンをk個並べた記号、「→^(k)」はk重の矢印です。k = 0 のときは、コロンも矢印もなくて、x, y もないものとします。

k = 0： z
k = 1： z:x→y
k = 2： z::x⇒y

今扱っているCATにおいては、

k = 0：圏 C
k = 1：関手 F:C→D
k = 2：自然変換 α::F⇒G

自然変換をより丁寧に表したいなら α::F⇒G:C→D のように書きます。F⇒G:C→D, F⇒G, C→D などが射のプロファイル〈profile〉でした。プロファイルにより、射の次元と所属する区域が確定します。プロファイルの詳細は「圏論的宇宙と反転原理と次元付きの記法」を見てください。

射の両端が分からない／興味がない／不要であるときは、F:?→?, α::?⇒? と書きます。コロンの個数／矢印の太さで次元が分かるので、次のようなin記法〈"in" notation〉が可能になります。

C in CAT ⇔ C∈|CAT|⁰
F:?→? in CAT ⇔ F∈|CAT|¹
F:C→D in CAT ⇔ F∈CAT¹(C, D)
α::?⇒? in CAT ⇔ α∈|CAT|²
α::F⇒G in CAT ⇔ α∈CAT²(F, G)

次元を、セミコロン個数と矢印太さで重複して表現しているので、セミコロンだけ書いて F:?, α::? でも問題ありませんが、矢印も書いておいたほうが落ち着く感じはします。

ラムダ記法

（インフォーマルな）ラムダ記法は、関手と自然変換の計算でも役立ちます。つうか、ラムダ記法なしでは辛い！ 必須と言っていいでしょう。

関手 F:C→D を表現するには、Fを対象部分〈object part〉と射部分〈morphism part〉に分けて、対象部分は F⁰:|C|→|D| という関数で、射部分はホムセットごとの関数の集まり F¹_X,Y:C(X, Y)→D(F⁰(X), F⁰(Y)) として書き下します。次の形ですね。

F⁰ := λX∈|C|.(F⁰(X) ∈|D|)
F¹_X,Y := λf∈C(X, Y).(F¹_X,Y(f) ∈D(F⁰(X), F⁰(Y)))

射部分の表示において、X, Yも変数なので、これもラムダ抽象すれば：

F¹ := λX, Y∈|C|.(λf∈C(X, Y).(F¹X,Y(f) ∈D(F⁰(X), F⁰(Y))))

同じ'λ'だと視認性が悪いので、大文字'Λ'にします。これは視認性だけの理由で、'λ'と'Λ'に本質的な違いはありません。

F¹ := ΛX, Y∈|C|.[λf∈C(X, Y).(F¹_X,Y(f) ∈D(F⁰(X), F⁰(Y)))]

ΛX, Y の部分は、総称関数における型パラメータなので、∀X, Y と全称記号を使う場合もありますが、'∀'は論理式にだけ使いたいので'Λ'にしました。

結局、関手を定義する形式は：

F:C→D :=
  λX∈|C|.(F⁰(X) ∈|D|)
  and
  ΛX, Y∈|C|.[λf∈C(X, Y).(F¹_X,Y(f) ∈D(F⁰(X), F⁰(Y)))]

これは、対象・射の対応手順を示しているだけなので、関手性〈functoriality〉の証明は別に必要です。上記のように定義された写像の集まりが、関手的〈functorial〉とは、圏の結合と恒等を保存することです；保存するという性質が関手性です。

自然変換 α::F⇒G:C→D は、|C|でインデックスされたDの射の族なので、関手より簡単に表現できます。αの表示は次にようになります。

α::F⇒G:C→D :=
  ΛX∈|C|.[α_X:F⁰(X)→G⁰(X) in D]

Dが一般の圏のときは、α_X:F⁰(X)→G⁰(X) in D をラムダ記法で表示できる保証はありませんが、D = Set のときはラムダ記法が使えます。

α_X:F(X)→G(X) in Set :=
  λx∈F(X).(α_X(x) ∈G(X))

組み合わせると：

α::F⇒G:C→Set :=
 ΛX∈|C|.[λx∈F(X).(α_X(x) ∈G(X)) : F(X)→G(X) in Set]

自然変換の表示も対応手順だけなので、自然性〈naturality〉の証明は別に必要です。上記のαの自然性を主張する等式的命題は次の形です。（'on set'は次節で説明します。）

∀f:A→B in C.
∀x∈F(A).
  α_B(F(f)(x)) = G(f)(α_A(x)) on set G(B)

等式とon記法

等式 x = y において、xとyが所属する集合を明示して、x =_A y のように書くことがあります。等号が集合でインデックスされます。インデックスがイヤなときは、x = y on A と書くことにします。さらにAが集合であることを強調したいときは、x = y on set A とします。

集合上の等式以外に、クラス上（on class）の等式と圏上（on cat）の等式を扱います。圏C上の等式はさらに、対象のあいだの等式と射のあいだの等式に分けます。

対象のあいだの等式： A = B on cat C
射のあいだの等式： f = g : A→B on cat C

それぞれ、クラス上の等式、集合上の等式に還元できます。

A = B on class |C|
f = g on set C(A, B)

Cが小さい圏のときは、対象のあいだの等式も集合上の等式に還元できます。

A = B on set |C|

2つの関手F, Gの等しさ、F = G を考えると、とりあえずは F = G on class |CAT|¹ ですが、F, Gの両端が等しいのは前提されるので

F = G : C→D on cat CAT

つまり、

F = G on class CAT¹(C, D)

前節の関手の表現を考慮すると、上記等式は次のように還元できます。

∀X∈|C|.
  F⁰(X) = G⁰(X) on class |D|

∀X, Y∈|C|.
  F¹_X,Y(f) = G¹_X,Y(f) on set D(F⁰(X), G⁰(Y))

D = Set のときは、

∀X∈|C|.
  ∀x.(x∈F⁰(X) ⇔ x∈G⁰(X))

∀X, Y∈|C|.
  ∀x∈F⁰(X).
     F¹_X,Y(f)(x) = G¹_X,Y(f)(x) on set G⁰(Y)

F = G を証明するとは、上記の2つの命題を証明することです。F, Gが前層（を表す関手）のときは、向きを逆転します。

今まで説明したような、等式を「“どこで”考えているか？」を'on'で明示する記法をon記法〈"on" notation〉と呼びます。

自然変換に関する等式

α, β:F→G in C^♠ に関して、等式 α = β を考えてみます。

α, β:F→G は、C上の前層の圏C^♠の2つの射です。これを、外側の環境CATで考えれば、

α, β::F⇒G:C^op→Set in CAT

したがって、等式は、

α = β on set CAT²(F, G)

（クラスではなく）集合上の等式であるのは、Cが小さいことからCAT²(F, G)も小さくなるからです。CAT²(F, G)より、Nat(F, G:C^op→Set)と書いたほうが事情がハッキリするので、そう書くことにして：

α = β on set Nat(F, G:C^op→Set)

自然変換の等しさは成分ごとに等しければいいので、次のように還元できます。

∀X∈|C^op|.
  α_X = β_X on set Set(F(X), G(X))

集合圏のホムセット上の等式、つまり写像のあいだの等式なので、値ごとの等しさに還元できます。

∀X∈|C^op|.
  ∀x∈F(X).
    α_X(x) = β_X(x) on set G(X)

証明のお膳立ての観点から言うと、α = β : F→G on cat C^♠ という命題が示すべきターゲット命題として与えられたとき、次のような変形（ターゲットの還元）が許されます。

  Γ |-? α = β : F→G on cat C^♠
 ----------------------------------[自然変換の等値性]
  Γ, X∈|C^op|, x∈F(X) |-?
      α_X(x) = β_X(x) on set G(X)

このような記法／計算を使う実例は、たぶんそのうち（割とすぐに）出します。

*1:プロファイリングは、型理論における型つけ〈typing〉を高次元まで拡張したものです。