Lean4 によるラグランジュの定理の証明
Last active
August 25, 2025 19:38
-
-
Save lotz84/ec6de49bfb11e8e64f9b7b14d4733e82 to your computer and use it in GitHub Desktop.
Lean4 によるラグランジュの定理の証明
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- メモ1： | |
| -- 有限群を定義するために mathlib4 の有限であることを表す型クラス Fintype を利用する | |
| -- Fintype はイデアル類群の位数が有限であることの証明にも使われている(Mathlib.NumberTheory.ClassNumber.Finite) | |
| -- Fintype の定義は以下の通り | |
| -- ``` | |
| -- class Fintype (α : Type*) where | |
| -- elems : Finset α | |
| -- complete : ∀ x : α, x ∈ elems | |
| -- ``` | |
| -- つまり Fintype は、要素を表す有限集合 elems と | |
| -- elems に型 α の項がすべて含まれていることの証明 complete から成る | |
| -- また Finset の定義は以下の通り | |
| -- ``` | |
| -- structure Finset (α : Type*) where | |
| -- val : Multiset α | |
| -- nodup : Nodup val | |
| -- ``` | |
| -- つまり Finset は、要素を表す有限多重集合 val と | |
| -- val に要素の重複がないことの証明 nodup から成る | |
| -- また Multiset の定義は以下の通り（u はユニバースを表す変数） | |
| -- ``` | |
| -- def Multiset (α : Type u) : Type u := Quotient (List.isSetoid α) | |
| -- ``` | |
| -- Quotient は商型を表し List.isSetoid は並び替え(Permutation)による同値関係を表す | |
| -- つまり Multiset は List を並び替えを区別せず同一視したものとして定義されている | |
| -- Lean4 において List は帰納型として定義されているためその要素数は有限である | |
| -- メモ2: | |
| -- 最初は Fintype も自作しようとしたが、、、 | |
| -- List で成り立つ性質が同値類による商を取った場合でも成り立つことを | |
| -- 逐一証明する作業が必要になり大変だったので、 | |
| -- 素直に mathlib4 の Fintype を利用する（巨人の肩に乗る）ことにした (^^;) | |
| import Mathlib.Algebra.BigOperators.Group.Finset.Basic -- Finset の総和(Σ)を取るために必要 | |
| import Mathlib.Data.Finset.Union -- Finset (Finset α) → Finset α を行う(Finset.biUnion)ために必要 | |
| import Mathlib.Data.Fintype.Card -- Fintype, Finset の要素数を数える(Fintype.card)ために必要 | |
| -- 自前で群を定義する（mathlib4 の Group と名前が被らないように） | |
| class Group' (G : Type u) where | |
| mul : G → G → G -- 演算 | |
| one : G -- 単位元 | |
| inv : G → G -- 逆元 | |
| assoc : ∀ a b c : G, mul (mul a b) c = mul a (mul b c) -- 結合法則（の証明） | |
| one_mul : ∀ a : G, mul one a = a -- 左単位元（が存在することの証明） | |
| inv_mul_self : ∀ a : G, mul (inv a) a = one -- 左逆元（が存在することの証明） | |
| namespace Group' | |
| -- 群の諸概念を表す記号を導入する | |
| infixl:70 "*" => mul | |
| notation "e" => one | |
| postfix:75 "⁻¹" => inv | |
| -- 以下 | |
| -- G を群(Group')とする | |
| variable {G : Type u} [Group' G] | |
| /-- 左逆元が右逆元となることの証明 -/ | |
| lemma self_mul_inv (a : G) : a * a⁻¹ = e := by | |
| calc | |
| a * a⁻¹ = e * (a * a⁻¹) := by rw [one_mul] | |
| _ = ((a⁻¹)⁻¹ * a⁻¹) * (a * a⁻¹) := by rw [inv_mul_self] | |
| _ = (a⁻¹)⁻¹ * (a⁻¹ * (a * a⁻¹)) := by rw [assoc] | |
| _ = (a⁻¹)⁻¹ * ((a⁻¹ * a) * a⁻¹) := by rw [assoc] | |
| _ = (a⁻¹)⁻¹ * (e * a⁻¹) := by rw [inv_mul_self] | |
| _ = (a⁻¹)⁻¹ * a⁻¹ := by rw [one_mul] | |
| _ = e := by rw [inv_mul_self] | |
| /-- 左単位元が右単位元となることの証明 -/ | |
| lemma mul_one (a : G) : a * e = a := by | |
| calc | |
| a * e = a * (a⁻¹ * a) := by rw [inv_mul_self] | |
| _ = (a * a⁻¹) * a := by rw [assoc] | |
| _ = e * a := by rw [self_mul_inv] | |
| _ = a := by rw [one_mul] | |
| /-- 逆元の逆元は最初の元に一致することの証明 -/ | |
| lemma inv_comp_inv (a : G) : (a⁻¹)⁻¹ = a := by | |
| calc | |
| (a⁻¹)⁻¹ = e * (a⁻¹)⁻¹ := by rw [one_mul] | |
| _ = (a * a⁻¹) * (a⁻¹)⁻¹ := by rw [self_mul_inv] | |
| _ = a * (a⁻¹ * (a⁻¹)⁻¹) := by rw [assoc] | |
| _ = a * e := by rw [self_mul_inv] | |
| _ = a := by rw [mul_one] | |
| /-- 積の逆元は順番を入れ替えた逆元の積と一致することの証明 -/ | |
| lemma mul_inv (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by | |
| calc | |
| (a * b)⁻¹ = e * (a * b)⁻¹ := by rw [one_mul] | |
| _ = b⁻¹ * b * (a * b)⁻¹ := by rw [inv_mul_self] | |
| _ = b⁻¹ * (e * b) * (a * b)⁻¹ := by rw [one_mul] | |
| _ = b⁻¹ * (a⁻¹ * a * b) * (a * b)⁻¹ := by rw [inv_mul_self] | |
| _ = b⁻¹ * (a⁻¹ * (a * b)) * (a * b)⁻¹ := by conv => enter [1, 1]; rw [assoc] -- ネストしている場合は conv で直接辿ることが可能 | |
| _ = ((b⁻¹ * a⁻¹) * (a * b)) * (a * b)⁻¹ := by simp only [assoc] -- 式を見れば明らかなので今後は simp only で楽をする | |
| _ = (b⁻¹ * a⁻¹) * ((a * b) * (a * b)⁻¹) := by rw [assoc] | |
| _ = (b⁻¹ * a⁻¹) * e := by rw [self_mul_inv] | |
| _ = b⁻¹ * a⁻¹ := by rw [mul_one] | |
| /-- 左簡約律の証明 -/ | |
| lemma mul_left_cancel {a b c : G} (h : a * b = a * c) : b = c := by | |
| calc | |
| b = e * b := by rw [one_mul] | |
| _ = (a⁻¹ * a) * b := by rw [inv_mul_self] | |
| _ = a⁻¹ * (a * b) := by rw [assoc] | |
| _ = a⁻¹ * (a * c) := by rw [h] | |
| _ = (a⁻¹ * a) * c := by rw [assoc] | |
| _ = e * c := by rw [inv_mul_self] | |
| _ = c := by rw [one_mul] | |
| /-- 右簡約律の証明 -/ | |
| lemma mul_right_cancel {a b c : G} (h : b * a = c * a) : b = c := by | |
| calc | |
| b = b * e := by rw [mul_one] | |
| _ = b * (a * a⁻¹) := by rw [self_mul_inv] | |
| _ = (b * a) * a⁻¹ := by rw [assoc] | |
| _ = (c * a) * a⁻¹ := by rw [h] | |
| _ = c * (a * a⁻¹) := by rw [assoc] | |
| _ = c * e := by rw [self_mul_inv] | |
| _ = c := by rw [mul_one] | |
| /-- a ∈ G, h ↦ a * h が単射であることの証明 -/ | |
| lemma mul_left_injective (a : G) : Function.Injective (fun h : G => a * h) := by | |
| -- def Function.Injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂ | |
| -- 単射であることの証明は左簡約律の証明とほぼ同じなので最初の2つの変数a₁,a₂は使わない | |
| -- h : a * a₁ = a * a₂ | |
| intro _ _ h | |
| exact mul_left_cancel h | |
| end Group' | |
| /-- 部分群 -/ | |
| structure Subgroup (G : Type*) [Group' G] where | |
| carrier : Set G -- 部分群に属するGの元の集合 | |
| -- mathlib4 では Set は以下のように定義されている | |
| -- def Set (α : Type u) := α → Prop | |
| -- また x ∈ s は s x と定義される | |
| -- carrier は空集合ではない（ことの証明） | |
| nonempty : ∃ x : G, x ∈ carrier | |
| -- 部分群となるための条件（を満たすことの証明） | |
| self_mul_inv_mem : ∀ {x y : G}, x ∈ carrier → y ∈ carrier → x * y⁻¹ ∈ carrier | |
| namespace Subgroup | |
| -- 以下 | |
| -- G を群(Group')とする | |
| -- H をGの部分群(Subgroup G)とする | |
| variable {G : Type u} [Group' G] | |
| variable {H : Subgroup G} | |
| /-- 部分群は単位元を含むことの証明 -/ | |
| lemma one_mem : (e : G) ∈ H.carrier := by | |
| -- rcases でパターンマッチを行い、空集合ではないという条件から要素を一つ取り出す | |
| -- a : G | |
| -- ha : a ∈ H.carrier | |
| rcases H.nonempty with ⟨a, ha⟩ | |
| have : a * a⁻¹ ∈ H.carrier := H.self_mul_inv_mem ha ha -- 補題の証明 | |
| rw [Group'.self_mul_inv] at this -- 名前をつけずに証明した補題は this で参照できる | |
| exact this | |
| /-- 部分群が逆元を取る操作で閉じていることの証明 -/ | |
| lemma inv_mem : ∀ {a : G}, a ∈ H.carrier → a⁻¹ ∈ H.carrier := by | |
| -- a : G | |
| -- ha : a ∈ H.carrier | |
| intro a ha | |
| have : e * a⁻¹ ∈ H.carrier := H.self_mul_inv_mem one_mem ha | |
| rw [Group'.one_mul] at this | |
| exact this | |
| /-- 部分群が群の演算で閉じていることの証明 -/ | |
| lemma mul_mem : ∀ {a b : G}, a ∈ H.carrier → b ∈ H.carrier → a * b ∈ H.carrier := by | |
| -- a : G | |
| -- b : G | |
| -- ha : a ∈ H.carrier | |
| -- hb : b ∈ H.carrier | |
| intro a b ha hb | |
| have : b⁻¹ ∈ H.carrier := inv_mem hb | |
| have : a * (b⁻¹)⁻¹ ∈ H.carrier := H.self_mul_inv_mem ha this | |
| rw [Group'.inv_comp_inv] at this | |
| exact this | |
| -- 以下 | |
| -- G を有限な(Fintype)群(Group')とする | |
| -- H をGの部分群(Subgroup G)とし、 | |
| -- 群Gの元がHに含まれること(H.carrier)は決定可能である(DecidablePred)とする | |
| variable {G : Type u} [Group' G] [Fintype G] | |
| variable {H : Subgroup G} [DecidablePred H.carrier] | |
| -- Hに属する元の有限集合による表現 | |
| -- carrier の実態は関数なので必要に応じて finset と使い分ける | |
| def finset : Finset G := Finset.univ.filter H.carrier | |
| /-- H.finset に属することと H.carrier に属することが実質的に同じことであることの証明 -/ | |
| lemma mem_finset {x : G} : x ∈ H.finset ↔ x ∈ H.carrier := by | |
| calc | |
| x ∈ H.finset ↔ x ∈ Finset.univ.filter H.carrier := by rw [finset] | |
| _ ↔ x ∈ Finset.univ ∧ x ∈ H.carrier := Finset.mem_filter | |
| _ ↔ True ∧ x ∈ H.carrier := by simp only [Finset.mem_univ] | |
| _ ↔ x ∈ H.carrier := by rw [true_and] | |
| -- 以下 | |
| -- G を有限な(Fintype)群(Group')とする | |
| -- **また任意のGの元a, bに対し a = b が決定可能である(DecidableEq)とする** | |
| -- H をGの部分群(Subgroup G)とし、 | |
| -- 群Gの元がHに含まれること(H.carrier)は決定可能である(DecidablePred)とする | |
| variable {G : Type u} [Group' G] [Fintype G] [DecidableEq G] | |
| variable {H : Subgroup G} [DecidablePred H.carrier] | |
| /-- g による H を法とする左剰余類 -/ | |
| def leftCoset (g : G) : Finset G := H.finset.image (fun x => g * x) | |
| /-- 左剰余類全体の集合 -/ | |
| def leftCosets : Finset (Finset G) := Finset.univ.image (fun (g : G) => H.leftCoset g) | |
| /-- x が左剰余類 gH の元であることは、あるHの元hが存在して x = gh と書けることと同値 -/ | |
| lemma mem_leftCoset_iff {g x : G} : x ∈ H.leftCoset g ↔ ∃ h : G, h ∈ H.carrier ∧ x = g * h := by | |
| calc | |
| x ∈ H.leftCoset g ↔ x ∈ Finset.image (fun x => g * x) H.finset := by rw [leftCoset] | |
| _ ↔ ∃ h ∈ H.finset, g * h = x := Finset.mem_image | |
| _ ↔ ∃ h : G, h ∈ H.carrier ∧ g * h = x := by simp only [mem_finset] | |
| _ ↔ ∃ h : G, h ∈ H.carrier ∧ x = g * h := by simp only [eq_comm] | |
| /-- 任意の左剰余類 gH の要素数は H の位数に等しい -/ | |
| lemma card_leftCoset : ∀ (g : G), (H.leftCoset g).card = H.finset.card := by | |
| intro g; calc | |
| (H.leftCoset g).card = (H.finset.image (fun x => g * x)).card := by rw [leftCoset] | |
| _ = H.finset.card | |
| := by apply Finset.card_image_iff.mpr | |
| intro _ _ _ _ hxy | |
| exact (Group'.mul_left_injective g) hxy | |
| -- apply を用いると、最終的に b を証明したいときに、 a → b を使って a を証明すれば良いことにできる | |
| -- ここでは (H.finset.image f).card = H.finset.card を証明したいので | |
| -- card_image_iff : (Finset.image f s).card = s.card ↔ Set.InjOn f s | |
| -- を apply すれば(.mpr は左向き矢印を使うという意味) | |
| -- Set.InjOn (fun x => g * x) H.finset を証明すれば良いことになる | |
| -- ``` | |
| -- def InjOn (f : α → β) (s : Set α) : Prop := | |
| -- ∀ ⦃x₁ : α⦄, x₁ ∈ s → ∀ ⦃x₂ : α⦄, x₂ ∈ s → f x₁ = f x₂ → x₁ = x₂ | |
| -- ``` | |
| -- なので intro で hxy : (fun x => g * x) x₁ = (fun x => g * x) x₂ を導入すれば | |
| -- 左簡約律から x₁ = x₂ が証明できる | |
| /-- 左剰余類全体の集合の元である集合の要素数は H の位数に等しい -/ | |
| lemma card_of_each_coset : ∀C ∈ H.leftCosets, C.card = H.finset.card := by | |
| -- hC : C ∈ leftCosets | |
| intro _ hC | |
| rcases Finset.mem_image.mp hC with ⟨g, _, rfl⟩ | |
| -- mem_image : b ∈ Finset.image f s ↔ ∃ a ∈ s, f a = b | |
| -- を使って左剰余類 C の代表元 g を取り出す | |
| -- rfl は H.leftCoset g = C の証明として指定している | |
| exact card_leftCoset g | |
| /-- 2つの左剰余類の共通集合が空でなければその２つの左剰余類は等しいことの証明 -/ | |
| lemma coset_eq_of_inter_nonempty {a b : G} (hne : ((H.leftCoset a) ∩ (H.leftCoset b)).Nonempty) : H.leftCoset a = H.leftCoset b := by | |
| -- x : G | |
| -- hx : x ∈ H.leftCoset a ∩ H.leftCoset b | |
| -- hxA : x ∈ H.leftCoset a | |
| -- hxB : x ∈ H.leftCoset b | |
| rcases hne with ⟨x, hx⟩; rw [Finset.mem_inter] at hx; rcases hx with ⟨hxA, hxB⟩ | |
| -- h₁ : G | |
| -- hh₁ : h₁ ∈ H.carrier | |
| -- h₂ : G | |
| -- hh₂ : h₂ ∈ H.carrier | |
| -- ah1_eq_bh2 : a * h₁ = b * h₂ | |
| rcases mem_leftCoset_iff.mp hxA with ⟨h₁, hh₁, rfl⟩ | |
| rcases mem_leftCoset_iff.mp hxB with ⟨h₂, hh₂, ah1_eq_bh2⟩ | |
| have b_inv_a_in_H : b⁻¹ * a ∈ H.carrier := by | |
| have : b⁻¹ * a = h₂ * h₁⁻¹ := by | |
| calc | |
| b⁻¹ * a = b⁻¹ * a * h₁ * h₁⁻¹ := by simp only [Group'.mul_one, Group'.self_mul_inv, Group'.assoc] | |
| _ = b⁻¹ * b * h₂ * h₁⁻¹ := by simp only [ah1_eq_bh2, Group'.assoc] | |
| _ = h₂ * h₁⁻¹ := by rw [Group'.inv_mul_self, Group'.one_mul] | |
| rw [this] | |
| exact H.mul_mem hh₂ (H.inv_mem hh₁) | |
| have sub_ab : H.leftCoset a ⊆ H.leftCoset b := by | |
| -- subset_iff : s₁ ⊆ s₂ ↔ ∀ ⦃x : α⦄, x ∈ s₁ → x ∈ s₂ | |
| apply Finset.subset_iff.mpr | |
| intro x hxA' | |
| rcases mem_leftCoset_iff.mp hxA' with ⟨h, hh, xah⟩ | |
| -- mem_leftCoset_iff : x ∈ leftCoset g ↔ ∃ h ∈ H.carrier, x = g*h | |
| apply mem_leftCoset_iff.mpr | |
| have b_inv_a_h_in_H : b⁻¹ * a * h ∈ H.carrier := H.mul_mem b_inv_a_in_H hh | |
| have : x = b * (b⁻¹ * a * h) := by | |
| calc | |
| x = a * h := by rw [xah] | |
| _ = b * b⁻¹ * a * h := by simp only [Group'.one_mul, Group'.self_mul_inv] | |
| _ = b * (b⁻¹ * a * h) := by simp only [Group'.assoc] | |
| exact ⟨b⁻¹ * a * h, b_inv_a_h_in_H, this⟩ | |
| have sub_ba : H.leftCoset b ⊆ H.leftCoset a := by | |
| apply Finset.subset_iff.mpr | |
| intro x hxB' | |
| rcases mem_leftCoset_iff.mp hxB' with ⟨h, hh, xbh⟩ | |
| apply mem_leftCoset_iff.mpr | |
| have a_inv_b_h_in_H : a⁻¹ * b * h ∈ H.carrier := by | |
| have : a⁻¹ * b * h = (b⁻¹ * a)⁻¹ * h := by | |
| calc | |
| a⁻¹ * b * h = a⁻¹ * (b⁻¹)⁻¹ * h := by rw [Group'.inv_comp_inv] | |
| _ = (b⁻¹ * a)⁻¹ * h := by rw [Group'.mul_inv] | |
| rw [this] | |
| exact H.mul_mem (H.inv_mem b_inv_a_in_H) hh | |
| have : x = a * (a⁻¹ * b * h) := by | |
| calc | |
| x = b * h := by rw [xbh] | |
| _ = a * a⁻¹ * b * h := by simp only [Group'.one_mul, Group'.self_mul_inv] | |
| _ = a * (a⁻¹ * b * h) := by simp only [Group'.assoc] | |
| exact ⟨a⁻¹ * b * h, a_inv_b_h_in_H, this⟩ | |
| -- antisymm_iff : s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁ | |
| exact Finset.Subset.antisymm_iff.mpr ⟨sub_ab, sub_ba⟩ | |
| /-- 左剰余類は異なる集合であれば交わりを持たない -/ | |
| lemma disjoint_of_ne_cosets {a b : G} (hne : H.leftCoset a ≠ H.leftCoset b) : Disjoint (H.leftCoset a) (H.leftCoset b) := by | |
| -- disjoint_left : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t | |
| apply Finset.disjoint_left.mpr | |
| intro x hxA hxB -- x ∉ H.leftCoset b = x ∈ H.leftCoset b → False なのでゴールが False となる。つまり矛盾を示せば良い | |
| -- mem_inter : a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂ | |
| exact hne (coset_eq_of_inter_nonempty ⟨x, Finset.mem_inter.mpr ⟨hxA, hxB⟩⟩) -- False となり矛盾 | |
| /-- 左剰余類の和集合は元の群全体と一致する -/ | |
| lemma cosets_union_eq_univ : H.leftCosets.biUnion id = (Finset.univ : Finset G) := by | |
| apply Finset.Subset.antisymm_iff.mpr | |
| constructor -- a ∧ b の証明を a と b それぞれの証明に分ける（各証明は·で始まる） | |
| · -- H.leftCosets.biUnion ⊆ Finset.univ を示す | |
| -- x : G | |
| intro x _ | |
| exact Finset.mem_univ x | |
| · -- Finset.univ ⊆ H.leftCosets.biUnion を示す | |
| -- g : G | |
| intro g _ | |
| have gH_in_cosets : H.leftCoset g ∈ H.leftCosets := Finset.mem_image.mpr ⟨g, Finset.mem_univ g, rfl⟩ | |
| have : g ∈ H.leftCoset g := mem_leftCoset_iff.mpr ⟨e, H.one_mem, by rw [Group'.mul_one]⟩ | |
| -- mem_biUnion : b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a | |
| exact Finset.mem_biUnion.mpr ⟨H.leftCoset g, gH_in_cosets, this⟩ | |
| /-- 左剰余類は異なる集合であれば交わりを持たない（leftCosets版） -/ | |
| lemma pairwise_disjoint_on_cosets : ∀ C₁ ∈ H.leftCosets, ∀ C₂ ∈ H.leftCosets, C₁ ≠ C₂ → Disjoint C₁ C₂ := by | |
| -- h1 : C₁ ∈ leftCosets | |
| -- h2 : C₂ ∈ leftCosets | |
| intro _ h1 _ h2 hne | |
| rcases Finset.mem_image.mp h1 with ⟨_, _, rfl⟩ -- ∃a ∈ Finset.univ, C₁ = leftCoset a | |
| rcases Finset.mem_image.mp h2 with ⟨_, _, rfl⟩ -- ∃b ∈ Finset.univ, C₂ = leftCoset b | |
| exact disjoint_of_ne_cosets hne | |
| /-- ラグランジュの定理 -/ | |
| theorem card_subgroup_divides_card : H.finset.card ∣ Fintype.card G := by | |
| have : Fintype.card G = H.finset.card * H.leftCosets.card := by | |
| calc | |
| Fintype.card G = (H.leftCosets.biUnion id).card := by rw [cosets_union_eq_univ, Finset.card_univ] | |
| -- card_biUnion (h : s.PairwiseDisjoint t) : (s.biUnion t).card = ∑ u ∈ s, (t u).card | |
| _ = ∑ C ∈ H.leftCosets, C.card := Finset.card_biUnion pairwise_disjoint_on_cosets | |
| -- sum_congr : (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g | |
| _ = ∑ C ∈ H.leftCosets, H.finset.card := Finset.sum_congr rfl card_of_each_coset | |
| -- sum_const_nat (h : ∀ x ∈ s, f x = m) : ∑ x ∈ s, f x = s.card * m | |
| _ = H.leftCosets.card * H.finset.card := Finset.sum_const_nat (by intro _ _; rfl) | |
| _ = H.finset.card * H.leftCosets.card := by rw [Nat.mul_comm] | |
| exact ⟨H.leftCosets.card, this⟩ | |
| end Subgroup |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment