2015-09-26

圏論ぐらい普通に生きてればわかる人

世の中には二種類の人間がいる。普通に生きてれば圏論がわかる人と，そうでない人だ。

とかいうのは仮に真だとしても圏論を勉強するうえで何の助けにもならないし，だいたいきれいに二つに分けられるはずもないのですが，しかしある程度は正しいことを言っているのではないかと思います。

圏論に限らず，ものごとの理解の難しさには，人ごとに違いがあります。同じ人でも，対象によって簡単だったり難しかったりします。それが何によって決まっているかといえば，おそらくその人がその瞬間までにどういう経験をしてきたか，でしょう。圏論を理解することについていえば，それがある人にとってどれくらい難しいかは，その人がこれまでにどんな数学的概念にどれだけ親しんできたかに強く依存するでしょう。高校までの数学しか知らない人が圏論を勉強しようとすればかなりの困難が予想されるし，逆に既に抽象代数に慣れている人にとっては圏論の基本的な事項（関手とか極限とか）を理解するくらいは難しくないでしょう。個人的な経験として，普遍写像性を使った議論にははじめから馴染めた記憶がありますが，これはあらかじめ普遍写像性がどういうものかを具体例（直積，商，局所化，テンソル積など）を通じて「既に知っていた」ことが大きく影響しているだろうと思います。いろんな概念が一つの型に納まってしまうのを見て，なるほどうまいことやるものだと感心したものです。

そういう現象は別に数学に限ったことでは全然なくて，例えばスポーツの苦手な人が初めて野球をやったらたぶんバットをボールに当てることができないと思うんですが，できる人は野球をやったことがなくてもきちんと打てたりします。実際，中学のとき同じクラスにスポーツが得意だけど野球はやったことがないらしい人がいましたが，体育の授業でソフトボールをやったらその人は最初からちゃんと打てるんですね。一方，僕は野球はそこそこ好きでたまに友人とやっていたけど，下手なので，あんまり打てない。スポーツのできる彼がいうには「ボールをよく見れば打てる」のだそうですが，よく見ると言われても，できない人にはそもそもそれがどういうことだか想像がつかないのです。

圏論がわかる人とそうでない人の間にもきっと溝があって，わかる人は定義といくつかの例や定理を見て飲み込めるけど，そうでない人はそう簡単にはいかなくて，定義や例や定理をどうやって咀嚼して自分のものにすればいいかわからないのではないでしょうか。「ボールをよく見る」に相当するものが圏論でいうと何なのかはわかりませんが，「定義より明らか」などは近いかもしれません。どちらも簡単なことだと言いたげな言葉遣いですが，それは必要な経験を積んでいる者にしか通じない。

2015-08-14

掛け算と割り算は随伴

m が正整数のとき $m x \leq y \iff x \leq \lfloor y/m \rfloor$ となることを証明する。

適当な仮定の下で $R : \mathcal C \to \mathcal D$ の左随伴 L は $LD \simeq \lim (\pi : D \downarrow R \to \mathcal C)$ と表される。そこで $\mathcal C = \mathcal D = \mathbb Z$ （普通の順序で圏とみなす）かつ $R y = \lfloor y/m \rfloor$ の場合を考える。すると， $\mathbb Z$ における極限は最小値なので，確かに

$Lx = \lim (\pi : x \downarrow R \to \mathbb Z) = \min \{ y \mid x \le \lfloor y/m \rfloor \} = mx$

となることがわかる。

2015-06-22

多項式の微分は積の微分から出てくる

多項式を微分すると指数が係数に出てくるのって，積の微分の公式 $(fg)' = f' \cdot g + f\cdot g'$ と $x' = 1$ を使って

$(x^2)' = x' \cdot x + x \cdot x' = x + x = 2x$
$(x^3)' = (x^2)' \cdot x + x^2 \cdot x' = 2x^2 + x^2 = 3x^2$

とかやると出てくる。

ということに，多項式を計算機上でいじることについて考えていて初めて気付いた。

2015-06-19

積分

日常

ぼくにとって，数学といえば積分らしい。

それはきっと昔からそうで，ぼくにとって「積分」という言葉と積分記号は特別なものなのだろうと思う。例えば，あなたが誰かに向かって数学の話をしているところを想像して下さいと言われたら，黒板かホワイトボードに積分記号を書いているところを思い浮かべそうな気がする。普段は解析を使うようなことをあまりしないから，積分という概念自体はそれほど身近なものとはいえなくなっている気がするけど，そうなってから何年も経ってもやはりぼくにとって積分の特別さは変わらないものらしい。

どうして積分なのか，ということは，長い間気にしたことがないどころか，積分というものが頭の中の目立つ場所に居座っていることに気付いてすらいなかった。数年前にようやく，どういうきっかけだったか忘れたが，どうやらぼくの頭には積分という言葉が頻繁に浮かんできているようだということに気がついた。その後もそれがなぜなのかを考えた記憶はほとんどない。ところがこの間突然，これもきっかけは忘れてしまったが，もしかしたらあれではないかという記憶に思い当たった。中学の数学の授業中に積分の話を少しだけ聞いたことがあって，それが高校生になって実際に積分を学ぶまでずっと気になっていたのだ。

