「数学」カテゴリーアーカイブ

R^3のベクトル積とso(3)のメモ

今回は \(\mathbf{R}^3\) のベクトル積とか回転行列とかに関する覚え書き。割と初等的。大学2年ぐらいのレベルだろうか。オチはない。

定義とか

3次の実正方行列全体の集合を \(M(3,\mathbf{R})\) で表す。3次の特殊直交群 \(SO(3)\) を\[
SO(3)=\{A\in M(3,\mathbf{R})\mid\det A=1,~{}^tAA=I\}
\]で定める。特殊直交群の元はいわゆる回転を表す行列である。

3次の交代行列全体の集合を \(\mathfrak{so}(3)\) で表す。\(\mathfrak{so}\) は小文字のsoをフラクトゥールで書いたものである。\[
\mathfrak{so}(3)=\{X\in M(3,\mathbf{R})\mid X+{}^tX=0\}
\]\(\mathfrak{so}(3)\) は3次元の実線形空間であり、\begin{align*}
E_1&=\begin{pmatrix}0&0&0\\0&0&-1\\0&1&0\end{pmatrix},&
E_2&=\begin{pmatrix}0&0&1\\0&0&0\\-1&0&0\end{pmatrix},&
E_3&=\begin{pmatrix}0&-1&0\\1&0&0\\0&0&0\end{pmatrix}
\end{align*}は一組の基底となっている。\(\mathfrak{so}(3)\) の元 \(X\in\mathfrak{so}(3)\) は実数 \(a,b,c\in\mathbf{R}\) により\[
X=\begin{pmatrix}0&-c&b\\c&0&-a\\-b&a&0\end{pmatrix}=aE_1+bE_2+cE_3
\]と書ける。

ベクトル積

続きを読む →

学園祭で来場者に複素関数を教えた話

11月22日から24日にかけて行われた東京大学駒場キャンパスでの第65回駒場祭で、数学科有志による「ますらぼ」企画(@UTmathlabo)に参加していました。「ますらぼ」では、数学科生・院生による発表、我々で作った冊子の配布、それから数学に関する展示が行われていました。

私は、かねてから作っていた複素関数を視覚化するWebアプリケーション “Conformality” に関する記事を書いたり、展示をしたりしていました。

冊子には、いくつかの複素関数の例・解説と、Webアプリの舞台裏に関する記事を書きました。一方、展示では、いくつかの複素関数の例・解説をポスター（というほどの紙の大きさでもない）で貼ったのと、パソコンとタブレットを用意して実際にWebアプリを動かしながら解説するのをやりました。

来場者に解説するとき、聞き手のレベルに合わせて話して、分かってもらうのは楽しかったです。実際どのぐらい理解してもらえたかは不明ですが…。あと、ふだんあまり喋らないので声が枯れました。

具体的に、レベルに応じてどんな内容を話したかというと、

小学生（！）

そもそも0や負の数はまだ習っていないので、まずはそこから。
複素数の足し算が平行移動になることを説明できれば十分すぎるだろう。

中学生

実数はOK。「数直線の数」みたいな感じ。
複素数を紹介。いずれ高校で習うよ、ということで。
複素数のかけ算ぐらいまでは解説しただろうか？
「関数」としては \(y=ax^2\) ぐらいがいいとこだったかな？と思ったが、中学校では「関数」として「一次関数」というのが出てくるのを失念していた。

高校生

現行の学習指導要領では数学IIIで複素数平面を扱う。複素数自体は、もっと前の2次方程式関連のところで出てくるはず。（高校では「複素数平面」というようだが、数学が専門の人は普通は「複素平面」と言う。私のような面倒くさがりな人には1文字少ないのはでかい）
学年としては、3年生は複素数平面知っているはず。2年生の11月では複素数平面をやっている学校があるかないか、という感じ。聞いてみたところ「明日（火曜日）から複素数平面の単元に入る」という人もいた。
事前に書店などに出向いて数学IIIの参考書を立ち読みしたところ、高校で扱うのは（今回関係ありそうなのは）複素数のかけ算の図形的な意味やド・モアブルの定理がせいぜいだということが分かった。
今は高校で行列を教えないので、一次分数変換と行列の関係を教えにくかった。
高校では実数の指数関数や三角関数を習う。

