Yamaguchi Lean 4 Library
FenchelNielsenZomorrodian/Discrete/FiniteIndex/Definitions.lean
FenchelNielsenZomorrodian/Discrete/FiniteIndex/Definitions/Source

FenchelNielsenZomorrodian/Discrete/FiniteIndex/Definitions.lean

1import FenchelNielsenZomorrodian.Discrete.GroupTheory.DerivedSeries
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/FiniteIndex/Definitions.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 (H : Subgroup G) (m : ℕ) : Prop :=
21 derivedSeries G m ≤ H
24 (G : Type*) [Group G] (m : ℕ) : Prop :=
25 ∃ H : Subgroup G,
26 H.FiniteIndex ∧ H.Normal ∧ IsTorsionFreeGroup H ∧
30 (G : Type*) [Group G] (m : ℕ) : Prop :=
31 ∃ H : Subgroup G,
32 H.FiniteIndex ∧ IsTorsionFreeGroup H ∧
36 {G : Type*} [Group G] {H : Subgroup G} {m n : ℕ}
37 (hmn : m ≤ n)
40 intro g hg
41 exact h ((derivedSeries_antitone G hmn) hg)
44 {G : Type*} [Group G] {m n : ℕ} (hmn : m ≤ n)
47 rcases h with ⟨H, hHFiniteIndex, hHTF, hHQuot⟩
48 exact ⟨H, hHFiniteIndex, hHTF,
51end FenchelNielsen