FenchelNielsenZomorrodian/Discrete/GroupTheory/DerivedSeries.lean
1import FenchelNielsenZomorrodian.Discrete.GroupTheory.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/GroupTheory/DerivedSeries.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
19universe u v
22 (G : Type*) [CommGroup G] :
23 derivedSeries G 1 = ⊥ := by
24 rw [derivedSeries_one]
25 rw [commutator_eq_bot_iff_center_eq_top, CommGroup.center_eq_top]
28 {G : Type*} [Group G] (H : Subgroup G) (hH : derivedSeries G 1 ≤ H) :
29 ∀ n : ℕ, derivedSeries G (n + 1) ≤ (derivedSeries H n).map H.subtype := by
30 intro n
31 induction n with
33 have hRange : H ≤ H.subtype.range := by
34 simp only [H.range_subtype, le_refl]
35 simpa [derivedSeries_zero, MonoidHom.range_eq_map] using hH.trans hRange
36 | succ n ih =>
37 calc
38 derivedSeries G (n + 1 + 1) = ⁅derivedSeries G (n + 1), derivedSeries G (n + 1)⁆ := by
39 rw [derivedSeries_succ]
40 _ ≤ ⁅(derivedSeries H n).map H.subtype, (derivedSeries H n).map H.subtype⁆ :=
41 Subgroup.commutator_mono ih ih
42 _ = (derivedSeries H (n + 1)).map H.subtype := by
43 rw [derivedSeries_succ, Subgroup.map_commutator]
45theorem derivedSeries_map_surjective
46 {G : Type*} {H : Type*} [Group G] [Group H]
47 (f : G →* H) (hf : Function.Surjective f) :
48 ∀ m : ℕ, Subgroup.map f (derivedSeries G m) = derivedSeries H m := by
49 intro m
50 induction m with
52 ext y
53 constructor
54 · intro _hy
55 trivial
56 · intro _hy
57 rcases hf y with ⟨x, rfl⟩
58 exact ⟨x, trivial, rfl⟩
59 | succ m ih =>
60 rw [derivedSeries_succ, derivedSeries_succ, Subgroup.map_commutator, ih]
62theorem derivedSeries_ulift_eq_bot_of
63 {G : Type v} [Group G] {m : ℕ}
64 (h : derivedSeries G m = ⊥) :
65 derivedSeries (ULift.{u, v} G) m = ⊥ := by
66 let e : ULift.{u, v} G ≃* G := MulEquiv.ulift
67 have hmap :
68 Subgroup.map e.toMonoidHom (derivedSeries (ULift.{u, v} G) m) =
69 (⊥ : Subgroup G) := by
70 rw [derivedSeries_map_surjective e.toMonoidHom e.surjective m, h]
71 apply le_antisymm
72 · intro x hx
73 have hxmap :
74 e.toMonoidHom x ∈
75 Subgroup.map e.toMonoidHom (derivedSeries (ULift.{u, v} G) m) :=
76 ⟨x, hx, rfl⟩
77 rw [hmap] at hxmap
78 exact Subgroup.mem_bot.mpr
79 (e.injective (Subgroup.mem_bot.mp hxmap))
80 · exact bot_le
82end FenchelNielsen