今回もMathematics In Lean 4の第8章 群と環 から8.1.3 部分群を読んでいます。
8.1.3のハイライトはラグランジュの定理です。
ラグランジュの定理：有限群の部分群の位数はもとの群の位数の約数である。
|G|=[G:G'] |G'| 、あるいは同じことだが、|G|=|G/G'| |G'|
ここにGはある有限群、G'はその部分群、| |は群の位数（集合の要素数）、[G:G']はGにおけるG'の指数、G/G'はG'によるGの左剰余類の集合。
多分高校生の頃にこの定理は知っていたと思うのですが、腹落ちして感動したのは大学に入ってからだったと思います。抽象的な代数構造に見える群の勉強を進めてきてこの定理を勉強すると唐突に数論的な概念である約数が登場するわけです。抽象的な代数構造に思いもよらない制約が入っているのだと知って感動した記憶があります（同じように感動したのは剰余環の位数が素数だと体になるというやつです）。
今回ラグランジュの定理の形式化と形式証明がわかるということで、大変な期待を持って勉強をしてきたのですが、、、その証明は次の１行で終わっていました。
example {G : Type*} [Group G] [Fintype G] (G' : Subgroup G) : card G' ∣ card G :=
⟨G'.index, mul_comm G'.index _ ▸ G'.index_mul_card.symm⟩
証明項で１行で終わっており、横向き黒三角記号 ▸ も登場して意味が分かりません。が、そこはVS Codeを使ってマウスオーバーで大体の意味は取れました。
G'.indexは[G:G']のことです。またG'.index_mul_cardは
card G = Subgroup.index H * card ↥H
のことでした。これはまさにラグランジュの定理の式と同じです。というわけで単に証明すべき定理を、証明済みの指数を使った式に書き換えただけで終わっているのだと思います。
一旦この証明項の理解を深めるのは止めて、mathlib4の中でラグランジュの定理がどうやって証明されているのかを探ってみました。ラグランジュの定理はSubgroup.card_subgroup_dvd_cardという名前のついた定理です。その証明を追っていくと分かったのは定理、
G ≃ (G ⧸ G') × ↥G'
がベースになっていることでした。剰余類の集合と部分群の直積はもとの群と同型になるという定理で、Subgroup.groupEquivQuotientProdSubgroupという名前がついています。ラグランジュの定理をこの定理を仮定して証明するのは簡単にできました。こんな感じです。
example {G : Type*} [Group G] [Fintype G] (G' : Subgroup G) : card G' ∣ card G := by
rw [dvd_def] -- ⊢ ∃ c, card G = card ↥G' * c
use G'.index -- ⊢ card G = card ↥G' * Subgroup.index G'
rw [mul_comm] -- ⊢ card G = Subgroup.index G' * card ↥G'
rw [Subgroup.index_eq_card] -- ⊢ card G = card (G ⧸ G') * card ↥G'
rw [← Fintype.card_prod] -- ⊢ card G = card ((G ⧸ G') × ↥G')
refine card_congr ?h.f -- ⊢ G ≃ (G ⧸ G') × ↥G'
exact Subgroup.groupEquivQuotientProdSubgroup
use G'.indexを使って「割り切れる」を掛け算にうまく変形すること、indexをcard (cardinality)に直すこと、掛け算を直積に直すこと、そしてrefineの行で十分条件としてG ≃ (G ⧸ G') × ↥G'を得ること、でゴールの式変形だけで証明できました。個人の感想としては、集合の直積が登場すればそれは要素の数の約数の話に繋がることがなるほどと思えました。
このG ≃ (G ⧸ G') × ↥G'のmathlib4での証明は読んでみたのですが、まだちゃんと理解できていません。色々と新しい技があるようでもう少しちゃんと勉強が必要そうです。
