Avendia19
English

日記 (2019 年 1 月 21 日)

久しぶりに解析的関手や正規関手に触れることになったので、 分かったことをまとめるため、 1 年ほど前の日記の続きを書いていこうと思う。

各種概念の定義や性質については過去の日記に説明を譲ることにする。 私が復習するに当たって説明が少し不十分だと感じた部分については、 追記として加筆しておいた。 1 つだけ以降の議論で重要になる定理があるので、 ここでも繰り返しておく。 以下は、 2 月 6 日の定理 7 である。 今後の議論の都合上、 式の右辺の直積の左右を逆にしてある。

1

圏同値 [SetA,SetB]NFSetB×expA が成立する。

正規関手 F:SetASetB に対し、 󰂡F: B×expA Set (b,γ) #{(γ,c) の形の El(Fb) の正規対象の同型類} とおき、 逆に関手 M:B×expASet に対しては、 各 bB に対して、 M󰂦b: SetA Set X 󰄘γexpA(M(b,γ)×HomSetA(γ,X)) とおく。 すると、 これらが定理中の圏同値の対象の対応を与えるのであった。

さて、 正規関手の特徴付けとして、 フィルター余極限と広義引き戻しを保つというものがあったのを思い出そう。 この条件を少し厳しくして、 フィルター余極限だけでなく全ての (小さな) 余極限を保つ関手を考える。

2

関手 F:SetASetB をとる。 F が余極限と広義引き戻しを保つとき、 F線型linear であるという。

さらに、 このような関手が成す圏も考える。

3

[SetA,SetB]LF を、

として定義する。 ここで、 カルテシアン自然変換の同値性は、 [SetA,SetB]NF を定義したときと同じものであるとする。

4

CAAccLF を、

として定義する。

以上のようにすると、 定理 1 と同様の形の圏同値が線型関手に関しても存在する。

5

圏同値 [SetA,SetB]LFSetB×A が成立する。

まず、 線型関手 F:SetASetB に対し、 󰂡F: B×A Set (b,a) #{({a},c) の形の El(Fb) の正規対象の同型類} とおき、 逆に関手 M:B×ASet に対しては、 各 bB に対して、 M󰂦b: SetA Set X 󰄘aA(M(b,a)×Xa) とおく。 すると、 定理 1 の証明と同様にして、 これらの対応が定理中の圏同値を与えることが示せる。 詳細はここでは省略することにする。

さて、 この定理によって、 線型関手 F:SetASetB は集合族 󰂡FSetB×A と同一視できることが分かった。 この 󰂡F は、 B の元と A の元という 2 つのパラメータに対して集合が 1 つ定まっているものなので、 行に B の元が対応して列に A の元が対応するような無限の大きさの集合値行列だと思うことができる。 実際、 このようにして行列だと思うことには意味があり、 例えば以下の命題が成り立つ。

6

線型関手 F:SetASetB,G:SetBSetC に対し、 その合成に対応する行列は、 󰂡GF: C×A Set (c,a) 󰄘bB(󰂡G(c,b)×󰂡F(b,a)) で与えられる。

XSetAcC に対して、 定義に従って計算すると、 (GF)cX 󰄘bB(󰂡G(c,b)×(FX)b) 󰄘bB󰄘aA(󰂡G(c,b)×󰂡F(b,a)×Xa) 󰄘aA((󰄘bB(󰂡G(c,b)×󰂡F(b,a)))×Xa) となる。 したがって、 命題が示された。

この命題を踏まえて、 直積上の集合族の合成を以下のように定義する。

7

集合族 MSetB×A,NSetC×B に対し、 NM: C×A Set (c,a) 󰄘bB(N(c,b)×M(b,a)) として集合族 NMSetC×A を定義し、 これを MN合成composition という。

この合成の式は、 通常の行列の積と全く同じ形をしており、 上の定理から関手と集合族の同一視と両立している。 線型代数の理論においては、 線型空間の間の線型写像は基底を固定すれば行列と同一視でき、 写像の合成と集合の積はこの同一視と両立しているが、 まさに同じことが線型関手と集合族の間にも成立するのである。 そこで、 以降は B×ASet の形の集合族のことを、 単に行列と呼ぶことにする。

なお、 線型関手が行列に似ているので、 線型関手の名前は線型代数から来ているように思えるが、 実際にはおそらく線型論理から来ている。 これは今後の日記で扱うが、 線型関手を射とする圏 CAAccLF は、 線型論理の圏論的モデルになるのである。

追記 (2019 年 4 月 7 日)

本文で述べたように、 集合族 MSetB×A と線型関手 M󰂦:SetASetB は同一視でき、 M は行が B の元を表し列が A の元を表す行列だと見なせる。 例えば、 A が 3 元集合で B が 2 元集合であるとし、 A=:{a1,a2,a3}, B=:{b1,b2} と表すことにすれば、 M=( M(b1,a1) M(b1,a2) M(b1,a3) M(b2,a1) M(b2,a2) M(b2,a3)) と書き表すことができる。

このような見方をした場合、 集合族 XSetA は列ベクトルだと見なすと都合が良い。 実際、 集合族 MSetB×A が与えられたとき、 M と対応する線型関手 M󰂦:SetASetBX における値を YSetB とすると、 Y: B Set b 󰄘aA(M(b,a)×Xa) が成り立つ。 この右辺は線型代数の理論における行列と列ベクトルの積に非常に似ている。 先程と同じく例えば A=:{a1,a2,a3}, B=:{b1,b2} の場合であれば、 上の関係は、 ( Yb1 Yb2)=( M(b1,a1) M(b1,a2) M(b1,a3) M(b2,a1) M(b2,a2) M(b2,a3))( Xa1 Xa2 Xa3) とより行列らしく書ける。 この式の右辺は、 通常の行列の積のように計算し、 数の和と積と代わりに集合の直和と直積を用いることにすれば、 完全に正当化できる。

参考文献

  1. R. Hasegawa (2006) 「Two applications of analytic functors」 『Theoretical Computer Science』 272:113–175