概要

群論の初歩、特に群の定義とそれを弱められること、また、単位元・逆元の一意性についてLeanという定理証明支援系を使って、実装例を示しながら紹介します。

群とは

群とは、集合に対して良い性質を持った演算が定義されたもので、歴史的には代数方程式の解の研究に遡ります。5次方程式が加減乗除と根号による解の公式を持たないことは広く知られていますが、これは群論が基礎となっているガロア理論によって証明されています。
また、群は対称性の構造を記述するともいわれ、物理学や化学など広く応用があります。

Leanとは

Leanは、数学の定理証明支援が可能なプログラミング言語の一つで、2024年現在の最新バージョンがLean4です。複雑な数学の定理はしばしば証明の妥当性を検証することが困難ですが、定理証明支援系を用いるとコードのコンパイルが通ることをもって、定理の正当性を検証することができます。

環境構築

以下に従い、VS Codeの拡張機能を利用してLeanをインストールしてください。

また、LeanではMathlibと呼ばれる基本的な数学の定義や定理をまとめたライブラリが存在します。以下に従い、Mathlibを依存に追加して新規プロジェクトを作成してください。

群に関してもライブラリ内で実装されていますが、練習のため以下で最低限必要なものだけimportしたうえで独自に定義していきます。

import Mathlib.Tactic

namespace Example

end Example

ライブラリ内の定義と重複しないように適当なnamespaceを用意しその中に定義や定理を記述していきます。

群の定義

$X$を集合としたとき、写像$\phi:X×X→X$を$X$上の演算といいます。以下では$\phi(a,b)$を$a*b$と書きます。

$G$を空でない集合とし、$G$上の演算が定義され、以下の性質を満たすとき$G$を群といいます。

（単位元の存在）
単位元 $1 \in G$が存在し、任意の$a \in G$に対し、$1 * a = a * 1 = a$を満たす。
（逆元の存在）
任意の$a \in G$に対し、逆元 $a^{-1} \in G$が存在し、$a^{-1} * a = a * a^{-1} = 1$を満たす。
（結合法則）
任意の$a, b, c \in G$に対し、$(a * b) * c=a * (b * c)$を満たす。

また、任意の$a \in G$に対し、$1 * a = a$を満たす$1$を左単位元、$a^{-1} * a = 1$を満たす$a^{-1} \in G$を左逆元といいます。右単位元、右逆元も同様に定義します。

例えば、実数全体は通常の加法を演算として群となります。単位元は$0$、$a$の逆元は$-a$となります。また、$n$次正則行列全体は行列の積を演算として群となります。単位元は単位行列、逆元は逆行列となります。

一般的に群は上のように定義されますが、実は右単位元、右逆元の条件は他の条件から導けるため除くことができます。どのように導けるかは後に示しますが、まずはこれらの条件を除いた定義に基づいてLeanでの実装例を示します。

-- 群の定義
class Group (G : Type) where
  mul : G → G → G
  one : G
  inv : G → G
  mul_assoc : ∀ a b c : G, mul (mul a b) c = mul a (mul b c)
  one_mul : ∀ a : G, mul one a = a
  mul_left_inv : ∀ a : G, mul (inv a) a = one

-- 群Gを作成
variable [Group G]

群の構造をGroupというクラスによって定義します。
G　:　TypeでGが集合であることを表します。

mul
G上の演算、すなわちGの２つの元の組に対してその積を返す写像が定まっていることを表します。
Leanでは、Gの元に対してGからGへの写像を返す写像と解釈し、G　→　(G　→　G)のように書きます。上の実装では、()を省略して、G　→　G　→　Gとしています。
one
Gの単位元oneが存在することを表します。
inv
Gの各元に対してその逆元が存在することを表します。
Leanでは、Gの元に対してGの元を返す写像と解釈し、G→Gのように書きます。

さらに以下で、上記の二項演算、単位元、逆元が満たすべき条件を記述します。

mul_assoc
結合法則を満たすことを表します。
one_mul
oneが左単位元の条件を満たすことを表します。
mul_left_inv
inv aが左逆元の条件を満たすことを表します。

Leanによる証明の例

群の定義ができたところで、Leanによる証明の例を見ていきます。
まずは、群の定義をそのまま使って結合法則、左単位元、左逆元の性質を証明します。

-- 群の定義を使った証明
example (a b c : G) : Group.mul (Group.mul a b) c = Group.mul a (Group.mul b c) :=
  Group.mul_assoc a b c

example (a : G) : Group.mul Group.one a = a :=
  Group.one_mul a

example (a : G) : Group.mul (Group.inv a) a = Group.one :=
  Group.mul_left_inv a

