FenchelNielsenZomorrodian/Discrete/FiniteIndex/KernelTransfer.lean
1import FenchelNielsenZomorrodian.Discrete.FiniteIndex.NormalCore
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/FiniteIndex/KernelTransfer.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finite-index torsion-free subgroup data
14Abstract finite-index and smooth quotient data, kernel transfer, normal core, and derived-length predicates for discrete Fuchsian groups.
15-/
17namespace FenchelNielsen
20 {G G' : Type*} [Group G] [Group G']
21 (f : G →* G') (H : Subgroup G') [H.FiniteIndex] :
22 (H.comap f).FiniteIndex := by
23 apply Subgroup.finiteIndex_iff.2
24 rw [Subgroup.index_comap]
25 exact Subgroup.FiniteIndex.index_ne_zero (H := H.subgroupOf f.range)
28 {G A H : Type*} [Group G] [CommGroup A] [Finite A] [Group H]
29 (φ : G →* A)
30 (e : φ.ker ≃* H) {n : ℕ}
31 (hTarget : ∃ L : Subgroup H,
32 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
34 ∃ S : Subgroup G,
35 S.FiniteIndex ∧ IsTorsionFreeGroup S ∧
36 SubgroupQuotientHasDerivedLengthAtMost S (n + 1) := by
37 haveI : φ.ker.FiniteIndex := Subgroup.finiteIndex_ker φ
38 rcases hTarget with ⟨L, hLFiniteIndex, hLTF, hLQuot⟩
39 haveI : L.FiniteIndex := hLFiniteIndex
40 let L₀ : Subgroup φ.ker := L.comap e.toMonoidHom
41 let S : Subgroup G := L₀.map φ.ker.subtype
42 haveI : L₀.FiniteIndex :=
43 subgroup_finiteIndex_comap_of_finiteIndex e.toMonoidHom L
44 haveI : S.FiniteIndex := by
45 apply Subgroup.finiteIndex_iff.2
46 rw [Subgroup.index_map_subtype]
47 exact mul_ne_zero
48 (Subgroup.FiniteIndex.index_ne_zero (H := L₀))
49 (Subgroup.FiniteIndex.index_ne_zero (H := φ.ker))
50 have hL₀TF : IsTorsionFreeGroup L₀ := by
51 intro x hxfin
52 have hxfinKer : IsOfFinOrder (x : φ.ker) := by
53 simpa using
54 (Submonoid.isOfFinOrder_coe
55 (H := L₀.toSubmonoid) (x := x)).2 hxfin
56 let y : L := ⟨e (x : φ.ker), x.2⟩
57 have hyfin : IsOfFinOrder y := by
58 have heyfin : IsOfFinOrder (e (x : φ.ker)) :=
59 MonoidHom.isOfFinOrder e.toMonoidHom hxfinKer
60 simpa [y] using
61 (Submonoid.isOfFinOrder_coe
62 (H := L.toSubmonoid) (x := y)).1 heyfin
63 have hyone : y = 1 := hLTF y hyfin
64 have heyone : e (x : φ.ker) = 1 :=
65 congrArg (fun z : L => (z : H)) hyone
66 have hxoneKer : (x : φ.ker) = 1 := by
67 apply e.injective
68 simpa using heyone
69 exact Subtype.ext hxoneKer
70 let eS : L₀ ≃* S :=
71 L₀.equivMapOfInjective φ.ker.subtype φ.ker.subtype_injective
72 have hSTF : IsTorsionFreeGroup S :=
73 isTorsionFreeGroup_of_mulEquiv eS hL₀TF
74 have hDerivedL₀ : derivedSeries φ.ker n ≤ L₀ := by
75 intro x hx
76 change e x ∈ L
77 have hxmap :
78 e x ∈ (derivedSeries φ.ker n).map e.toMonoidHom := by
79 exact ⟨x, hx, rfl⟩
80 have hxDer : e x ∈ derivedSeries H n := by
81 have hmapeq :
82 (derivedSeries φ.ker n).map e.toMonoidHom = derivedSeries H n :=
83 map_derivedSeries_eq (f := e.toMonoidHom) e.surjective n
84 rw [hmapeq] at hxmap
85 exact hxmap
86 exact hLQuot hxDer
87 have hFirstDerivedKer : derivedSeries G 1 ≤ φ.ker := by
88 simpa [derivedSeries_one] using Abelianization.commutator_subset_ker φ
89 have hDerivedS : derivedSeries G (n + 1) ≤ S := by
90 intro g hg
91 have hmap :
92 g ∈ (derivedSeries φ.ker n).map φ.ker.subtype :=
94 φ.ker hFirstDerivedKer n hg
95 rcases Subgroup.mem_map.mp hmap with ⟨x, hx, hxeq⟩
96 exact Subgroup.mem_map.mpr ⟨x, hDerivedL₀ hx, hxeq⟩
97 exact ⟨S, inferInstance, hSTF, hDerivedS⟩
100 {G H : Type*} [Group G] [Group H] {m : ℕ}
101 (e : G ≃* H)
102 (h : ∃ L : Subgroup H,
103 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
105 ∃ K : Subgroup G,
106 K.FiniteIndex ∧ IsTorsionFreeGroup K ∧
107 SubgroupQuotientHasDerivedLengthAtMost K m := by
108 rcases h with ⟨L, hLFiniteIndex, hLTF, hLQuot⟩
109 haveI : L.FiniteIndex := hLFiniteIndex
110 let K : Subgroup G := L.comap e.toMonoidHom
111 haveI : K.FiniteIndex := subgroup_finiteIndex_comap_of_finiteIndex e.toMonoidHom L
112 have hKTF : IsTorsionFreeGroup K := by
113 intro x hxfin
114 have hxfinG : IsOfFinOrder (x : G) := by
115 simpa using
116 (Submonoid.isOfFinOrder_coe
117 (H := K.toSubmonoid) (x := x)).2 hxfin
118 let y : L := ⟨e (x : G), x.2⟩
119 have hyfin : IsOfFinOrder y := by
120 have heyfin : IsOfFinOrder (e (x : G)) :=
121 MonoidHom.isOfFinOrder e.toMonoidHom hxfinG
122 simpa [y] using
123 (Submonoid.isOfFinOrder_coe
124 (H := L.toSubmonoid) (x := y)).1 heyfin
125 have hyone : y = 1 := hLTF y hyfin
126 have heyone : e (x : G) = 1 :=
127 congrArg (fun z : L => (z : H)) hyone
128 have hxoneG : (x : G) = 1 := by
129 apply e.injective
130 simpa using heyone
131 exact Subtype.ext hxoneG
132 have hKQuot : SubgroupQuotientHasDerivedLengthAtMost K m := by
133 intro g hg
134 change e g ∈ L
135 have hmap : e g ∈ (derivedSeries G m).map e.toMonoidHom := ⟨g, hg, rfl⟩
136 have hderH : e g ∈ derivedSeries H m :=
137 (map_derivedSeries_le_derivedSeries e.toMonoidHom m) hmap
138 exact hLQuot hderH
139 exact ⟨K, inferInstance, hKTF, hKQuot⟩
141end FenchelNielsen