FenchelNielsenZomorrodian/Discrete/GroupTheory/Basic.lean
1import Mathlib.Tactic.NormNum.LegendreSymbol
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/GroupTheory/Basic.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Discrete group-theoretic support
15-/
17namespace FenchelNielsen
19def IsTorsionFreeGroup (G : Type*) [Group G] : Prop :=
20 ∀ g : G, IsOfFinOrder g → g = 1
22def IsPerfectGroup (G : Type*) [Group G] : Prop :=
23 derivedSeries G 1 = ⊤
25theorem isTorsionFreeGroup_of_mulEquiv
26 {G H : Type*} [Group G] [Group H] (e : G ≃* H)
27 (hTF : IsTorsionFreeGroup G) :
28 IsTorsionFreeGroup H := by
29 intro h hfin
30 have hpre :
31 e.symm h = 1 :=
32 hTF (e.symm h) (MonoidHom.isOfFinOrder e.symm.toMonoidHom hfin)
33 simpa using congrArg e hpre
36 {G H : Type*} [Group G] [Group H] (φ : G →* H)
37 (hker : IsTorsionFreeGroup φ.ker) {x : G} (hx : IsOfFinOrder x) :
38 orderOf (φ x) = orderOf x := by
39 apply Nat.dvd_antisymm
40 · exact orderOf_map_dvd φ x
41 · have hpowMap : φ (x ^ orderOf (φ x)) = 1 := by
42 rw [map_pow, pow_orderOf_eq_one]
43 let k : φ.ker := ⟨x ^ orderOf (φ x), hpowMap⟩
44 have hkfin : IsOfFinOrder k := by
45 have hxpow : IsOfFinOrder (x ^ orderOf (φ x)) := hx.pow
46 simpa [k] using
47 (Submonoid.isOfFinOrder_coe
48 (H := φ.ker.toSubmonoid) (x := k)).1 hxpow
49 have hkone : k = 1 := hker k hkfin
50 have hxpowOne : x ^ orderOf (φ x) = 1 := by
51 simpa [k] using congrArg Subtype.val hkone
52 exact orderOf_dvd_of_pow_eq_one hxpowOne
54end FenchelNielsen