大学生

複素数や複素平面はまあ知っている（1、2年生や、文系の3、4年生も含めて）。
理系の3、4年生には一次分数変換の円円対応や正則関数の等角性まで知っている人もいて話が早かった。

という感じでした。

教える関数としては、当初は一次分数変換が一番単純かなあと思いましたが、高校生を視野に入れるなら複素数のかけ算（拡大縮小と回転）からやった方が学習の役にも立つだろうと思って、冊子やポスターでは最初に複素数のかけ算の例を載せました。しかし、実際に人に教えるときはもっと初歩的な、複素数の足し算の幾何学的意味（平行移動）から始めたので、他人への解説の仕方というのは自分だけで考えてもわからないものだということを認識しました。

解説内容はそのうちこのブログかどこかに載せたいと思います（時間があれば）。

余談として、「ますらぼ」の教室では学内無線LANが使えないので、Webアプリケーションを動かすには工夫が必要でした。持ち込んだ機器は

MacBook
- 解説の際の主力。
- ペアレンタルコントロールを設定したアカウントでWebブラウザを動かした。
- セキュリティースロットにワイヤーをつけて盗まれないようにした。6年半前にこのMacBookを買ってから初めてセキュリティースロットが活躍した。
Nexus 7
- 画面が小さいので微妙に使いづらかった。
- 制限アカウントを作って使ってもらった。
- タブレット本体にはセキュリティースロットがないので、サンワサプライの7インチタブレット向け盗難防止用具を買ってそれにワイヤーをつけた。
AirMac Express
- Nexus 7とMacBookを同一ネットワークにつなげた。

で、MacでWebサーバーを動かしてWebアプリケーションを動かす感じにしました。URLは本来の “https://miz-ar.info/webapp/conformality/” で動いているように見せたかったので、MacBookとNexus 7で d-poppo.nazo.cc がMacBookのIPアドレスに解決されるようにしました。

ドメイン名に対して好き勝手なIPアドレスを割り当てるためには /etc/hosts をいじるのが手軽な方法だと思います。しかし、Androidの場合は /etc/hosts をいじるにはroot権限を取る必要があり、調べてみたところ思いの外危なそう＆面倒くさそうだなあと思ったので、代わりに手元でDNSサーバーを動かすことにしました。MacBookにはDNSサーバーのソフトウエア（BIND9）が搭載されていた（最新のOSXにはないらしい）のですが、駒場祭直前にBIND9の使い方なんて覚えられない…。と思っていたらWebminとかいう便利なツールがあることを知ったので軟弱者の私はそれでBIND9を設定しました。めでたしめでたし。

滑らかな曲線をベジエ曲線で近似する

2件の返信

ベジエ曲線とは
滑らかな曲線をベジエ曲線で近似する
- JavaScriptによるコード例
差の評価

ベジエ曲線とは

ベジエ曲線とはWikipedia(英語版)によると(本当はちゃんとした文献を当たるべきなのだろうが)、\(n+1\) 個の点 \(x_0, x_1, \dots, x_n\) が与えられた時に\[
B(t)=\sum_{i=0}^{n}\binom{n}{i}t^i(1-t)^{n-i}x_i, \quad 0\le t\le 1
\]で定まる曲線らしい。始点 (\(t=0\)) は \(x_0\)、終点(\(t=1\))は \(x_n\) である。\(n\) のことを次数という。

(1次の場合は単なる線分なので置いておいて)よく使われるのは2次の場合と3次の場合である。それぞれ\begin{align*}
\mathit{quadratic B\acute{e}zier}(t)&=(1-t)^2x_0+2t(1-t)x_1+t^2x_2, \\
\mathit{cubic B\acute{e}zier}(t)&=(1-t)^3x_0+3t(1-t)^2x_1+3t^2(1-t)x_2+t^3x_3
\end{align*}で与えられる。

2次の場合は始点 \(x_0\) と終点 \(x_2\) の他に1個の制御点 \(x_1\)、3次の場合は始点 \(x_0\)、終点 \(x_3\) の他に2個の制御点 \(x_1\), \(x_2\) によって決まる。制御点は始点及び終点における接線を与えるためにある。ここではベジエ曲線についてはこれ以上突っ込んだ事は取り扱わない。

