今回もMathematics In Lean 4の第8章 群と環 から8.1.3 部分群を読んでいます。前回の記事でラグランジュの定理「有限群の元の個数は部分群の源の個数で割り切れる」をLean4で形式証明しました。
証明の肝はSubgroup.groupEquivQuotientProdSubgroupという長い名前の定理です。定理の内容は次の式です。
G ≃ (G ⧸ G') × G'
ここでGは群、G'はその部分群です。G⧸G'はGをG'で割った商集合（同値類の集合）です。×は群の直積、≃は群同型です。
意味は群はその部分群で割った商集合と部分群の直積に同型である、ということです。
この定理の証明なんですが、思ったよりも難しく、全てのステップを追いきれていません。今回は大筋を説明したいと思います。将来詳細が追い切れたらまた別に記事を書くかもしれません、、、（挫折するかもですが、、、）
Mathlib.GroupTheory.Cosetの中をみると以下のような証明を見ることができます。以下でG=α, G'=sです。
noncomputable def groupEquivQuotientProdSubgroup : α ≃ (α ⧸ s) × s :=
calc
α ≃ ΣL : α ⧸ s, { x : α // (x : α ⧸ s) = L } := by
exact (Equiv.sigmaFiberEquiv fun (x: α) => (x : α ⧸ s)).symm
_ ≃ ΣL : α ⧸ s, (Quotient.out' L • s : Set α) := by sorry
_ ≃ Σ _L : α ⧸ s, s := by sorry
_ ≃ (α ⧸ s) × s := by sorry
calcで同値変形して証明しています。各ステップの証明はここでは省略してsorryにして、流れが見えるようにしてあります。
個人的にはcalcの最初のステップα ≃ ΣL : α ⧸ s, { x : α // (x : α ⧸ s) = L }は重要だと思います。各ステップはLが商集合（同値類の集合）を動く時の総和の形になっています。最初のステップで総和の形に変形しています。とはいっても各同値類についてそこに含まれる元を全部集めると元の集合になる、という（当たり前と言えば当たり前の）定理Equiv.sigmaFiberEquivがmathlib4にあり、それを群と部分群の場合に適用すれば最初のステップの証明はほぼ明らかです。
２番目のステップ
ΣL : α ⧸ s, { x : α // (x : α ⧸ s) = L }≃ ΣL : α ⧸ s, (Quotient.out' L • s : Set α)
は、結構たくさんの記号を理解する必要があります。目立つところでは左辺の{}の中でx : αと書きながらすぐにx : α ⧸ sと書いてあり？？？な感じですよね。これはx : α ⧸ sが強制型変換で、x : αを、xを含む同値類に変換しています。確かにユニークに定まるしいいんですが、それも型変換なんですね。
また右辺のQuotient.out' Lは同値類Lから元を１つ取り出す関数です。いわゆる代表元を取り出しているのですが、Lは有限とは限らずそこから適当に選ぶので選択公理をつかっているそうです。
右辺の• は代表元と部分群sの要素を個別に群演算した結果の集合です。つまり２番目のステップの右辺は同値類の代表元をa,b,c,...としたときα = a s + b s + c s + ...などと直和で書きますがそれを総和で書いたものです。
３番目ステップ
ΣL : α ⧸ s, (Quotient.out' L • s : Set α)≃ Σ _L : α ⧸ s, s
は代表元と部分群の積の直和を同値類でインデックスされた部分群sの和として変形します（残念ながらここはちゃんと分かってはいません）。
４番目のステップ
Σ _L : α ⧸ s, s ≃ (α ⧸ s) × s
で最終形に辿り着き証明が終わります。インデックスされた部分集合の和はインデックスの集合と部分集合の積になる、という定理を使っています。
それぞれのステップは言葉で説明するとふんわりとしていてダメな感じですね。とは言っても各ステップの形式証明がよく分からず今のところ理解するのは挫折中です。個人的にはもう少し泥臭く、G と (G ⧸ G') × G'の間に写像を構成して、それが全単射でかつ準同型（つまり同型）になっていることを示す方が簡単なのではないか、と考えています。
