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

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

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

参照用 記事

前層の圏における記法と計算

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

内容:

前層の圏

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

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

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

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

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

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

  • C =  \hat{\mathcal{C}} = PSh(C) = SetCop = [Cop, Set]

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

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

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

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

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

  1. |CAT|0 = Mor0(CAT) = Obj(CAT) = |CAT| = {すべての局所小な圏}
  2. |CAT|1 = Mor1(CAT) = {すべての関手}
  3. |CAT|2 = Mor2(CAT) = {すべての自然変換}

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

  1. Cは(局所小な)圏 ⇔ C∈|CAT|0
  2. Fは関手 ⇔ F∈|CAT|1
  3. αは自然変換 ⇔ α∈|CAT|2

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

  1. CAT1(C, D) = Hom1CAT(C, D) = Functor(C, D) = {CからDへのすべての関手}
  2. CAT2(F, G) = Hom2CAT(F, G) = Nat(F, G) = {FからGへのすべての自然変換}

つまり、

  1. FはCからDへの関手 ⇔ F∈CAT1(C, D)
  2. αはFからGへの自然変換 ⇔ α∈CAT2(F, G)

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

  1. k = 0: z
  2. k = 1: z:x→y
  3. k = 2: z::x⇒y

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

  1. k = 0: 圏 C
  2. k = 1: 関手 F:CD
  3. k = 2: 自然変換 α::F⇒G

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

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

  1. C in CATC∈|CAT|0
  2. F:?→? in CAT ⇔ F∈|CAT|1
  3. F:C→D in CAT ⇔ F∈CAT1(C, D)
  4. α::?⇒? in CAT ⇔ α∈|CAT|2
  5. α::F⇒G in CAT ⇔ α∈CAT2(F, G)

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

ラムダ記法

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

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

  • F0 := λX∈|C|.(F0(X) ∈|D|)
  • F1X,Y := λf∈C(X, Y).(F1X,Y(f) ∈D(F0(X), F0(Y)))

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

  • F1 := λX, Y∈|C|.(λf∈C(X, Y).(F1X,Y(f) ∈D(F0(X), F0(Y))))

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

  • F1 := ΛX, Y∈|C|.[λf∈C(X, Y).(F1X,Y(f) ∈D(F0(X), F0(Y)))]

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

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


F:CD :=
λX∈|C|.(F0(X) ∈|D|)
and
ΛX, Y∈|C|.[λf∈C(X, Y).(F1X,Y(f) ∈D(F0(X), F0(Y)))]

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

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


α::F⇒G:CD :=
ΛX∈|C|.[αX:F0(X)→G0(X) in D]

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


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

組み合わせると:


α::F⇒G:CSet :=
Λ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|1 ですが、F, Gの両端が等しいのは前提されるので

  • F = G : CD on cat CAT

つまり、

  • F = G on class CAT1(C, D)

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


∀X∈|C|.
F0(X) = G0(X) on class |D|

∀X, Y∈|C|.
F1X,Y(f) = G1X,Y(f) on set D(F0(X), G0(Y))

D = Set のときは、


∀X∈|C|.
∀x.(x∈F0(X) ⇔ x∈G0(X))

∀X, Y∈|C|.
∀x∈F0(X).
F1X,Y(f)(x) = G1X,Y(f)(x) on set G0(Y)

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

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

自然変換に関する等式

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

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

  • α, β::F⇒G:CopSet in CAT

したがって、等式は、

  • α = β on set CAT2(F, G)

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

  • α = β on set Nat(F, G:CopSet)

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


∀X∈|Cop|.
αX = βX on set Set(F(X), G(X))

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


∀X∈|Cop|.
∀x∈F(X).
αX(x) = βX(x) on set G(X)

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


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



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

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