👋
ヨビノリ群論入門②をLean4で形式化 ~ 群の定義 ~
この記事について
以下のヨビノリの群論入門②をLean4で形式化していきます。
ヨビノリ群論入門をLean4で形式化の一つです。
Mathlibの実装を参考にしています。
おまじない
MyGroup.lean
-- 証明に「タクティク」を使うときに必要。
import Mathlib.Tactic
-- コンピュータでできない計算を扱うときに必要
-- 存在命題から存在している対象をとってくる、実数の割り算、etc...
-- 数学するならつけといて損はないと思います。
noncomputable section
群の定義
群はclassを用いて定義すると良いです。
MyGroup.lean
class MyGroup (G : Type*) where
op : G → G → G -- 群の演算
id_elem : G -- 群の単位元
inv : G → G -- 群の各元に(右)逆元を与える関数
op_assoc : ∀ a b c, op (op a b) c = op a (op b c) -- 演算の結合法則
op_e : ∀ a, op a id_elem = a -- 右単位元の性質
e_op : ∀ a, op id_elem a = a -- 左単位元の性質
op_inv : ∀ a, op a (inv a) = id_elem -- 右逆元の性質
classで定義することで、型Gに対して[MyGroup G]と書けば、Gが群の構造を持つことをLean側でよしなに考慮してくれます。
いちいちop、id_elem、invと書いていては面倒なので自分で記号を定義できます。
MyGroup.lean
infixl:70 " ⋆ " => MyGroup.op -- 左結合の中置記法、優先順位70
notation "e" => MyGroup.id_elem -- 単位元の記法
postfix:max "⁻¹" => MyGroup.inv -- 逆元の後置記法
classを作ってそのクラスに関する性質を証明していくとき、通常class名と同じ名前空間で作業すると整理の観点から良いです。
MyGroup.lean
namespace MyGroup
これ以降、型の変数Gは群の構造を持つことにしましょう。
MyGroup.lean
variable {G : Type*} [MyGroup G]
定義に入ることも多い、右逆元が左逆元にもなることを示していきます。
MyGroup.lean
theorem inv_op : ∀ a : G, a⁻¹ ⋆ a = e := by
intro a
calc
a⁻¹ ⋆ a = (a⁻¹ ⋆ a) ⋆ e := by rw [op_e]
_ = (a⁻¹ ⋆ a) ⋆ ((a⁻¹ ⋆ a) ⋆ (a⁻¹ ⋆ a)⁻¹) := by rw [op_inv]
_ = a⁻¹ ⋆ (a ⋆ a⁻¹) ⋆ a ⋆ (a⁻¹ ⋆ a)⁻¹ := by simp only [op_assoc]
_ = a⁻¹ ⋆ e ⋆ a ⋆ (a⁻¹ ⋆ a)⁻¹ := by rw [op_inv]
_ = a⁻¹ ⋆ a ⋆ (a⁻¹ ⋆ a)⁻¹ := by rw [op_e]
_ = e := by rw [op_inv]
群の具体例
instanceを生成することでclassの構造を持つ具体例を作ることができます。
MyGroup.lean
-- (ℝ, +)が群である
instance : MyGroup ℝ where
op a b := a + b
id_elem := 0
inv a := -a
op_assoc a b c := add_assoc a b c
op_e a := add_zero a
e_op a := zero_add a
op_inv a := add_neg_cancel a
このinstanceを生成したことで、ℝとその演算+にMyGroupの性質を適用することができるようになります。
MyGroup.lean
-- instanceを作っておけば、MyGroupの定理inv_opをℝにも使える
example (a : ℝ) : -a + a = 0 := inv_op a
動画中の他の例もinstanceを生成してみます。(未完)
かなりの部分をsimpタクティクのブラックボックスに託していますが...
MyGroup.lean
instance : MyGroup ℤ where
op a b := a + b
id_elem := 0
inv a := -a
op_assoc a b c := add_assoc a b c
op_e a := add_zero a
e_op a := zero_add a
op_inv a := add_neg_cancel a
instance : MyGroup {x : ℝ // x ≠ 0} where
op a b := ⟨a.val * b.val, mul_ne_zero a.prop b.prop⟩
id_elem := ⟨1, one_ne_zero⟩
inv a := ⟨1 / a.val, by (simp; exact a.prop)⟩
op_assoc a b c := by simp; exact mul_assoc a.val b.val c.val
op_e a := by simp
e_op a := by simp
op_inv a := by simp; exact mul_inv_cancel₀ a.prop
instance : MyGroup {z : ℂ // ‖z‖ = 1} where
op a b := ⟨a.val * b.val, by
rw [norm_mul, a.prop, b.prop, mul_one]
⟩
id_elem := ⟨1, norm_one⟩
inv a := ⟨1 / a.val, by simp; exact a.prop⟩
op_assoc a b c := by simp; exact mul_assoc a.val b.val c.val
op_e a := by simp
e_op a := by simp
op_inv a := by
simp
have : a.val ≠ 0 := by
intro ha
have : ‖a.val‖ = 0 := by rw [ha]; exact norm_zero
rw [a.prop] at this
exact one_ne_zero this
exact mul_inv_cancel₀ this
instance : MyGroup {x // x = 1} where
op a b := ⟨a.val * b.val, by rw [a.prop, b.prop, one_mul]⟩
id_elem := ⟨1, rfl⟩
inv a := ⟨1 / a.val, by rw [a.prop]⟩
op_assoc a b c := by simp; rw [a.prop, b.prop, c.prop]
op_e a := by simp;
e_op a := by simp;
op_inv a := by
simp
constructor
· exact a.prop
· rw [a.prop]
rfl
{~ // ~}の形はSubtypeと呼ばれるものです。2つ目の例で言えば、集合ℝ \ {0}が群であることを言いたいのですがこれは以下の理由で無理です。
- 今、MyGroupは型変数に対して定義されているので、集合に群の構造を持たせることはできない
- Leanの言葉で言えばℝは型なので、差集合
\を考えることがそもそもできない
これを解決するのがSubtypeという集合を無理やり型にしたようなもので、{x : ℝ // x ≠ 0}は、実数であり0でないものが属する型です。ただし、実際に属しているのは(実数のデータval, valが0でない証明prop)の組になっています。
可換群の定義
よくあるプログラミング言語と同様、classを拡張することができます。MyGroupを拡張して可換群AbelianGroupを定義します。
MyGroup.lean
class MyAbelianGroup (G : Type*) extends MyGroup G where
op_comm : ∀ a b : G, a ⋆ b = b ⋆ a
群の基本的な性質を証明
単位元、逆元の一意性
左単位元の一意性は「a ⋆ b = bが成り立つならばa = eである」と表現されます。よって、Lean4では以下のように表現、証明できます。
MyGroup.lean
theorem left_e_unique (a b : G) (h : a ⋆ b = b) : a = e := by calc
a = a ⋆ b ⋆ b⁻¹ := by rw [op_assoc, op_inv, op_e]
_ = b ⋆ b⁻¹ := by rw [h]
_ = e := by rw [op_inv]
右単位元も同様です。
MyGroup.lean
theorem right_e_unique (a b : G) (h : a ⋆ b = a) : b = e := by calc
b = a⁻¹ ⋆ (a ⋆ b) := by rw [← op_assoc, inv_op, e_op]
_ = a⁻¹ ⋆ a := by rw [h]
_ = e := by rw [inv_op]
左逆元の一意性は「a ⋆ b = eが成り立つならばa = b⁻¹である」と表現されます。よって、Lean4では以下のように表現、証明できます。
MyGroup.lean
theorem left_inv_unique (a b : G) (h : a ⋆ b = e) : a = b⁻¹ := by calc
a = a ⋆ b ⋆ b⁻¹ := by rw [op_assoc, op_inv, op_e]
_ = e ⋆ b⁻¹ := by rw [h]
_ = b⁻¹ := by rw [e_op]
右逆元も同様です。
MyGroup.lean
theorem right_inv_unique (a b : G) (h : a ⋆ b = e) : b = a⁻¹ := by calc
b = a⁻¹ ⋆ (a ⋆ b) := by rw [← op_assoc, inv_op, e_op]
_ = a⁻¹ ⋆ e := by rw [h]
_ = a⁻¹ := by rw [op_e]
逆元の逆元、演算結果の逆元
逆元の逆元が自分自身であることはLean4で以下のように表現、証明できます。
MyGroup.lean
theorem inv_of_inv (a : G) : (a⁻¹)⁻¹ = a := by calc
a⁻¹⁻¹ = a ⋆ a⁻¹ ⋆ a⁻¹⁻¹ := by rw [op_inv, e_op]
_ = a ⋆ e := by rw [op_assoc, op_inv]
_ = a := by rw [op_e]
演算結果の逆元が、それぞれの逆元の、順番を入れ替えた演算結果になっていることはLean4で以下のように表現、証明できます。
MyGroup.lean
theorem inv_of_op (a b : G) : (a ⋆ b)⁻¹ = b⁻¹ ⋆ a⁻¹ := by
have : (a ⋆ b) ⋆ (b⁻¹ ⋆ a⁻¹) = e := by calc
(a ⋆ b) ⋆ (b⁻¹ ⋆ a⁻¹) = a ⋆ (b ⋆ b⁻¹) ⋆ a⁻¹ := by simp only [op_assoc]
_ = a ⋆ a⁻¹ := by rw [op_inv, op_e]
_ = e := by rw [op_inv]
exact (right_inv_unique (a ⋆ b) (b⁻¹ ⋆ a⁻¹) this).symm
参考文献
Discussion