雑記帳
【泥沼】 様々な "カノニカルな写像" とやらの具体的な構成方法に真面目に向き合ってみる
カノニカルな写像を具体的に構成する
まず「カノニカル」って何？
抽象数学をやっていると、しばしば「カノニカルな写像 / 標準的な写像 (canonical mapping)」とかいう (現時点では一般に厳格な定義が与えられていないとされている) 漠然としたワードと遭遇する。
恐らく、この「カノニカルな写像」の意味がいまいちつかめなくて困った経験をした初学者は珍しくないと思うのだが、それが通常どういった意味合いで使用されるのかを強いて言葉にするのであれば、
- 与えられたドメインとコドメインを持つ写像の内、数学の慣習に馴染みのある多くの人が、使用されている文脈から想定するであろう特定の写像
といった感じになる。(とはいえこれに対する認識は、個々人で違いがあるかもしれない)
一応パッとしない人がいるかもしれないので、以下にその「カノニカルな写像」の具体例も幾つか挙げておく。
- 「カノニカルな写像 \(A\times B\rightarrow B\times A\)」といえば通常、第一成分と第二成分の入れ替え
- 「カノニカルな写像 \({\mathbb{Q}}\rightarrow {\mathbb{R}}\)」といえば通常、有理数から実数へのキャスト
また余談にはなるが
- 初めからそこにある (公理的に存在を認めている) 写像と、既存の写像から新たな写像の存在を誘導するための (公理的に認めている) 操作の組み合わせとして得られる「人為的に定義されるよりも前に、初めからそこに自然と存在していたと考えることができる写像」
に対して「カノニカルな写像」というワードを使う場合もあるかもしれないが、そうなると「選択公理を欠いた ETCS 集合論」で構成される写像は基本的に漏れなくすべて「カノニカルな写像」扱いになる。
余談
僕が持っている集合論の教科書の１つである斎藤毅さんの「集合と位相」でも、標準的な写像は「自然に定まっているように思える写像」というかなりフワッとしたものになっている。
カノニカルな写像に対する具体的な構成を示せないのか？
圏論に浴びせられる常套文句の１つに「圏論は地に足ついてない」といったものがある。
確かに、圏論での主役は「対象 (集合)」から「矢印 (写像)」に置き換わり、その中で前節で挙げたような杜撰な写像の取り扱いが披露されているのを目の当たりにしてしまうと、そのような圏論に対するネガティブな印象を持ってしまうのも無理はない。
しかし、実のところは
- 具体的な構成が技術的に不可能だから、そういったフワッとした謎のワード「カノニカル」で読者を煙に巻いている
のではなく、
- 純粋圏論的に具体的な構成を与えること自体はできるが、とにかく煩雑で全容を書き下すのが面倒であり、そういった写像の具体的な構成を自明なこととしてスキップために「カノニカル」という表現を便宜的に用いる
といった方が実情に近いかもしれない。
とはいえ、言葉でそう説明されたとしても具体例無しで納得までしてくれる人は多くないかもしれないので、この記事ではカノニカルな写像と表現されがちな様々な写像の具体的な構成方法を、全ての有限余積を持つカルテシアン閉圏の設定の下で紹介してみる。
具体例
現在の「全ての有限余積を持つカルテシアン閉圏」という設定において、その一般論で扱う圏の射を「写像」と呼ぶことについて多少の語弊があるため、以降は「カノニカルな写像」ではなく「カノニカルな射」という表現を使用していく。(詳しくは ETCS 等の圏論的集合論の記事を参照)
またその設定を採用している理由は、例によって「Haskell での機械的な動作検証」が可能なためである。
カノニカルな射 A×B→B×A
ここで意図しているカノニカルな射 \(i_1:A\times B\rightarrow B\times A\) は、前置きの中でも触れたが 第一成分と第二成分の入れ替えを行う射であり、数学的には
\[
i_1 = \langle {\rm prj}_2, {\rm prj}_1 \rangle
\]
というように構成できる。
ちなみにこのサイトでは、その射に対して \({\rm tw}\) という記号を割り当てている。
Haskell で書くと
i_1 :: (a *** b) -> (b *** a)
i_1 =
pair(prj2,prj1)カノニカルな射 (A×B)×C→A×(B×C)
ここで意図しているカノニカルな射 \(i_2:(A\times B)\times C\rightarrow A\times (B\times C)\) は、\(A,B,C\) の各々の対象の要素に対して非自明な処理を適用することなしに成分のぶら下がりの構造だけを変化させるものであり、
\[
i_2 = \langle {\rm prj}_1{\sf \, ⨟ \,}{\rm prj}_1, \langle {\rm prj}_1{\sf \, ⨟ \,}{\rm prj}_2, {\rm prj}_2 \rangle \rangle
\]
というように構成できる。
Haskell で書くと
i_2 :: ((a *** b) *** c) -> (a *** (b *** c))
i_2 =
pair(prj1-:prj1,pair(prj1-:prj2,prj2))カノニカルな射 A+B→B+A
ここで意図しているカノニカルな射 \(i_3:A+B\rightarrow B+A\) は、\(A,B\) の要素に付けられる第一入射と第二入射を入れ替える射であり、数学的には
\[
i_3 = \left(\begin{matrix} {\rm inj}_2 \cr {\rm inj}_1 \end{matrix}\right)
\]
というように構成できる。
Haskell で書くと
i_3 :: (a +++ b) -> (b +++ a)
i_3 =
coPair(inj2,inj1)カノニカルな射 (X×A)+(X×B)→X×(A+B)
ここで意図しているカノニカルな射 \(i_4:(X\times A)+(X\times B)\rightarrow X\times (A+B)\) は、数学的に厳密ではないが、人が理解しやすいインフォーマルな形で書くとするならば
i_4_informal :: ((x *** a) +++ (x *** b)) -> (x *** (a +++ b))
i_4_informal x'a_or_x'b =
case x'a_or_x'b of
Left (x,a) -> (x,Left a)
Right (x,b) -> (x,Right b)といった感じの振る舞いをする射である。
この射は、分配的圏 (distributive category) の定義の際に登場する「カノニカルな射」として知られるものであり、数学的には
\[
i_4 = \left(\begin{matrix} X\times {\rm inj}_1 \cr X\times {\rm inj}_2 \end{matrix}\right)
\]
というように構成できる。
機械による動作チェックを行っているとはいえ、情報源がここだけだと信憑性に欠けると思われる気もするので、一応同じ情報を提供している外部の記事も紹介しておく。
- distributive category (nLab 記事)
Haskell で書くと
i_4 :: ((x *** a) +++ (x *** b)) -> (x *** (a +++ b))
i_4 =
coPair(id***inj1, id***inj2)カノニカルな射 X×(A+B)→(X×A)+(X×B)
ここで意図しているカノニカルな射 \(i_4:X\times (A+B) \rightarrow (X\times A)+(X\times B)\) は、数学的に厳密ではないが、人が理解しやすいインフォーマルな形で書くとするならば
i_5_informal :: (x *** (a +++ b)) -> ((x *** a) +++ (x *** b))
i_5_informal x'a_or_b =
case x'a_or_b of
(x,Left a) -> Left (x,a)
(x,Right b) -> Right (x,b)といった感じの振る舞いをする射であり、先のカノニカルな射のインヴァースに相当する。
人間の理解しやすさを意識した構文の上では、先のカノニカルな射の特徴付けとの間に大きなギャップは感じられないかもしれないものの、数学的な構成方法をしっかり考察してみると気付くことができるようにこちらの構成にはその過程で「カルテシアン閉」であることが要求される。
\[
i_5 = {\rm tw}{\sf \, ⨟ \,} \left( \left(\begin{matrix} \lambda[{\rm tw}{\sf \, ⨟ \,} {\rm inj}_1] \cr \lambda[{\rm tw}{\sf \, ⨟ \,} {\rm inj}_2] \end{matrix}\right) \times X \right){\sf \, ⨟ \,} {\rm ev}
\]
余談
その射のドメインとコドメインを見ての通り、それら対象自体は最低限「全ての有限余積と有限積を持つ圏」の設定さえあれば考えることができるのだが、それら対象の間を結びつけるこの矢印が実際に存在するのかどうかは、その種類の圏の一般論の中では実は非自明となる。
つまるところ、「○○をカノニカルな射とする」などと言いながらある射を議論に持ち出したつもりになっていたとしても、数学的厳密に考え直した時「実はその射は一般に構成できないものだった」というケースが事実存在することになる。
そしてその意味でも、何でもかんでも「カノニカルな射」というワードを使って、射の具体的な構成をスキップすることは、最低限数学的な勘がしっかりと養われるまでは避けた方が安全なのかもしれない。(とはいえ、「カルテシアン閉」という条件すら削ぎ落とされた非常に弱い設定を数学の基礎に設定する物好きがいるのかは知らないけど...)
Haskell で書くと
i_5 :: (x *** (a +++ b)) -> ((x *** a) +++ (x *** b))
i_5 =
tw-:(coPair(trans(tw-:inj1),trans(tw-:inj2))***id)-:evカノニカルな射 Xᴬ×Xᴮ→Xᴬ⁺ᴮ
ここで意図しているカノニカルな射 \(i_6:X^A\times X^B\rightarrow X^{A+B}\) は、Haskell でいうところの either 関数に相当する。
either 関数に相当する。数学的に厳密ではないが、人が理解しやすいインフォーマルな形で書くとするならば
i_6_informal :: ((x ^ a) *** (x ^ b)) -> x ^ (a +++ b)
i_6_informal (f,g) a_or_b =
case a_or_b of
Left a -> f(a)
Right b -> g(b)といった感じの振る舞いをする射である。
(より数学寄りの説明をすると、「2つの共通するコドメインを持つ射に対して、それらから引き起こされる余積に関する仲介射を与える射」に対応する。)
こうみると、別段全く複雑な感じはしないと思うのだが、このコードの中には「純粋数学的には扱えない記号操作」が含まれていて、その操作を数学的に意味のあるものとして解釈する過程が少し煩雑になる。
実際この射の構成は、ここで紹介するものの中で最も込み入った構成となり、具体的には以下となる。
\[
i_6 = \lambda\left[\left({\rm tw} {\sf \, ⨟ \,} \left(\left(\begin{matrix} \lambda[{\rm tw} {\sf \, ⨟ \,} {\rm inj}_1] \cr \lambda[{\rm tw} {\sf \, ⨟ \,} {\rm inj}_2] \end{matrix}\right) \times (X^A\times X^B)\right) {\sf \, ⨟ \,} {\rm ev} \right) {\sf \, ⨟ \,} (\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2,\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1,{\rm prj}_2 \rangle \rangle + \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1, \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2,{\rm prj}_2 \rangle \rangle) {\sf \, ⨟ \,} ((X^B\times {\rm ev})+ (X^A\times {\rm ev})) {\sf \, ⨟ \,} \left(\begin{matrix} {\rm inj}_1\times X \cr {\rm inj}_2\times X \end{matrix}\right) {\sf \, ⨟ \,} {\rm prj}_2 \right]
\]
(見ての通りこれまで構成したカノニカルな射の組み合わせになっているのだが、どうしてこうなるのかを是非自身で考えてみよう！)
Haskell で書くと
i_6 :: ((x ^ a) *** (x ^ b)) -> x ^ (a +++ b)
i_6 =
trans((tw-:(coPair(trans(tw-:inj1),trans(tw-:inj2))***id)-:ev) -:
(pair(prj1-:prj2,pair(prj1-:prj1,prj2))+++pair(prj1-:prj1,pair(prj1-:prj2,prj2))) -:
((id***ev)+++(id***ev)) -:
(coPair(inj1***id,inj2***id))
-: prj2)カノニカルな射 Aᴸ×Bᴸ→(A×B)ᴸ
ここで意図しているカノニカルな射 \(i_7:A^L\times B^L\rightarrow (A\times B)^L\) は、一つ前のカノニカルな射の圏論的積バージョンで、
- 2つの共通するドメインを持つ射に対して、それらから引き起こされる積に関する仲介射を与える射
に相当するものである。
こちらは余積バージョンと比較するとシンプルで
\[
i_7 = \lambda[\langle \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1,{\rm prj}_2 \rangle, \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2,{\rm prj}_2\rangle \rangle {\sf \, ⨟ \,} ({\rm ev}\times {\rm ev})]
\]
Haskell で書くと
i_7 :: ((a ^ l) *** (b ^ l)) -> (a *** b) ^ l
i_7 =
trans(pair(pair(prj1-:prj1,prj2),pair(prj1-:prj2,prj2))-:(ev***ev))あとがき
圏論には「地に足ついてない」のほかにも「簡単なことを無駄に難しくしている」という批判があるのだが、恐らくこの記事を介してその印象が一層強まってしまった人もいるだろう。
しかし捉え方次第では「簡単なことを無駄に難しくしている」わけではなくて
- 雰囲気で数学をやっている分には簡単に思えてしまう内容であっても、数学的に厳密な取り扱いへの移行を試みると、それまで認知できていなかった理論的な脆弱さの問題にぶち当たり、その点を解消しようとするとどうしても込み入った議論が必要になってくる
つまり「簡単と思われていたことが、実は全く簡単ではなかったことを明らかにしている」という見方もできないだろうか。
身近なものとしては
- 「自然数の足し算に対する結合法則や交換法則」(数学的帰納法が数学の基礎として認めている公理たちからどのように１つの定理として演繹的に証明されるのか)
- 関数の連続性や極限 (それらの数学的にかなり厳密な取り扱い)
などがそれに該当するだろう。
第一に数学的な厳密性に一切こだわらないのであれば、このページの内容自体全て無意味なものに見えるのだと思うが、こういった一見すると不毛に思えることでも、真面目に向き合ってみると案外思いがけない事実や面白い物語と巡り合えることも珍しくないので、食わず嫌いをしないでこの種の問題にたまには真剣に向き合うことも有意義ではないのかと。
この記事で使用した Haskell コード
{-# LANGUAGE TypeOperators #-}
import Data.Void
main :: IO ()
main = return ()
class (MyShow a) where
myShow :: a -> String
instance MyShow () where
myShow = const "*"
instance (MyShow a, MyShow b) => MyShow (Either a b) where
myShow = either
(\z -> if (myShow z == "*") then "inj1" else (myShow z) ++ ";inj1")
(\z -> if (myShow z == "*") then "inj2" else (myShow z) ++ ";inj2")
instance (MyShow a, MyShow b) => MyShow (a,b) where
myShow (x,y) = "(" ++ myShow x ++ "," ++ myShow y ++ ")"
instance MyShow Int where
myShow = show
instance MyShow (a -> b) where
myShow = const "(AN ARROW)"
-- X の要素を圏論に倣って終対象から X への射(Global element)として扱うための関数
el :: a -> (Pt -> a)
el = (const::a -> (Pt -> a))
-- Global elements 用 ユーティリティ
(===) :: Eq a => (Pt -> a) -> (Pt -> a) -> Bool
(===) x y = (x() == y())
showEl :: MyShow a => (Pt -> a) -> String
showEl x = (myShow $ x())
printEl :: MyShow a => (Pt -> a) -> IO ()
printEl = putStrLn . showEl
-- Diagrammatic-order な射の合成演算
(-:) = flip (.)
-- # 始対象と終対象
type Empty = Void
type Pt = ()
initArr :: Empty -> a
initArr = absurd
termArr :: a -> Pt
termArr = const ()
point :: Pt -> Pt
point = id
const' x = termArr -: x
-- # 余積対象と積対象
type (+++) a b = Either a b
type (***) a b = (a,b)
-- 入射
inj1 :: a -> a +++ b
inj1 = Left
inj2 :: b -> a +++ b
inj2 = Right
-- 射影
prj1 :: a *** b -> a
prj1 = fst
prj2 :: a *** b -> b
prj2 = snd
-- 余積対象の仲介射
coPair :: (a -> c, b -> c) -> (a +++ b -> c)
coPair = uncurry either
-- 積対象の仲介射
pair :: (c -> a, c -> b) -> (c -> a *** b)
pair = uncurry $ (<*>) . fmap (,)
-- 畳み込み
fol = coPair(id, id)
-- 対角射
dup = pair(id, id)
-- 射同士の余積
(+++) :: (a1 -> b1) -> (a2 -> b2) -> (a1 +++ a2 -> b1 +++ b2)
(+++) f g = coPair(f -: inj1 , g -: inj2)
-- 射同士の積
(***) :: (a1 -> b1) -> (a2 -> b2) -> (a1 *** a2 -> b1 *** b2)
(***) f g = pair(prj1 -: f, prj2 -: g)
-- Twist の形式的双対
coTw :: a +++ b -> b +++ a
coTw = coPair(inj2, inj1)
-- Twist
tw :: a *** b -> b *** a
tw = pair(prj2, prj1)
-- # Exponential 対象
type (^) b a = a -> b
-- 評価射
ev :: (b ^ a) *** a -> b
ev = uncurry id
-- 射の転置 (transpose) の構成
trans :: (c *** a -> b) -> (c -> b ^ a)
trans = curry
-- 射 h:a->b の Exponential 対象 (Exp b a) の要素への変換
arrToEl :: (a -> b) -> (Pt -> b ^ a)
arrToEl h = trans(prj2-:h)
elToArr x = pair(termArr, id) -: (x *** id) -: ev
i_1 :: (a *** b) -> (b *** a)
i_1 =
pair(prj2,prj1)
i_2 :: ((a *** b) *** c) -> (a *** (b *** c))
i_2 =
pair(prj1-:prj1,pair(prj1-:prj2,prj2))
i_3 :: (a +++ b) -> (b +++ a)
i_3 =
coPair(inj2,inj1)
i_4 :: ((x *** a) +++ (x *** b)) -> (x *** (a +++ b))
i_4 =
coPair(id***inj1, id***inj2)
i_4_informal :: ((x *** a) +++ (x *** b)) -> (x *** (a +++ b))
i_4_informal x'a_or_x'b =
case x'a_or_x'b of
Left (x,a) -> (x,Left a)
Right (x,b) -> (x,Right b)
i_5 :: (x *** (a +++ b)) -> ((x *** a) +++ (x *** b))
i_5 =
tw-:(coPair(trans(tw-:inj1),trans(tw-:inj2))***id)-:ev
i_5_informal :: (x *** (a +++ b)) -> ((x *** a) +++ (x *** b))
i_5_informal x'a_or_b =
case x'a_or_b of
(x,Left a) -> Left (x,a)
(x,Right b) -> Right (x,b)
i_6 :: ((x ^ a) *** (x ^ b)) -> x ^ (a +++ b)
i_6 =
trans((tw-:(coPair(trans(tw-:inj1),trans(tw-:inj2))***id)-:ev) -:
(pair(prj1-:prj2,pair(prj1-:prj1,prj2))+++pair(prj1-:prj1,pair(prj1-:prj2,prj2))) -:
((id***ev)+++(id***ev)) -:
(coPair(inj1***id,inj2***id))
-: prj2)
i_6_informal :: ((x ^ a) *** (x ^ b)) -> x ^ (a +++ b)
i_6_informal (f,g) a_or_b =
case a_or_b of
Left a -> f(a)
Right b -> g(b)
i_7 :: ((a ^ l) *** (b ^ l)) -> (a *** b) ^ l
i_7 =
trans(pair(pair(prj1-:prj1,prj2),pair(prj1-:prj2,prj2))-:(ev***ev))タグ一覧: