2015-10-22

既約性

$x^n + x - 1$ が既約であることと $n \not \equiv 5 \pmod 6$ であることが同値みたいなんだけど，どうやって証明するんだかわからなくて気になってとりあえず調べてみたことを書きます。

http://mathoverflow.net/questions/177789/is-xn-x-1-irreducible によると $x^n - x - 1$ は既約なので，それを認めると，n が偶数であれば -x を代入して $x^n + x - 1$ も既約であることがわかる。だから奇数の場合の既約性だけが問題になる。

http://math.stackexchange.com/questions/264853/irreducibility-of-xnx1 によると， $n \not\equiv 2 \pmod 3$ ならば $x^n + x + 1$ は既約なので，それをふたたび認めると，n が奇数のとき先程と同様に -x を代入することで $n\not\equiv 2 \pmod 3$ ならば $x^n + x - 1$ は既約であることがわかる。奇数について $n\not\equiv 2 \pmod 3$ は $n\not\equiv 5 \pmod 6$ と同値だから，n が奇数かつ $n\not\equiv 5 \pmod 6$ ならば $x^n + x - 1$ は既約である。

ということは，これらを合わせると $x\not\equiv5 \pmod 6$ ならば $x^n + x - 1$ は既約であることがわかる。

$x=5 \pmod 6$ のときは $x^n + x - 1$ は $x^2 - x + 1$ で割り切れることが容易に確かめられるから，最初に述べた同値性がわかった。

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

普通に日本語を話す

日常

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

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

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

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

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