ガウス整数とユークリッド整域 - Maxima で綴る数学の旅

ちょっとだけ環論の基礎の復習です。

可換環とは加法と乗法が定義されており、それぞれの単位元が0, 1であり、どちらもどちらも可換、かつ分配法則が成り立つ集合です。

整域とは零因子のない可換環でかつ自明でない環です。

$a, b$が零因子とは$a\ne 0, b\ne 0, a\,b=0$となるような$a,b$のことでした。また環が自明とは$0=1$が成り立つことでした。

ユークリッド整域($R$)とは整域でかつ除法の原理を満たすノルムと呼ばれる関数$f:R\rightarrow \mathbb{N}$が定義されていることをいう。

除法の原理：$a=b\,q+r, f(r)\lt f(a)$。

ガウス整数はユークリッド整域になります。すでにガウス整数が自明でない可換環になることは証明済みです。したがって整域であること、ノルムが定義できることを示せば「お仕事お仕舞い」となります。

Mathematics in Lean 4の「6.3 ガウス整数を構成する」ではまずガウス整数のノルムを定義し、また割り算と余りを求める演算を定義します。そしてこれらが除法の原理を満たすことを証明します。

ガウス整数がユークリッド整域になり、ユークリッド整域で成り立つ全ての定理が同様に成り立つことを次のようにして示します。前回と同様に証明のテンプレートを表示します。まず、

instance : EuclideanDomain gaussInt :=_

と入力するとエディタがヒントボタンを表示するのでクリックして、テンプレートの生成を選択します。これでEuclideanDomainが持つべき演算とその間に成り立つ必要のあるすべての制約がテンプレートとして生成されます。

instance : EuclideanDomain gaussInt where
add := _
add_assoc := _
zero := _
zero_add := _
add_zero := _
...
quotient := _
quotient_zero := _
remainder := _
quotient_mul_add_remainder_eq := _
r := _
r_wellFounded := _
remainder_lt := _
mul_left_not_lt := _

最初の部分はgaussIntが可換環(commRing)であることを示す際に表示された演算です。この前半の部分はもう一度可換環であることを示す必要はなくて、次のように書くことで、これらの前半の可換環の部分は証明済みにすることができます。

instance : EuclideanDomain gaussInt :=
{ gaussInt.instCommRing with
quotient := _
quotient_zero := _
remainder := _
quotient_mul_add_remainder_eq := _
r := _
r_wellFounded := _
remainder_lt := _
mul_left_not_lt := _ }

上記のquotient以下の部分がEuclideanDomainで固有の演算と制約になります。あれ、ノルムがない！と思った方、鋭いです。ガウス整数$a+b\,i$についてノルムを$a^2+b^2$で定義すると除法の原理を満たすことが証明できます。除法の原理はちょっと一般化されています。$r a b$という関係がおおむね$a<b$に対応しており、rが整列順序であることで定義されています。

すでにガウス整数のノルムの定義やそこで成り立つ定理が示してありますから、それらを使って上記の'_'を全て埋めれば証明終了となり、めでたくガウス整数がユークリッド整域になることが分かりました。'_'が全て埋まったコードは以下の通りです。

instance : EuclideanDomain gaussInt :=
{ gaussInt.instCommRing with
quotient := (· / ·)
remainder := (· % ·)
quotient_mul_add_remainder_eq :=
fun x y ↦ by simp only; rw [mod_def, add_comm, sub_add_cancel]
quotient_zero := fun x ↦ by
simp [div_def, norm, Int.div']
rfl
r := (measure (Int.natAbs ∘ norm)).1
r_wellFounded := (measure (Int.natAbs ∘ norm)).2
remainder_lt := natAbs_norm_mod_lt
mul_left_not_lt := not_norm_mul_left_lt_norm }

ここではrやr_wellFoundedの証明が見慣れない雰囲気です。とはいえガウス整数の割り算と余りの関係からこれらを長いけれども見慣れた感じで証明するのもそれほど難しくはなさそうです。

なるほど、こうやって構造体を使って関係性の証明やそれをシステムに登録して一連の定理を使えるようにすること出来るようになりました。例えばガウス整数では既約元と素元は一致することが直ちにわかります。