こういう、「制御点を与えて曲線を描く」のは、ドロー系の描画ソフトウエアを使ったことのある方はおなじみだろう。SVGやPostScriptなどのベクター画像形式でも、ベジエ曲線は基本的な描画対象である。

プログラミングに関して言うと、大抵のグラフィックAPIには2次か3次のベジエ曲線を描画するAPIがある。例えば、HTML5 Canvasの場合は

context.quadraticCurveTo(cpx, cpy, x, y) /* 2次 */
context.bezierCurveTo(cp1x, cp1y, cp2x, cp2y, x, y) /* 3次 */

というAPIがあり、Cocoaの場合は

NSBezierPath
-(void)curveToPoint:(NSPoint)aPoint controlPoint1:(NSPoint1) controlPoint2:(NSPoint)controlPoint2 /* 3次 */

というAPIがある。いずれも始点を指定する引数がないが、これらのAPIを使った時の始点は「現在の点の位置」になる。つまり、最後の描画操作における終点か、あるいはmoveToなどのAPIを使って指定した点である。

滑らかな曲線をベジエ曲線で近似する

さて、滑らかな曲線 \(f\colon[0,1]\to\mathbf{R}^2\) をベジエ曲線で近似するということを考えよう。動機としては例えば、プログラミングで曲線を描きたい時に、大抵のグラフィックスAPIには任意の曲線を描画するようなAPIはないので(2次か3次の)ベジエ曲線を使って近似する事になる。2次か3次と書いたが、以後3次のベジエ曲線で近似する事を考える。

続きを読む →

八元数について

2件の返信

最近、八元数を勉強しなければならないという電波を受信したので、とりあえず八元数のさわりだけ勉強する事にした。

複素数をさらに拡張したような数の体系として、八元数の前に四元数がある。四元数は3次元や4次元の回転（特殊直交行列; \(SO(3)\),\(SO(4)\)）と深い関わりがあるので、以前から（高校生の頃に）勉強して知っていた。四元数の積はノルムを保つため、単位四元数の積によって3次元球面 \(S^3\) にリー群の構造が入る。

八元数も、積がノルムを保つように定義されている。しかし積が結合的ではないため、群にはならない。いまいち勉強するモチベーションが起こらなかったのもその辺に理由がある気がする。

今参照している本はJohn H. ConwayとDerek A. SmithのOn Quaternions and Octonions: Their Geometry, Arithmetic, and Symmetryという本である。

複素数は1個(\(i\))、四元数は3個(\(i,j,k\))の直交する虚数単位があったが、八元数にはそれが7個ある。それを \(i_0,\dots,i_6\) で表す事にしよう。これに、「実数方向」の基底 \(1\) を加えると、八元数の \(\mathbf{R}\) 上線形空間としての基底 \(1,i_0,\dots,i_6\) ができる。

この基底を使うと、任意の八元数 \(x\) は次のように書ける:\[x=x_\infty+x_0i_0+x_1i_1+x_2i_2+x_3i_3+x_4i_4+x_5i_5+x_6i_6\]ただし、\(x_*\) は実数である。ノルムは普通の実数のノルム\[\left\lVert x\right\rVert^2=x_\infty^2+\sum_{n=0}^6 x_n^2\]とする。八元数の乗法をうまいこと定めてやると、2つの八元数 \(x\),\(y\) の積がノルムを保つ\[\left\lVert x\cdot y\right\rVert=\left\lVert x\right\rVert\cdot\left\lVert y\right\rVert\]ようにできる。どう定めるかというと、1以外の基底 \(i_n\) について\begin{align*}
i_n^2&=-1, \\
i_{n+1}i_{n+2}&=i_{n+4}=-i_{n+2}i_{n+1}, \\
i_{n+2}i_{n+4}&=i_{n+1}=-i_{n+4}i_{n+2}, \\
i_{n+4}i_{n+1}&=i_{n+2}=-i_{n+1}i_{n+4}
\end{align*}となるようにするらしい。ここで、\(n\) は整数を動き、添字は0から6に収まるように適宜 mod 7 で考える。

ということなのだが、この積の定義で本当にいいのか？本の記述を読み違えたとかいう可能性はないか？不安なので、積がノルムを保存することを確かめることにしよう。

続きを読む →

ベクトル束のテンソル積

