Mathematics In Lean 4の第8章 群と環 に進みます。第8章ではこれらの代数構造について部分集合や代数構造間の写像をLean4で表現する方法を学びます。代数構造としてはより単純なモノイドも扱います。演算の言葉として加法や乗法が出てきますが、主に記号の違いと思ってください。
今回は8.1 モノイドと群を読んでいきます。
以下の代数構造はすでにLean4 / Mathlibに定義されていてすぐに使えます。
Monoid, addMonoid, addCommMonoid
Group, addGroup, addCommGroup
Commがつけば可換、addがつけば加法群です。加法は可換が仮定されることが多く、可換でない場合は乗法を使うことが多いため、この中でもMonoid, addCommMonoid, Group, addCommGroupをよく使うそうです。
例えば可換加法群でx+y=y+xが成り立つことを証明することができます。
example {M : Type*} [AddCommGroup M] (x y : M) : x + y = y + x := add_comm x y
一般的には可換群では演算が可換であることは公理ですが、Lean 4ではちょっとだけ違います。VSCodeでadd_commにマウスを重ねてみるとわかりますが、add_commはAddCommMagmaという代数構造の性質です。つまりAddCommGroupはAddCommMagmaであること、AddCommMagmaではadd_commが成り立つことから証明できるわけです。
乗法群にはgroup, 可換加法群にはabelというタクティクがあります。群の要素の演算式の計算による証明を簡単に行えます。ここでは可換加法群で成り立つ計算式を証明してみます。
example {M : Type*} [AddCommGroup M] (x y z: M) : x + y - z = x - z - x + y + x := by abel
まあ、あっけないですね。
さて代数構造の間には同型写像、準同型写像などの構造をある程度保存する写像が定義されて、多くの定理が証明されています。この写像をここではmorphismと呼び日本では「射」を使います。圏論っぽい雰囲気を感じる人もいるかもしれませんが、ここではとりあえず普通の数学です。
Lean4ではfが群Gから群Hへの射であることをf : G →* Hと書きます。普通の関数はf : G → Hと書きますが、違いは構造の保存です。f : G →* Hなるfについて（乗法群の記法で書けば）f 1 = 1, f a*b = (f a) * (f b)は自動的に使えることになります。同じことですが、可換加法群では射をf : G →+ Hと書きます。
群のGの元xの逆元x⁻¹は射f : G →* Hでf xの逆元(f x)⁻¹に写ることを証明できます。
example {G H : Type*} [Group G] [Group H] (x : G) (f : G →* H) : f (x⁻¹) = (f x)⁻¹ :=
f.map_inv
この証明ではすでにLean4/Mathlibで証明済みの事実を持ってきただけですが、自分で頑張って証明することもできます。
example {G H : Type*} [Group G] [Group H] (x : G) (f : G →* H) : f (x⁻¹) = (f x)⁻¹ := by
have : f (x⁻¹) * (f x) = 1 := calc
f (x⁻¹) * (f x) = f ((x⁻¹) * x) := by exact (MonoidHom.map_mul f x⁻¹ x).symm
_= f 1 := by
refine (FunLike.congr_arg f ?h₂).symm
exact (mul_left_inv x).symm
_= 1 := by exact MonoidHom.map_one f
exact eq_inv_of_mul_eq_one_left this
証明の中でMonoidHom.map_mulはf (a*b) = (f a)*(f b)のことであり、MonoidHom.map_oneはf 1 = 1のことです。流れとしては補題 f (x⁻¹) * (f x) = 1 を証明し、最後に「a*b=1ならばb=a⁻¹」でQ.E.Dです。
今回はここまでとして、次回は部分群について勉強します。
