Skip to content

Instantly share code, notes, and snippets.

@lotz84

lotz84/README.md

Last active August 31, 2025 06:09
Show Gist options
  • Save lotz84/ba332f32f933adc1a0f6aa57e0d93e18 to your computer and use it in GitHub Desktop.
Save lotz84/ba332f32f933adc1a0f6aa57e0d93e18 to your computer and use it in GitHub Desktop.
Download ZIP
指数2の部分群は正規部分群であることの Lean4 による証明
Raw
README.md

指数2の部分群は正規部分群であることの Lean4 による証明

Lean4 Web

Raw
proof.lean
import Mathlib.GroupTheory.Index
-- 左剰余類 g • H と右剰余類 op g • H の演算子を使うため
open Pointwise MulOpposite
-- G を群とする
variable {G : Type*} [Group G]
-- H を G の部分群とする
variable {H : Subgroup G}
-- 元 g の H による左（右）剰余類を返す関数
def leftCoset (H : Subgroup G) (g : G) : Quotient (QuotientGroup.leftRel H) := Quot.mk (QuotientGroup.leftRel H) g
def rightCoset (H : Subgroup G) (g : G) : Quotient (QuotientGroup.rightRel H) := Quot.mk (QuotientGroup.rightRel H) g
-- mathlib にある以下の定理に似た QuotientGroup.eq_one_iff という定理は H が正規部分群であることを要請するが、
-- 今回は部分群であるという条件しか使えないので左剰余類版と右剰余類版を自分で証明する
/-- ある元 g の左剰余類が単位元の左剰余類と一致することは x が H に含まれること同値であることの証明 -/
theorem left_eq_one_iff (g : G) : leftCoset H g = leftCoset H 1 ↔ g ∈ H := by
-- QuotientGroup.eq : ↑a = ↑b ↔ a⁻¹ * b ∈ s
-- （↑は変換を強制すること（coercion）を表す）
apply QuotientGroup.eq.trans
-- apply により g⁻¹ * 1 ∈ H ↔ g ∈ H を証明すれば良い
rw [mul_one, Subgroup.inv_mem_iff]
/-- ある元 g の右剰余類が単位元の右剰余類と一致することは x が H に含まれること同値であることの証明 -/
theorem right_eq_one_iff (g : G) : rightCoset H g = rightCoset H 1 ↔ g ∈ H := by
-- Quotient.eq'' : Quotient.mk'' a = Quotient.mk'' b ↔ s a b
apply Quotient.eq''.trans
-- QuotientGroup.rightRel_apply : (QuotientGroup.rightRel s) x y ↔ y * x⁻¹ ∈ s
apply QuotientGroup.rightRel_apply.trans
rw [one_mul, Subgroup.inv_mem_iff]
/-- 指数2の部分群は正規部分群であることの証明 -/
theorem subgroup_of_index_two_is_normal (h_index : H.index = 2) : H.Normal := by
-- Subgroup.Normal.mk (conj_mem : ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H) : H.Normal
apply Subgroup.Normal.mk
-- apply により ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H) を証明すれば良い
-- n : G
-- hn : n ∈ H
-- g : G
intro n hn g
by_cases hg : g ∈ H
· -- hg : g ∈ H の場合は明らか
-- inv_mem : x ∈ H → x⁻¹ ∈ H
-- mul_mem : a ∈ H → b ∈ H → a * b ∈ H
exact mul_mem (mul_mem hg hn) (inv_mem hg)
· -- hg : g ∉ H の場合、
-- まず g の左剰余類と右剰余類が一致することを証明する
have h_gH_eq_Hg : g • H.carrier = op g • H.carrier := by
-- 群 G (Set.univ : Set G) は集合として左剰余類 H と gH の和集合と一致することの証明
have h_union_left : Set.univ = H.carrier ∪ g • H.carrier := by
-- ext により x ∈ Set.univ ↔ x ∈ H.carrier ∪ g • H.carrier を証明すれば良い
ext x; constructor
· -- x ∈ Set.univ → x ∈ H.carrier ∪ g • H.carrier
intro _
-- Set.mem_union : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b
rw [Set.mem_union]
by_cases hx : x ∈ H
· -- hx : x ∈ H の場合は明らか
exact Or.inl hx
· -- hx : x ∉ H の場合、
-- refine を使えば x ∈ g • H.carrier の証明（?_ の部分）に帰着する
refine Or.inr ?_
-- Set.mem_smul_set_iff_inv_smul_mem : x ∈ a • A ↔ a⁻¹ * x ∈ A
apply Set.mem_smul_set_iff_inv_smul_mem.mpr
-- apply により g⁻¹ * x ∈ H を証明すれば良い
-- 左剰余類全体の集合の型を LeftCosets と名付ける
let LeftCosets := Quotient (QuotientGroup.leftRel H)
-- 仮定より左剰余類の個数は2個
have h_card_LeftCosets : Nat.card LeftCosets = 2 := h_index
-- 単位元, x, g が属する左剰余類にそれぞれ名前をつける
let coset_1 : LeftCosets := leftCoset H 1
let coset_x : LeftCosets := leftCoset H x
let coset_g : LeftCosets := leftCoset H g
-- coset_x と coset_1 は異なる
have hx_coset_ne : coset_x ≠ coset_1 := by
-- h_eq : coset_x = coset_1
intro h_eq
-- coset_x = coset_1 なら x ∈ H となるが (hx : x ∉ H) より矛盾する
exact hx ((left_eq_one_iff x).mp h_eq)
-- coset_g と coset_1 は異なる
have hg_coset_ne : coset_g ≠ coset_1 := by
-- h_eq : coset_g = coset_1
intro h_eq
-- coset_g = coset_1 なら g ∈ H となるが (hg : x ∉ H) より矛盾する
exact hg ((left_eq_one_iff g).mp h_eq)
-- 左剰余類全体の集合の要素数は2なので単位元が属する左剰余類の他にもう一つだけ別の左剰余類が存在する
-- Nat.card_eq_two_iff' : Nat.card α = 2 ↔ ∃! y, y ≠ x
-- coset_y : LeftCosets
-- hy_unique : ∀ (coset_z : LeftCosets), coset_z ≠ coset_1 → coset_z = coset_y
-- （ obtain の際に - を指定するとコンテキストから消すことができる）
obtain ⟨coset_y, -, hy_unique⟩ : ∃!y, y ≠ coset_1 := (Nat.card_eq_two_iff' coset_1).mp h_card_LeftCosets
-- coset_g, coset_x は共に coset_1 と異なるため coset_y に等しく
-- それ故に coset_g と coset_x は等しい
have h_cosets_eq : coset_g = coset_x := by
calc
coset_g = coset_y := by rw [hy_unique (coset_g) hg_coset_ne]
_ = coset_x := by rw [hy_unique (coset_x) hx_coset_ne]
-- Quotient.eq' : Quotient.mk' a = Quotient.mk' b ↔ s a b
-- QuotientGroup.leftRel_apply : (QuotientGroup.leftRel s) x y ↔ x⁻¹ * y ∈ s
exact QuotientGroup.leftRel_apply.mp (Quotient.eq'.mp h_cosets_eq)
· -- x ∈ H.carrier ∪ g • H.carrier → x ∈ Set.univ
intro _
-- Set.eq_univ_iff_forall : s = Set.univ ↔ ∀ (x : α), x ∈ s
exact Set.eq_univ_iff_forall.mp rfl x
-- 群 G (Set.univ : Set G) は集合として右剰余類 H と Hg の和集合と一致することの証明
-- 証明は左剰余類の場合と同様だが mathlib の実装の都合により微妙に異なる
have h_union_right : Set.univ = H.carrier ∪ op g • H.carrier := by
ext x; constructor
· -- x ∈ Set.univ → x ∈ H.carrier ∪ op g • H.carrier
intro _
-- Set.mem_union : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b
rw [Set.mem_union]
by_cases hx : x ∈ H
· -- hx : x ∈ H の場合は明らか
exact Or.inl hx
· -- hx : x ∉ H の場合、
-- refine を使えば x ∈ op g • H.carrier の証明（?_ の部分）に帰着する
refine Or.inr ?_
-- Set.mem_smul_set_iff_inv_smul_mem : x ∈ a • A ↔ a⁻¹ * x ∈ A
apply Set.mem_smul_set_iff_inv_smul_mem.mpr
-- apply により x * g⁻¹ ∈ H を証明すれば良い
-- 右剰余類全体の集合の型を RightCosets と名付ける
let RightCosets := Quotient (QuotientGroup.rightRel H)
-- 右剰余類の個数は2個であることを証明したいが、
-- H.index = Nat.card (G⧸H) であり左剰余類(G⧸H)を経由する必要があるため左剰余類の時と比べて証明は面倒くさい(^^;)
-- （ちなみに G⧸H の真ん中の記号はスラッシュ / ではなく `\quot` で出る記号 ⧸ なので注意）
-- まず G⧸H が Fintype であることを証明する
have : H.index ≠ 0 := by
-- hzero : H.index = 0
intro hzero
-- hzero : 2 = 0
rw [h_index] at hzero
-- Nat.succ_ne_zero(n : Nat) : n.succ ≠ 0
-- 2 は 1 の後者なので 0 ではないので矛盾
exact (Nat.succ_ne_zero 1) hzero
have : H.FiniteIndex := ⟨this⟩
-- Subgroup.fintypeQuotientOfFiniteIndex {H : Subgroup G} [H.FiniteIndex] : Fintype (G⧸H)
have : Fintype (G⧸H) := Subgroup.fintypeQuotientOfFiniteIndex
-- 改めて、仮定より右剰余類の個数は2個であることを証明する
have h_card_RightCosets : Nat.card RightCosets = 2 := by
calc
Nat.card RightCosets = Nat.card (Quotient (QuotientGroup.rightRel H)) := by rfl
-- Nat.card_eq_fintype_card : Nat.card α = Fintype.card α
_ = Fintype.card (Quotient (QuotientGroup.rightRel H)) := by rw [Nat.card_eq_fintype_card]
-- QuotientGroup.card_quotient_rightRel.{u} {α : Type u} [Group α] (s : Subgroup α) [Fintype (α ⧸ s)] :
-- Fintype.card (Quotient (QuotientGroup.rightRel s)) = Fintype.card (α ⧸ s)
_ = Fintype.card (G⧸H) := by rw [QuotientGroup.card_quotient_rightRel]
_ = Nat.card (G⧸H) := by rw [Nat.card_eq_fintype_card]
_ = 2 := h_index
-- 単位元, x, g が属する右剰余類にそれぞれ名前をつける
let coset_1 : RightCosets := rightCoset H 1
let coset_x : RightCosets := rightCoset H x
let coset_g : RightCosets := rightCoset H g
-- coset_x と coset_1 は異なる
have hx_coset_ne : coset_x ≠ coset_1 := by
-- h_eq : coset_x = coset_1
intro h_eq
-- coset_x = coset_1 なら x ∈ H となるが (hx : x ∉ H) より矛盾する
exact hx ((right_eq_one_iff x).mp h_eq)
-- coset_g と coset_1 は異なる
have hg_coset_ne : coset_g ≠ coset_1 := by
-- h_eq : coset_g = coset_1
intro h_eq
-- coset_g = coset_1 なら g ∈ H となるが (hg : x ∉ H) より矛盾する
exact hg ((right_eq_one_iff g).mp h_eq)
-- 右剰余類全体の集合の要素数は2なので単位元が属する右剰余類の他にもう一つだけ別の右剰余類が存在する
-- Nat.card_eq_two_iff' : Nat.card α = 2 ↔ ∃! y, y ≠ x
-- coset_y : RightCosets
-- hy_unique : ∀ (coset_z : RightCosets), coset_z ≠ coset_1 → coset_z = coset_y
obtain ⟨coset_y, -, hy_unique⟩ : ∃!y, y ≠ coset_1 := (Nat.card_eq_two_iff' coset_1).mp h_card_RightCosets
-- coset_g, coset_x は共に coset_1 と異なるため coset_y に等しく
-- それ故に coset_g と coset_x は等しい
have h_cosets_eq : coset_g = coset_x := by
calc
coset_g = coset_y := by rw [hy_unique (coset_g) hg_coset_ne]
_ = coset_x := by rw [hy_unique (coset_x) hx_coset_ne]
-- Quotient.eq' : Quotient.mk' a = Quotient.mk' b ↔ s a b
-- QuotientGroup.rightRel_apply : (QuotientGroup.rightRel s) x y ↔ y * x⁻¹ ∈ s
exact QuotientGroup.rightRel_apply.mp (Quotient.eq'.mp h_cosets_eq)
· -- x ∈ H.carrier ∪ op g • H.carrier → x ∈ Set.univ
intro _
-- Set.eq_univ_iff_forall : s = Set.univ ↔ ∀ (x : α), x ∈ s
exact Set.eq_univ_iff_forall.mp rfl x
-- H.carrier と左剰余類 g • H.carrier が交わりを持たないことを証明する
have h_disjoint_left : Disjoint H.carrier (g • H.carrier) := by
-- Set.disjoint_left : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
apply Set.disjoint_left.mpr
-- x : G
-- hxH : x ∈ H.carrier
-- hxgH : x ∈ g • H.carrier
intro x hxH hxgH
-- h : G
-- hhH : h ∈ H.carrier
-- x = g * h
rcases hxgH with ⟨h, hhH, rfl⟩
have : (g * h) * h⁻¹ ∈ H := H.mul_mem hxH (H.inv_mem hhH)
have : g ∈ H := by rw [mul_assoc, mul_inv_cancel, mul_one] at this; exact this
-- これは hg : g ∉ H と矛盾する
exact hg this
-- H.carrier と右剰余類 op g • H.carrier が交わりを持たないことを証明する
have h_disjoint_right : Disjoint H.carrier (op g • H.carrier) := by
-- Set.disjoint_left : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
apply Set.disjoint_left.mpr
-- x : G
-- hxH : x ∈ H.carrier
-- hxHg : x ∈ op g • H.carrier
intro x hxH hxHg
-- h : G
-- hhH : h ∈ H.carrier
-- x = h * g
rcases hxHg with ⟨h, hhH, rfl⟩
have : h⁻¹ * (h * g) ∈ H := H.mul_mem (H.inv_mem hhH) hxH
have : g ∈ H := by rw [←mul_assoc, inv_mul_cancel, one_mul] at this; exact this
-- これは hg : g ∉ H と矛盾する
exact hg this
-- 左剰余類 gH は G \ H と集合として一致する
have h_left : g • H.carrier = Set.univ \ H.carrier := by
ext x; constructor
· -- x ∈ g • H.carrier → x ∈ Set.univ \ H.carrier
-- hxgH : x ∈ g • H.carrier
intro hxgH
constructor
· -- x ∈ Set.univ
exact Set.eq_univ_iff_forall.mp rfl x
· -- x ∉ H.carrier
-- hxH : x ∈ H.carrier
intro hxH
-- H.carrier と g • H.carrier は素集合なので
-- x ∈ g • H.carrier と x ∈ H.carrier が両立することは矛盾
-- Set.disjoint_left : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
exact (Set.disjoint_left.mp h_disjoint_left) hxH hxgH
· -- x ∈ Set.univ \ H.carrier → x ∈ g • H.carrier
-- hxDiff : x ∈ Set.univ \ H.carrier
intro hxDiff
-- hx_notH : x ∉ H.carrier
rcases hxDiff with ⟨_, hx_notH⟩
have hxHU : x ∈ H.carrier ∪ g • H.carrier := by
rw [←h_union_left]
exact Set.eq_univ_iff_forall.mp rfl x
by_cases hxH : x ∈ H.carrier
· -- hxH : x ∈ H.carrier
-- 仮定よりここには到達しないので到達すれば矛盾より証明終了
exact (hx_notH hxH).elim
· -- x ∉ H.carrier
-- Or.resolve_left (h : a ∨ b) (na : ¬a) : b
exact hxHU.resolve_left hxH
-- 右剰余類 Hg は G \ H と集合として一致する
have h_right : op g • H.carrier = Set.univ \ H.carrier := by
ext x; constructor
· -- x ∈ op g • H.carrier → x ∈ Set.univ \ H.carrier
-- hxHg : x ∈ op g • H.carrier
intro hxHg
constructor
· -- x ∈ Set.univ
exact Set.eq_univ_iff_forall.mp rfl x
· -- x ∉ H.carrier
-- hxH : x ∈ H.carrier
intro hxH
-- H.carrier と op g • H.carrier は素集合なので
-- x ∈ op g • H.carrier と x ∈ H.carrier が両立することは矛盾
-- Set.disjoint_left : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
exact (Set.disjoint_left.mp h_disjoint_right) hxH hxHg
· -- x ∈ Set.univ \ H.carrier → x ∈ op g • H.carrier
-- hxDiff : x ∈ Set.univ \ H.carrier
intro hxDiff
-- hx_notH : x ∉ H.carrier
rcases hxDiff with ⟨_, hx_notH⟩
have hxHU : x ∈ H.carrier ∪ op g • H.carrier := by
rw [←h_union_right]
exact Set.eq_univ_iff_forall.mp rfl x
by_cases hxH : x ∈ H.carrier
· -- hxH : x ∈ H.carrier
-- 仮定よりここには到達しないので到達すれば矛盾より証明終了
exact (hx_notH hxH).elim
· -- x ∉ H.carrier
-- Or.resolve_left (h : a ∨ b) (na : ¬a) : b
exact hxHU.resolve_left hxH
-- いよいよ本題！
-- これが g • H.carrier = op g • H.carrier の証明の途中であったことを思い出そう
calc
g • H.carrier = Set.univ \ H.carrier := h_left
_ = op g • H.carrier := h_right.symm
-- mem_leftCoset (g : G) (hxS : n ∈ H) : g * x ∈ g • H
have h_mem_gH : g * n ∈ g • H.carrier := mem_leftCoset g hn
have h_mem_Hg : g * n ∈ op g • H.carrier := by
rw [←h_gH_eq_Hg]
exact h_mem_gH
-- Set.mem_smul_set_iff_inv_smul_mem : x ∈ a • A ↔ a⁻¹ • x ∈ A
-- よって g * n * g⁻¹ ∈ H
exact Set.mem_smul_set_iff_inv_smul_mem.mp h_mem_Hg
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment