FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/Perfectness.lean
1import FenchelNielsenZomorrodian.Discrete.Abelianization.EllipticAbelianization
2import FenchelNielsenZomorrodian.Discrete.Arithmetic.PrimeDivisors
3import FenchelNielsenZomorrodian.Discrete.GroupTheory.Basic
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/Perfectness.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
16Organizes first and second reduction data, perfectness numerics, reindexing, cleanup data, and the final zero-genus three-step finite-index theorem.
17-/
19open scoped BigOperators
21namespace FenchelNielsen
23private theorem hom_trivial_of_zeroGenus_pairwiseCoprime
24 (σ : FuchsianSignature) (hZero : σ.orbitGenus = 0)
25 (hPair :
26 ∀ i j : Fin σ.numPeriods, i ≠ j → Nat.Coprime (σ.periods i) (σ.periods j))
27 {A : Type*} [CommGroup A] (φ : FuchsianPresentedGroup σ →* A) :
28 φ = 1 := by
29 apply PresentedGroup.ext
30 intro x
31 cases x with
32 | elliptic i =>
33 let ξ : Fin σ.numPeriods → A := fun j => φ (ellipticElement σ j)
34 have hpow : ∀ j : Fin σ.numPeriods, ξ j ^ σ.periods j = 1 := by
35 intro j
36 simpa [ξ, ellipticElement, xWord, MonoidHom.map_pow] using
37 congrArg φ
40 let L := otherPeriodsLcm σ.toFenchelSignature i
41 have hPow : ξ i ^ L = 1 := by
42 simpa [ξ, L] using
44 have hCoprimeProd :
45 Nat.Coprime (σ.periods i)
46 ((Finset.univ.erase i : Finset (Fin σ.numPeriods)).prod σ.periods) := by
47 rw [Nat.coprime_prod_right_iff]
48 intro j hj
49 exact hPair i j (Finset.mem_erase.mp hj).1.symm
50 have hLDiv :
51 L ∣ (Finset.univ.erase i : Finset (Fin σ.numPeriods)).prod σ.periods := by
52 dsimp [L, otherPeriodsLcm]
53 exact Finset.lcm_dvd (fun j hj => Finset.dvd_prod_of_mem _ hj)
54 have hCoprime : Nat.Coprime (σ.periods i) L := hCoprimeProd.of_dvd_right hLDiv
55 have hOrder :
56 orderOf (ξ i) = 1 := by
57 exact Nat.eq_one_of_dvd_coprimes hCoprime
58 (orderOf_dvd_of_pow_eq_one (hpow i))
59 (orderOf_dvd_of_pow_eq_one hPow)
60 exact orderOf_eq_one_iff.mp hOrder
61 | surfaceA j =>
62 exfalso
63 rw [hZero] at j
64 exact Nat.not_lt_zero _ j.2
65 | surfaceB j =>
66 exfalso
67 rw [hZero] at j
68 exact Nat.not_lt_zero _ j.2
70theorem FuchsianSignature.isPerfect_of_zeroGenus_pairwiseCoprime
71 (σ : FuchsianSignature) (hZero : σ.orbitGenus = 0)
72 (hPair :
73 ∀ i j : Fin σ.numPeriods, i ≠ j → Nat.Coprime (σ.periods i) (σ.periods j)) :
74 IsPerfectGroup (FuchsianPresentedGroup σ) := by
75 rw [IsPerfectGroup, derivedSeries_one]
76 apply top_le_iff.mp
77 intro g hg
78 rw [← Abelianization.ker_of (G := FuchsianPresentedGroup σ), MonoidHom.mem_ker]
79 have htriv :
80 (Abelianization.of :
81 FuchsianPresentedGroup σ →* Abelianization (FuchsianPresentedGroup σ)) = 1 :=
82 hom_trivial_of_zeroGenus_pairwiseCoprime σ hZero hPair Abelianization.of
83 simpa using congrArg
84 (fun f : FuchsianPresentedGroup σ →* Abelianization (FuchsianPresentedGroup σ) => f g) htriv
87 (σ : FuchsianSignature) (hZero : σ.orbitGenus = 0)
88 (hNonperfect : ¬ IsPerfectGroup (FuchsianPresentedGroup σ)) :
89 ∃ p : ℕ, p.Prime ∧
90 ∃ i j : Fin σ.numPeriods, i ≠ j ∧ p ∣ σ.periods i ∧ p ∣ σ.periods j := by
91 exact (not_pairwiseCoprimeFamily_iff_exists_prime_dvd_two (periods := σ.periods)).mp <| by
92 intro hPair
93 exact hNonperfect (FuchsianSignature.isPerfect_of_zeroGenus_pairwiseCoprime σ hZero hPair)
95end FenchelNielsen