Mathematics In Lean 4の第8章 群と環 に進みます。今回は8.1.3 部分群を読んでみます。
あるタイプAの元の集合が群をなすことを示すにはGroup A、Aの元の集合の部分集合がAの演算で群をなす（部分群になる）ことを示すにはSubgroup Aと書きます。演算が加法である場合にはAddSubgroup Aと書けば良いです。
Mathematics In Lean 4では例として整数のなす群が有理数のなす群の加法に関する部分群であることを示します。このためには４つのことを示す必要があります。
1. 整数の集合が有理数の集合の部分集合であること
2. 整数の集合が加法で閉じていること
3. 整数の集合に加法の単位元0が含まれること
4. 整数の集合に加法の逆元がふくまれること
ところがLean 4では整数の集合は有理数の集合の直接的には部分集合ではありません。ここでは整数は自然に有理数とみなせることを利用した整数から有理数への強制型変換関数↑を用います。この関数の定義域を整数の集合とした時、値域は整数に対応する有理数の集合なのでその元を整数とみなすことにします。これで有理数の中の整数を取り出すことができました。
example : AddSubgroup ℚ where
carrier := Set.range ((↑) : ℤ → ℚ)
add_mem' := by sorry // 加法で閉じていることの証明
zero_mem' := by sorry // 0が含まれることの証明
neg_mem' := by sorry // 加法の逆元が含まれることの証明
上記で、carrierには整数を強制型変換して作ったℚの部分集合が指定されています。
add_mem', zero_mem' neg_mem'はそれぞれ群が満たすべき条件2, 3, 4です。それぞれが満たされていることの証明は本書をみてください。
１つ自分でも部分群を作って証明したくなりますよね。偶数が整数の加法部分群であることを示してみましょう。より詳しくは、整数の中の2の倍数からなる部分集合は加算で群をなし整数の部分群となることを示してみましょう。こんな感じです。
example : AddSubgroup ℤ where
carrier := Set.range ((fun x:ℤ => x*2) : ℤ → ℤ )
add_mem' := by
intro a b ha hb
rcases ha with ⟨ aa, ha⟩
simp at ha
rcases hb with ⟨ bb, hb⟩
simp at hb
use aa + bb
simp
ring_nf
rw [ha,hb]
zero_mem' := by
use 0
simpneg_mem' := by
intro n h1
rcases h1 with ⟨ nn, h1⟩
simp at h1
use -nn
simp
exact h1
carrierには与えられた引数を２倍する無名関数の値域（つまり偶数の集合）を集合として指定してます。この値域に含まれる元a, bに対して、２倍するとa, bになる整数aa, bbが必ず見つかります。このaa, bbを足したaa+bbを２倍するとa+bになるため、a+bは２の倍数の集合に含まれる、というのがadd_mem'に書かれている証明の流れです。
zero_mem', neg_mem'の証明は短いですし、ぜひVSCodeで試してみてください。
