FenchelNielsenZomorrodian/Discrete/Abelianization/PeriodClassOrder.lean
1import FenchelNielsenZomorrodian.Discrete.Abelianization.PeriodCoordinate
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Abelianization/PeriodClassOrder.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Abelianization of compact Fuchsian presentations
14Finite cyclic coordinate calculations for elliptic generators, period classes, period quotients, and order formulas in compact Fuchsian abelianizations.
15-/
17namespace FenchelNielsen
20 (σ : FuchsianSignature) (i : Fin σ.numPeriods) {n : ℕ}
21 (hzero : n • periodClass σ i = 0) :
22 Nat.gcd (σ.periods i) (otherPeriodsLcm σ.toFenchelSignature i) ∣ n := by
23 classical
24 let L := otherPeriodsLcm σ.toFenchelSignature i
25 let d := Nat.gcd (σ.periods i) L
26 have hmem : n • periodBasisVector σ i ∈ periodRelation σ := by
27 simpa using
28 (QuotientAddGroup.eq_iff_sub_mem (N := periodRelation σ)
29 (x := n • periodBasisVector σ i) (y := 0)).1 <| by
30 simpa [periodClass] using hzero
31 change n • periodBasisVector σ i ∈ AddSubgroup.zmultiples (periodDiagonal σ) at hmem
32 rcases hmem with ⟨z, hz⟩
33 have hOthers :
34 ∀ j ∈ (Finset.univ.erase i : Finset (Fin σ.numPeriods)),
35 σ.periods j ∣ Int.natAbs z := by
36 intro j hj
37 have hji : j ≠ i := (Finset.mem_erase.mp hj).1
38 have hcoord : (z : ZMod (σ.periods j)) = 0 := by
39 have := congrArg (fun v : PeriodCoordinate σ => v j) hz
40 simpa [periodDiagonal, periodBasisVector, zmodBasisVector, hji] using this
41 have hzdiv : (σ.periods j : ℤ) ∣ z := by
42 exact (ZMod.intCast_zmod_eq_zero_iff_dvd z (σ.periods j)).mp hcoord
43 exact Int.natCast_dvd.mp hzdiv
44 have hLzNat : L ∣ Int.natAbs z := by
45 exact Finset.lcm_dvd hOthers
46 have hdzNat : d ∣ Int.natAbs z :=
47 (Nat.gcd_dvd_right (σ.periods i) L).trans hLzNat
48 have hdzInt : (d : ℤ) ∣ z := by
49 exact Int.natCast_dvd.mpr hdzNat
50 have hdaNat : d ∣ σ.periods i := Nat.gcd_dvd_left (σ.periods i) L
51 have hdaInt : (d : ℤ) ∣ (σ.periods i : ℤ) := by
52 exact Int.natCast_dvd_natCast.mpr hdaNat
53 have hcoordi :
54 ((n : ℤ) : ZMod (σ.periods i)) = (z : ZMod (σ.periods i)) := by
55 have := congrArg (fun v : PeriodCoordinate σ => v i) hz
56 simpa [periodDiagonal, periodBasisVector, zmodBasisVector] using this.symm
57 have hdiff : (σ.periods i : ℤ) ∣ z - (n : ℤ) := by
58 exact
59 (ZMod.intCast_eq_intCast_iff_dvd_sub (n : ℤ) z (σ.periods i)).mp hcoordi
60 have hdDiff : (d : ℤ) ∣ z - (n : ℤ) := hdaInt.trans hdiff
61 have hdNInt : (d : ℤ) ∣ (n : ℤ) := by
62 have hsub : (d : ℤ) ∣ z - (z - (n : ℤ)) := dvd_sub hdzInt hdDiff
63 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using hsub
64 exact Int.natCast_dvd_natCast.mp hdNInt
66theorem periodClass_addOrderOf_eq_gcd
67 (σ : FuchsianSignature) (i : Fin σ.numPeriods) :
68 addOrderOf (periodClass σ i) =
69 Nat.gcd (σ.periods i) (otherPeriodsLcm σ.toFenchelSignature i) := by
70 apply Nat.dvd_antisymm
71 · exact Nat.dvd_gcd
72 ((addOrderOf_dvd_iff_nsmul_eq_zero).2 (periodClass_nsmul_eq_zero σ i))
73 ((addOrderOf_dvd_iff_nsmul_eq_zero).2
75 · exact gcd_period_otherLcm_dvd_of_nsmul_periodClass_eq_zero σ i (by simp only [addOrderOf_nsmul_eq_zero])
78 {σ : FuchsianSignature} {i : Fin σ.numPeriods} :
79 addOrderOf (periodClass σ i) = σ.periods i ↔
80 σ.periods i ∣ otherPeriodsLcm σ.toFenchelSignature i := by
82 exact Nat.gcd_eq_left_iff_dvd
85 {σ : FuchsianSignature} {i : Fin σ.numPeriods} :
86 orderOf (Multiplicative.ofAdd (periodClass σ i)) = σ.periods i ↔
87 σ.periods i ∣ otherPeriodsLcm σ.toFenchelSignature i := by
88 rw [orderOf_ofAdd_eq_addOrderOf]
89 exact periodClass_addOrderOf_eq_period_iff (σ := σ) (i := i)
92 (σ : FuchsianSignature) (hLCM : LCMCondition σ.toFenchelSignature)
93 (i : Fin σ.numPeriods) :
94 addOrderOf (periodClass σ i) = σ.periods i :=
95 (periodClass_addOrderOf_eq_period_iff (σ := σ) (i := i)).2 (hLCM i)
97theorem periodClass_orderOf_eq_period
98 (σ : FuchsianSignature) (hLCM : LCMCondition σ.toFenchelSignature)
99 (i : Fin σ.numPeriods) :
100 orderOf (Multiplicative.ofAdd (periodClass σ i)) = σ.periods i :=
101 (periodClass_orderOf_eq_period_iff (σ := σ) (i := i)).2 (hLCM i)
103end FenchelNielsen