FenchelNielsenZomorrodian/Discrete/FiniteIndex/NormalCore.lean
1import FenchelNielsenZomorrodian.Discrete.FiniteIndex.Definitions
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/FiniteIndex/NormalCore.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 : Type*} [Group G] {H K : Subgroup G}
21 (hHK : H ≤ K) (hK : IsTorsionFreeGroup K) :
22 IsTorsionFreeGroup H := by
23 intro h hhfin
24 have hhfinG : IsOfFinOrder (h : G) := by
25 simpa using
26 (Submonoid.isOfFinOrder_coe
27 (H := H.toSubmonoid) (x := h)).2 hhfin
28 let k : K := ⟨h, hHK h.2⟩
29 have hkfin : IsOfFinOrder k := by
30 simpa [k] using
31 (Submonoid.isOfFinOrder_coe
32 (H := K.toSubmonoid) (x := k)).1 hhfinG
33 have hkone : k = 1 := hK k hkfin
34 have hkoneG : ((k : K) : G) = 1 :=
35 congrArg (fun x : K => (x : G)) hkone
36 exact Subtype.ext (by simpa [k] using hkoneG)
39 {G : Type*} [Group G] {m : ℕ}
40 (H : Subgroup G) [H.FiniteIndex]
41 (hTF : IsTorsionFreeGroup H)
42 (hDerived : derivedSeries G m ≤ H) :
44 let K : Subgroup G := H.normalCore
45 haveI : K.FiniteIndex := Subgroup.finiteIndex_normalCore (H := H)
46 have hKTF : IsTorsionFreeGroup K :=
47 isTorsionFreeGroup_of_subgroup_le (Subgroup.normalCore_le H) hTF
48 have hDerivedK : derivedSeries G m ≤ K := by
49 haveI : (derivedSeries G m).Normal := derivedSeries_normal G m
50 exact
51 (Subgroup.normal_le_normalCore
52 (H := H) (N := derivedSeries G m)).2 hDerived
53 exact ⟨K, inferInstance, inferInstance, hKTF, hDerivedK⟩
55end FenchelNielsen