長めの例: 共役部分群¶
群 G の部分群 S と元 g : G に対して，
g S g⁻¹ = {x | ∃ s ∈ S, x = g * s * g⁻¹} はまた部分群です．
これは抽象代数学の基本例で，閉性の証明に group がよく効きます．
section ConjugateSubgroup
variable {G : Type*} [Group G]
def conjugateSubgroup (g : G) (S : Subgroup G) : Subgroup G where
carrier := {x : G | ∃ s, s ∈ S ∧ x = g * s * g⁻¹}
one_mem' := by
refine ⟨1, S.one_mem, ?_⟩
group
mul_mem' := by
rintro x y ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩
refine ⟨s * t, S.mul_mem hs ht, ?_⟩
group
inv_mem' := by
rintro x ⟨s, hs, rfl⟩
refine ⟨s⁻¹, S.inv_mem hs, ?_⟩
group
example (g : G) (S : Subgroup G) {x : G} :
x ∈ conjugateSubgroup g S ↔ ∃ s, s ∈ S ∧ x = g * s * g⁻¹ := by
rfl
example (S : Subgroup G) {x : G} : x ∈ conjugateSubgroup (1 : G) S ↔ x ∈ S := by
constructor
· rintro ⟨s, hs, rfl⟩
simpa using hs
· intro hx
refine ⟨x, hx, ?_⟩
group
end ConjugateSubgroup
この例で使った証明パターンは，部分構造の自作で頻繁に現れます．
rintro ... ⟨s, hs, rfl⟩で存在記号と等式を分解する．- 閉性は
S.mul_mem，S.inv_memなどを使う． - 群の計算は
groupに任せる．
学部レベルの代数を形式化するときは，まずこのような「集合を carrier として持つ構造体」を自作できることが重要です．
演習問題¶
conjugateSubgroup について，g⁻¹ で再び共役すると元に戻ることを示してください．