1件のフィードバック

ベクトル束のテンソル積には2種類ある。

一つ目。\(E\to M\), \(F\to N\) をそれぞれ \(K\)-ベクトル束とする。このとき、\[\bigsqcup_{(x,y)\in{M\times N}} {E_x\otimes F_y}\]は \(M\times N\) 上のベクトル束となる。底空間は直積 \(M\times N\) となる。

二つ目。\(E\to M\), \(F\to M\) をそれぞれ \(K\)-ベクトル束とする。一つ目の場合は底空間が異なる場合も許したが、ここでは底空間は同じものを考えることに注意しよう。このとき、\[\bigsqcup_{x\in M} {E_x\otimes F_x}\]は \(M\) 上のベクトル束となる。底空間は \(M\) のままである。

最初に読んだ本では二つ目のやつを \(E\otimes F\) で表していたが、今読んでいる本は一つ目のやつを \(E\otimes F\) と書いて、二つ目のやつは \(E\mathop{\hat{\otimes}}F\) で書いていた。これに気づかないで読み進めたためにひどい目にあった（ちゃんと注意して読めという話だが）。

個人的には、二つ目の方を \(\otimes\) で書くのがいいかなあと思うが（この分野の最近の傾向を知らないのでアレだが）、じゃあ一つ目のテンソル積を書く必要があるときはどうするの、という話だ。どうしよう。

Five LemmaのダイアグラムチェースをするWebページを作った

コメントを残す

最近、Webの標準技術であるSVGとMathMLを組み合わせて、Webページ上で数学の図式などを表現できないかと考えている。

このブログでもたまに図式や証明図を載せているが、今までのは画像として貼り付ける形だった。静的なコンテンツならこれでもいいのだが、JavaScriptを使ってインタラクティブなコンテンツを作ろうとした時に、画像では動的に内容を変えるというようなことがやりにくい。そこで考えられるのが、Web標準技術のSVGやMathMLといった、HTMLやJavaScriptと相性のいい技術を使って数学の図式を記述するということである。

SVGは基本的に図を記述する言語で、MathMLは数式を記述する言語だが、ブラウザが対応していれば、SVGの図の中にMathMLを埋め込むことは難しくない。だが、数式の幅、高さを見ながら図のレイアウトを決めてやるのは正直楽しい作業ではない。JavaScriptを使えば、ブラウザがレンダリングした数式の大きさを見て適切に位置を合わせるということができるだろう。また、JavaScriptを使えば、ユーザーのクリックに反応して数式を変えたり、色を変えたりできるだろう。

SVGは最近のブラウザならだいたい対応しているが、MathMLのブラウザ側の対応はまちまちである。Firefoxはかなり昔からMathMLに対応していた。Safariは最近対応したようだが、筆者はあまり触っていない。Chromeは、数年前に見聞きした話では対応する意思がないらしい。

という感じで、とりあえず作る時はFirefoxで表示させることを優先させる。Safariは余力があれば対応させたい。Chromeは知らん。

というわけで、そういうのを実験的に実装してみた。このページは、みなさんお世話になっているであろう圏論的な直積の図式を表現している。

直積の図式を表示てきたはいいものの、これは動きがない。ユーザーの操作によって表示が変わるようなものを作ろう。というわけで、Five Lemmaのダイアグラムチェースによる証明(真ん中の射がmonicであることを示す)をするページを作った。クリックするとダイアグラムチェースが進む。かなりやっつけな書き方をしているので、例えばAndroid上のFirefoxでは表示が崩れた。Safariでは文字が途切れる。JavaScriptのソースコードもかなり汚い。改善の余地は大きいだろう。

演算子オーバーロードのないJavaScriptであまり複雑なことをしても記述性が悪い。例えばHaskellのような言語で記述してJavaScriptにコンパイルするという手順を取ると良いのかもしれない。

The middle 3×3 lemma

コメントを残す

先週に続いて、Categories for the Working MathematicianのAbelian Categoriesの章で勉強している。

ExercisesのThe middle 3×3 lemmaを証明しようとしたのだが、どうにも証明できそうにない。問題文曰く、上の図式の全ての列、それに第一行と第三行が短完全列ならば第二行も短完全列であることを証明せよ、だそうだ。与えられた短完全列の両端に0を付加すると次の図式になる。

手始めに、真ん中の行の2つの射を合成すると0となることを証明しようとしたが、どうにも方法が浮かばない。先週は勘違いでさんざん悩んだので、これはもしや成り立たないのではないか、と思って、調べてみることにした。（反例を考えるのは面倒くさかった）

手持ちの別の本を参照したところ、真ん中の行の2つの射を合成すると0となることは仮定しなければならないそうである。反例もあった。ググって出てきたnLabの項にも書かれていた。

アーベル圏を勉強している

コメントを残す

せっかく作ったブログをいつまでも放置するのもアレなので、最近勉強していることを書くことにする。

先学期の授業で登場したけど全然理解しないまま終わったホモロジーとかを理解したくて、どうせやるならと思ってアーベル圏の勉強をしている。本はCWMの、アーベル圏の章を進めている。

アーベル圏というのはどういう圏のことを言うのかというと、単純なものから順に定義を書いておくと

Preadditive category (前加法圏)

各 hom-set にアーベル群の構造が入っていて、射の合成が bilinear になっている圏を preadditive category という。CWMでは Ab-category と呼んでいる。

Kernel, cokernel や biproduct などの概念を定義することができる(kernel, cokernel は preadditive category でなくても、ゼロ射さえあれば定義できる)。

Additive category (加法圏)

Preadditive category であって、ゼロ対象と biproduct (直和) をもっている圏を additive category という。

Abelian category (アーベル圏)

Additive category であって、全ての射が kernel と cokernel を持っていて、全ての monic 射が kernel であり、全ての epi 射が cokernel である圏を abelian category という。

Abelian category では、射の image や coimage の概念を定義することができる。また、完全列の概念も定義できる。

…という風になる。

アーベル圏で完全列を定義できるということは、five lemma とか snake lemma を定式化できるということである。この辺のレンマの証明は、CWMではアーベル圏の章のセクション4に書かれている。

このセクションの最初の方にアーベル圏 A の短完全列の圏 Ses A が加法圏であるとさらっと書かれているが、最初に読んだときに Ses A もアーベル圏なんだと勘違いして証明を考えるのに数週間費やしてしまった。おかげで図式の扱いには慣れた気がするし、短完全列の射のカーネル、コカーネルがどうなるのかという話はスネークレンマに繋がってくるとはいえ、とんだ時間の浪費だった。

アーベル圏を勉強する前は、授業などでこれらの補題の証明にいわゆる “diagram chase” を使っているのを見て（加群の圏上ではあったが）、
「元を取ってdiagram chaseなんてしたら圏論的な証明にならないのでは！？」
と思っていたが、蓋を開けてみたら、一般のアーベル圏上で「元」に相当する概念を定義して、その「元」に対して monic や epi がそれぞれ普通の単射、全射と同じような振る舞いをすることを証明し、five lemma や snake lemma などの補題の証明では元を取って証明していたのだった。もちろん、圏論的な証明であるから、「dual を取って証明の半分を省略する」というようなことはできる。

Idrisで遊んでみた (2) — 自然数に関する命題の証明

コメントを残す

前回は等号の証明に使える公理や規則(Idrisの組み込み関数)をいくつか紹介した。

これに加え、Idrisの標準ライブラリには自然数の性質に関する補題(?)がいくつか用意されている。そのうち、後で使う2つを紹介する。

一つ目は、和と後続者に関するものである。ペアノ算術にはちょうどこのような公理があったはずだ。

もう一つは、和の可換性である。ペアノ算術ではこれを証明するためには帰納法を使うが、証明(関数の実装)は標準ライブラリで用意されているので、ここではそれを使うだけにとどめておく。

さて、前回証明したいと言っていた命題は\[x=y+\mathtt{difference}\ p\]であった。ただし、\(p\) の表す命題は \(y\le x\), Idrisの型で言うと LTE y x である。この等式を証明するには、
[sourcecode lang=”plain”]
differenceP : {x:Nat} -> {y:Nat} -> (p : LTE y x) -> (x = y + difference p)
[/sourcecode]
という型の関数を実装すれば良い。

例によって場合分けする。

