My formalization project

Noboru Nawashiro

0.1 section1

Definition 1

✓

\(E_8\)格子とは，integralLatticeであって，even unimodularかつランクが\(8\)であるもののことである．

Theorem 2

2つの\(E_8\)格子\(\Lambda _1,\ \Lambda _2\)は同型である．

Proof ▶

sorry.

Definition 3

✓

\(E_8\)のCartan行列を\(M_0\)，それを1行ずつ行基本変形していき(その過程の行列を\(M_1, M_2, \ldots , M_6\)とする)上三角にしたものを\(M_7\)とする：

\begin{gather} M_0 := \begin{pmatrix} 2 & 0 & -1 & 0 & 0 & 0 & 0 & 0 \\ 0 & 2 & 0 & -1 & 0 & 0 & 0 & 0 \\ -1 & 0 & 2 & -1 & 0 & 0 & 0 & 0 \\ 0 & -1 & -1 & 2 & -1 & 0 & 0 & 0 \\ 0 & 0 & 0 & -1 & 2 & -1 & 0 & 0 \\ 0 & 0 & 0 & 0 & -1 & 2 & -1 & 0 \\ 0 & 0 & 0 & 0 & 0 & -1 & 2 & -1 \\ 0 & 0 & 0 & 0 & 0 & 0 & -1 & 2 \end{pmatrix},\\ M_7 := \begin{pmatrix} 2 & 0 & -1 & 0 & 0 & 0 & 0 & 0 \\ 0 & 2 & 0 & -1 & 0 & 0 & 0 & 0 \\ 0 & 0 & 3/2 & -1 & 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 5/6 & -1 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 & 4/5 & -1 & 0 & 0 \\ 0 & 0 & 0 & 0 & 0 & 3/4 & -1 & 0 \\ 0 & 0 & 0 & 0 & 0 & 0 & 2/3 & -1 \\ 0 & 0 & 0 & 0 & 0 & 0 & 0 & 1/2 \end{pmatrix}. \end{gather}

Lemma 4

✓

\(M_7\)は上三角である．

Proof ▶

略．

Lemma 5

✓

\(\det M_7 = 1\)である．

Proof ▶

補題 4より，\(M_7\)の行列式は対角成分たちの積であるから

\begin{equation} \det M_7 = 2 \cdot 2 \cdot (3 / 2) \cdot (5 / 6) \cdot (4 / 5) \cdot (3 / 4) \cdot (2 / 3) \cdot (1 / 2)\\ = 1. \end{equation}

Theorem 6

\(E_8\)のCartan行列の行列式は\(1\)である．

Proof ▶

補題 5より

\begin{equation} (\textrm{求める行列式}) = \det M_0 = \det M_1 = \cdots = \det M_7 = 1. \end{equation}

Definition 7

✓

\(B\)を\(E_8\)のCartan行列\(C (= M_0) \in \operatorname {M}_8(\mathbb {Z})\)から定まる双線型形式とする：

\begin{equation} B(x, y) := {}^t\! x C y = \left\langle x, Cy \right\rangle \qquad (\forall x, y \in \mathbb {Z}^8). \end{equation}

Lemma 8

✓

任意の\(x \in \mathbb {Z}^8\)に対し，次が成り立つ：

\begin{equation} \begin{split} B(x, x) ={}& 2 (x_0^2 + x_1^2 + x_2^2 + x_3^2 + x_4^2 + x_5^2 + x_6^2 + x_7^2\\ & - (x_0 x_2 + x_1 x_3 + x_2 x_3 + x_3 x_4 + x_4 x_5 + x_5 x_6 + x_6 x_7)) \end{split} \end{equation}

Proof ▶

内積の形にして，あとは具体的に計算：

\begin{equation} B(x, x) = \left\langle x, Cx \right\rangle = (\textrm{右辺}). \end{equation}

Lemma 9

✓

任意の\(x \in \mathbb {Z}^8\)に対し，平方完成すると次のようになる：

\begin{equation} \begin{split} B(x, x) ={}& \left( \sqrt{2} \, x_0 - \sqrt{\frac{1}{2}} \, x_2 \right)^2 + \left( \sqrt{2} \, x_1 - \sqrt{\frac{1}{2}} \, x_3 \right)^2 + \left( \sqrt{\frac{3}{2}} \, x_2 - \sqrt{\frac{2}{3}} \, x_3 \right)^2 \\ & + \left( \sqrt{\frac{5}{6}} \, x_3 - \sqrt{\frac{6}{5}} \, x_4 \right)^2 + \left( \sqrt{\frac{4}{5}} \, x_4 - \sqrt{\frac{5}{4}} \, x_5 \right)^2 + \left( \sqrt{\frac{3}{4}} \, x_5 - \sqrt{\frac{4}{3}} \, x_6 \right)^2 \\ & + \left( \sqrt{\frac{2}{3}} \, x_6 - \sqrt{\frac{3}{2}} \, x_7 \right)^2 + \frac{1}{2} \, x_7^2 \end{split} \end{equation}

Proof ▶

左辺に補題 8を代入して計算すれば得られる．

Theorem 10

✓

\(\forall x, y, z \in \mathbb {Z}^8,\ B(x+y, z) = B(x, z) + B(y, z)\).

Proof ▶

計算するだけ．

Theorem 11

✓

\(\forall x, y \in \mathbb {Z}^8,\ B(x, y) = B(y, x)\).

Proof ▶

計算するだけ．

Theorem 12

✓

\(\forall x \in \mathbb {Z}^8,\ B(x, x) \ge 0\).

Proof ▶

補題 9より，\(B(x, x)\)は平方の和で表せるから成り立つ．

Theorem 13

✓

\(\forall x \in \mathbb {Z}^8,\ B(x, x) = 0 \implies x = 0\).

Proof ▶

補題 9より，\(B(x, x)\)は平方の和で表せ，\(= 0\)とすると各項が\(0\)である．よって，最後の項に注目すると，\(x_7 = 0\)である．したがって，最後から2番目の項に注目すると，\(x_6 = 0\)である．これを繰り返すと，\(x_0 = \cdots = x_7 = 0\)を得る．

Theorem 14

✓

\(\forall x \in \mathbb {Z}^8,\ 2 \mid \left\langle x, x \right\rangle _{\mathbb {Z}}\).

Proof ▶

補題 8より従う．

Theorem 15

\(E_8\)格子はunimodularである．

Proof ▶

sorry.

Theorem 16

\(E_8\)格子は存在する．

Proof ▶

sorry.

Theorem 17

\(E_8\)格子\(\Lambda \)に対し，\(\forall n \in \mathbb {N},\ \# \left\lbrace x \in \Lambda \mathrel {} \middle | \mathrel {} B(x, x) = n \right\rbrace {\lt} \infty \).

Proof ▶

sorry.

Lemma 18

\(E_8\)格子\(\Lambda \)に対し，\(\# \left\lbrace x \in \Lambda \mathrel {} \middle | \mathrel {} B(x, x) = 2 \right\rbrace = 240\).

Proof ▶

sorry.