その中学の授業中に聞いた話というのは，扇形の面積が「半径×弧長÷2」になるということを習ったときに余談として出てきたものだ。この面積の式は三角形のそれと似ているけど，これは偶然ではなくて，細い三角形が無数に並んでいるとみなして計算すればこうなると理解できるということ。それから，今のは厳密ではない説明だけど，積分というのがあって，それを使うとこのアイデアはもっと厳密な議論に落とし込むことができるのだということ。その二つのことを聞いたのだと思う。

それ以上の説明は聞かなかったから，積分というものがどういうものなのかはわからなかった。でも，その時に出てきた「積分」という言葉はそれ以来ずっと覚えていたし，何か気になる，という気持ちを持ち続けていた。過去を思い返してみると，数学に対する興味は昔からあっても，具体的な数学の概念に対して興味を持ったことはそれまでにはなかった気がする。だからもしかすると「よくわからないけどおもしろそうだ」とかいうことを思ったのはそれが最初だったのかもしれない。そういうことがあったから，ぼくの頭の中では「積分」という言葉やあの記号が何か数学の魅力の象徴のようなものとして位置付けられているのだろうか。

2015-06-11

Lean をインストールしてみた

Lean 本体

最初，github にあるソースを自分でコンパイルしようとしたらうまくいかなかった。apt-get で入るので始めからそうすればよかった。

https://leanprover.github.io/download/ に環境ごとのインストールのしかたが書いてある。

Emacs の lean-mode

Emacs のモードがけっこうちゃんとしているみたい。インストールのしかたは https://github.com/leanprover/lean/blob/master/src/emacs/README.md に書いてある。

なんかいろんなパッケージに依存しているらしいけど，Installation のセクションの最初に書いてあるコードを何も考えずに *scratch* に貼り付けて評価したら全部勝手に入った（多分）。最近は elisp のパッケージ管理のための仕組みも整備されてきているようだけど，時代に追いつけていないのでよくわからない。

あとは，本体を apt-get で入れたので Case 2 に書いてあるやつを見て適当にいじって init.el に設定を書いた。

;;; lean-mode
(when (file-exists-p "/usr/share/emacs/site-lisp/lean/")
  (add-to-list 'load-path "/usr/share/emacs/site-lisp/lean/")
  (autoload 'lean-mode "lean-mode" nil t)
  (setq lean-rootdir "/usr")
  (add-to-list 'auto-mode-alist '("\\.h?lean$" . lean-mode)))

lean-rootdir をちゃんとセットしないと lean-mode の挙動がなんかおかしなことになった。lean のプロセスを起動してそれとやりとりしようとしてうまくいってないように見えた。

ドキュメント

https://leanprover.github.io/documentation/ に置いてある tutorial がかなり充実してそう。

まだ Chapter 4 までしか目を通していない（しかも斜め読み）けど，説明は丁寧そうなので証明支援系にそんなに慣れてなくても読めるかも。Curry-Howard 同型の説明とかもしてる。

2015-05-23

普通に日本語を話す

日常

「普通においしい」「普通に嫌い」「普通に言う」などの表現に違和感がある。自己の判断を述べる際に，なぜわざわざ「普通に」と付けるのか。どういう意味で普通だと言っているのかよくわからないし，そもそもそんな疑問が浮かぶ以前に，響きに違和感がある，とも思う。

でもここで正しい日本語がどうのという話をする気はない。

「やっぱり」という言葉がある。この言葉をまったく使わないという人はあまりいないと思うし，よく耳にする言葉だが，それはどういう意味かとあらためて考えてみると，これもまたはっきりしない。

「やっぱり」とは何か，ということについては森本哲郎『日本語表と裏』に面白いことが書いてある。日本人はとかくみんなと同じでなければならないと思いがちで，周りと異なる存在になることを恐れる。そういう傾向を持っているから，何か意見を述べるときにも単に自分はこう思いますと言うだけではなくて，これは異質な意見でも何でもなくて，自分はみんなと同じことを考えているのですと言いたがる。そこで「やっぱり」と付けることで，世間一般の人たちがそう思っているのと同じように，自分もそう思います，というニュアンスを出すのではないか。そんなようなことが書かれている。

普通に，と言うのもそういう意識があるからじゃないだろうか，と思うと腑に落ちる気がした。やっぱり日本語なのだ。

2015-05-01

well-definedness と universal map

well-definedness 周りの議論ってわりと何してるのかわかりにくくない？と思って考えてたら universality のほうがわかりやすい気がしてきりしたので書いてみた。

以下 $A$ , $B$ は集合， $E$ は $A$ 上の同値関係。

well-defined とは

写像 $f: A/E \to B$ が well-defined であるとはどういうことか，ということから一応。

まず well-defined であるという述語は，写像そのものに適用されるものというよりは，その定義に適用されるものであることに注意する。確かに言葉の上では「この写像は well-defined である」などという言い方をするのだが，このような言明は普通，写像の定義に伴って表れるものであり，その実際の内容は「今述べた定義は確かに写像を一つ定めている」ということである。したがって意味的には well-defined とは数学的対象に関する概念ではなくその記述方法というメタなレベルのことがらに関する概念であるということになる。

では $f([a]) = e\{a\}$ を写像 $f$ の定義だとしよう。ここで $a$ は変数であり $[a]$ は $E$ に関する同値類を表す。右辺の $e\{a\}$ *1 は $a$ を含む式である。変数とは何かとか式とは何かとか言い出すと面倒なことになりそうなので，細かいことは言わないで素朴に解釈することにしてほしい。それと，別に式を使って等式の形で定義を述べなければならないわけではないが，話を簡単にするためにそうした。

これが well-defined であるとはどういうことか。写像 $f$ に渡されるものは $A/E$ の要素であり，すなわち同値類なのだから，少なくとも建前としてはまず同値類 $x \in A/E$ が与えられ（この時点では代表元は与えられていない）， $f(x)$ を定めなければならない。そのために同値類から代表元 $a \in x$ を取って云々，とやるのだから， $a$ のとり方を変えたときに式 $e$ が違う値になってしまうといけない。そのような問題が起きない，ということが well-defined であるということである。正確に書けば $a E a' \implies e\{a\} = e\{a'\}$ でなければならない。これが確かめられればさっきの $f$ が確かに写像として定義される，すなわち well-defined であるということが結論できる。こういう話であった。

写像の分解と見る

さっき $e\{a\}$ は「式である」と雑な言い方をしたが，要するに $a$ は $A$ の元を指示する変数であり， $e\{a\}$ は $B$ の元を表すのだから， $e\{a\}$ と書いたのは結局のところ写像 $e : A \to B$ であると思ってもよさそうである。（このあたりはずいぶんいい加減なようだが，そもそも大雑把な話をしているということで見逃してほしい）

そうるすとさっきやったことは見方を変えてこのように理解できる。写像 $e : A \to B$ を与え，それが性質 $a E a' \implies e(a) = e(a')$ を持つことを確認せよ。それができれば確かに $f: A/E \to B$ が定義されたことになる。これが商集合上の写像が well-defined であると言うときに行われていることである。