exampleで証明の例であることを表し、変数と証明したい式を記述します。
証明は:=に続けて記述します。上記ではでは群の定義をそのまま利用することを表しています。

上の証明でも問題ありませんが、わざわざ積をmul a b、単位元をone、逆元をinv aと記述するのは煩わしいです。そこで、代わりに*, 1, ⁻¹の記号を使えるようにします。

-- *, 1, ⁻¹の記号を使う準備
instance : Mul G := ⟨Group.mul⟩
instance : One G := ⟨Group.one⟩
instance : Inv G := ⟨Group.inv⟩

-- 群の定義を使った証明
theorem mul_assoc (a b c : G) : a * b * c = a * (b * c) :=
  Group.mul_assoc a b c

theorem one_mul (a : G) : 1 * a = a :=
  Group.one_mul a

theorem mul_left_inv (a : G) : a⁻¹ * a = 1 :=
  Group.mul_left_inv a

同じ主張がかなり見やすくなりました。これらは後に使うためexampleの代わりにtheoremとして名前をつけておきます。

右単位元、右逆元

さて、ここまでは群の定義から直ちに分かるつまらない証明の例でした。
以下では、上で証明した定理を組み合わせて群の定義が弱められること、すなわち右単位元、右逆元の条件は他の条件から導けることを示します。

まずは右逆元の条件を示します。

-- a⁻¹はaの右逆元
theorem mul_right_inv (a : G) : a * a⁻¹ = 1 := by
  calc
    a * a⁻¹ = 1 * (a * a⁻¹) := by
      rw [one_mul]
    _ = (a * a⁻¹)⁻¹ * (a * a⁻¹) * (a * a⁻¹) := by
      rw [← mul_left_inv (a * a⁻¹)]
    _ = (a * a⁻¹)⁻¹ * (a * (a⁻¹ * a * a⁻¹)) := by
      rw [mul_assoc, mul_assoc, ← mul_assoc a⁻¹]
    _ = (a * a⁻¹)⁻¹ * (a * a⁻¹) := by
      rw [mul_left_inv, one_mul]
    _ = 1 := by
      rw [mul_left_inv]

一般に、群では交換法則a　*　b　=　b　*　aを仮定しないため、左逆元の条件から右逆元の条件が直ちに分かるわけではないことに注意してください。

calcと書くと、等号をつなげて式変形する形で証明を記述することができます。各式変形で使った定理は、:=　byの後に記述します。

rwはrewriteを意味し、定理を用いて式変形することを表します。例えば、rw [one_mul]は、上で示したone_mulの1 * a = aを用いて式変形することを表しています。

←は、定理の式を右から左に利用することを表し、定理の名前の後には定理への入力を記述することもできます。例えば、rw [← mul_left_inv (a * a⁻¹)]は、mul_left_invのa⁻¹* a = 1におけるaとして(a * a⁻¹)を使って、1を(a * a⁻¹)⁻¹ * (a * a⁻¹)に書き換えることを表します。

右逆元の条件が示されると、1が右単位元であることを示すのは難しくありません。

-- 1は右単位元
theorem mul_one (a : G) : a * 1 = a := by
  calc
    a * 1 = a * (a⁻¹ * a) := by
      rw [← mul_left_inv a]
    _ = a * a⁻¹ * a := by
      rw [← mul_assoc]
    _ = 1 * a := by
      rw [mul_right_inv]
    _ = a := by
      rw [one_mul]

単位元と逆元の一意性

最後に、単位元と逆元の一意性も確認しておきます。
上の実装では少なくとも1つ存在を仮定した単位元を1と表していましたが、もし単位元の条件を満たすGの元eが存在するとすればそれは1に他ならないことを示します。

-- 単位元の一意性
theorem one_unique (e : G) (h : ∀ a : G, e * a = a) : e = 1 := by
  calc
    e = e * 1 := by
      rw [mul_one]
    _ = 1 := by
      rw [h 1]

rwでは定理の仮定を利用することもできます。
例えば、rw [h 1]は、定理の仮定hに1を入力したものを使って式変形することを表します。

Gの各元bに対し、少なくとも1つ存在する逆元はb⁻¹と表していましたが、もし逆元の条件を満たすGの元aが存在するとすればそれはb⁻¹に他ならないことを示します。

-- 逆元の一意性
theorem inv_unique (a b : G) (h : a * b = 1) : a = b⁻¹ := by
  calc
    a = a * 1 := by
      rw [mul_one]
    _ = a * (b * b⁻¹) := by
      rw [← mul_right_inv b]
    _ = a * b * b⁻¹ := by
      rw [← mul_assoc]
    _ = 1 * b⁻¹ := by
      rw [h]
    _ = b⁻¹ := by
      rw [one_mul]

参考文献