\(y=0\), つまり p=lteZero の場合:
- この等式は自明に成り立つ。refl を返せば良い。
それ以外、つまり \(x=Sx’\), \(y=Sy’\), p=lteSucc p' の場合:
- 帰納法の仮定として differenceP p' : x' = y' + difference p' が使える。
- この仮定を使って S x' = (S y') + difference p' を示せば良い。(difference の定義を見れば difference p = difference p' なので、S x' = (S y') + difference p は自動的に導いてくれるようだ)
- この仮定と、先に紹介した公理、補題を使って、自然演繹っぽい証明図を書くと、となる。
- この証明図にIdrisの項を書き加えるととなる。ただし、一部をアンダースコアで省略している。

これらをまとめて、Idrisの式として書けば
[sourcecode lang=”plain”]
differenceP : {x:Nat} -> {y:Nat} -> (p : LTE y x) -> (x = y + difference p)
differenceP lteZero = refl
differenceP {x = S x’} {y = S y’} (lteSucc p’) = trans (trans (cong {f=S} (trans (differenceP p’) (plusCommutative _ _))) (plusSuccRightSucc _ _)) (plusCommutative _ (S y’))
[/sourcecode]
となる。一部の式をアンダースコアで省略しているが、最後の (S y') まで省略してしまうと処理系に怒られたので、そこは明示的に書いている。

今回は、自然演繹の証明図をCurry-Howard対応で翻訳することによって、命題を証明(関数を実装)した。等式の変形のところがやや煩雑になっているが、それはもとの自然演繹の証明図がそういうことになっていたことに起因するもので、Curry-Howard対応のせいでどうこうというものではない。

次回は量化子を含む命題を証明する予定である。Tacticを使った証明は筆者が不勉強なのでまだ扱わない。

Idrisで遊んでみた (1)

コメントを残す

前回はIdrisで2つの自然数を比較し、結果とその証明を返す関数 compareNats を作った。今回は、それに追加していくつかの関数を実装してみる。

まず、二つの自然数 \(x\) と \(y\) の差、\(x-y\) を計算する関数 difference を作る。\(y\le x\) の場合は良いが、\(x\lt y\) の場合はどうするか考えどころである。0を返すようにしてもよいが、ここは「\(y\le x\) であることの証拠を要求する」ことにして、\(x\lt y\) の場合は考える必要がない、という仕様にする。型を書けば
[sourcecode lang=”plain”]
difference : (x:Nat) -> (y:Nat) -> LTE y x -> Nat
[/sourcecode]
となる。前回書いたように、LTE y x は命題 \(y\le x\) に対応する型である。

実装には、例によって引数によるパターンマッチをする。

\(y=0\) の場合
- \(x\) を返す。第三引数は lteZero である。
- コードで書けば difference x 0 lteZero = x となる。
\(x=Sx’, \>y=Sy’\) の場合
- 第3引数は lteSucc p の形をしている。
- difference x' y' p によって \(x’-y’\) を計算できる。\(x-y=x’-y’\) なので、それをそのまま返せば良い。
- コードで書けば difference (S x') (S y') (lteSucc p) = difference x' y' p となる。

まとめると
[sourcecode lang=”plain”]
difference : (x:Nat) -> (y:Nat) -> LTE y x -> Nat
difference x 0 lteZero = x
difference (S x’) (S y’) (lteSucc p) = difference x’ y’ p
[/sourcecode]
となる。

さて、よく考えてみると、第1引数 x と第2引数 y の情報は第3引数の型を見れば自動的に得られる。したがって、第1引数と第2引数は省略できるのではないか？

Idrisにはimplicit argumentsという機能があるので、この場合実際に x と y を省略できる。Implicit argumentsを使うと、difference は次のように書ける:
[sourcecode lang=”plain”]
difference : {x:Nat} -> {y:Nat} -> LTE y x -> Nat
difference {x} lteZero = x
difference (lteSucc p) = difference p
[/sourcecode]

この difference という関数は、\(y \le x\) を満たす任意の自然数 \(x\), \(y\) および \(y \le x\) の「証拠」p : LTE y x に対して、\[x = y + \mathtt{difference}\>p\]という関係を満たす。この関係式を「証明」するにはどうすればよいだろうか？

その前に、述語論理における等号の公理と、それがIdrisではどうなっているか見ておこう。自然演繹チックに書けば、述語論理の等号の公理と関連する推論規則は