ついでに言うとこの $f$ は， $\pi : A \to A/E$ を射影として $f \circ \pi = e$ を満たす。つまり，最初に与えた写像 $e$ を射影によって分解することで欲しい写像を得ているのである。

よく見てみると，こちらの見方の中には「定義の記述」のようなものが現れないことがわかる。そうではなくて，いきなり定義しようとしている写像の定義域 $A/E$ を考えないで，まずは商をとる前の $A$ からの写像を定めよ，そしてそれがある性質を満たしていることを確認せよ，そうすれば望む写像が得られる，と言っている。つまり，いきなり商集合の上の写像を定義しようとするとそれがちゃんと定まるかどうかがわからないので「その定義は well-defined であるかどうか」というメタな話が出てくるのに対して，商をとる前の集合を相手にすることで「別のある写像が要求された性質を満たすかどうか」という数学的対象についての話に置き換わったわけだ。

メタレベルを意識しなくても理解が可能な分，後者の説明のしかたのほうがすっきりしていて分かりやすいように思われる。初学者にとってどうかはわからないが，僕にとってはこちらのほうが納得がいくように感じる。

普遍写像性

ところで，これに似たような状況は数学でよく出てくる。いわゆる普遍写像性というやつである。

その言葉でさっきの話をきちんと書くとこうなる。関手 $\Delta: \mathbf{Set} \to \mathbf{Setoid}$ を $\Delta(X) = (X, \Delta_X)$ （つまり集合をその上の普通の意味の等しさと組にして setoid とみなす）で定めたとき，setoid $(A, E)$ から $\Delta$ への universal arrow が射影 $\pi: A \to A/E$ である。

随伴関手の言葉にすると，上の $\Delta$ は setoid $(A, E)$ から商集合 $A/E$ を作る関手の右随伴であると言うことができる。すなわち $\mathbf{Set}(A/E, B) \simeq \mathbf{Setoid}( (A, E), \Delta(B) )$ である。また，この同型は $\pi: A\to A/E$ による引き戻しで与えられる。

普通の議論のしかたをこの表現と対応付けてみる。いま写像 $f : A \to B$ があり，これが $a E a' \implies f(a) = f(a')$ を満たすとする。これはすなわち， $f \in \mathbf{Setoid}( (A, E), \Delta(B) )$ を仮定するということに他ならない。このとき， $\bar f : A/E \to B$ であって， $\bar f \circ \pi = f$ を満たすものが一意的に存在する。これは， $\pi$ による引き戻しが全単射であるという上に述べた事実の単なる言い換えである。

*1:あまり標準的でない記法なのは他の括弧を使うと紛らわしかったため