FenchelNielsenZomorrodian/Discrete/Abelianization/EllipticAbelianization.lean
1import FenchelNielsenZomorrodian.Discrete.Abelianization.PeriodClassOrder
2import FenchelNielsenZomorrodian.Discrete.Core.EllipticCompact
3import FenchelNielsenZomorrodian.Discrete.Core.EllipticQuotientHom
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Abelianization/EllipticAbelianization.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Abelianization of compact Fuchsian presentations
16Finite cyclic coordinate calculations for elliptic generators, period classes, period quotients, and order formulas in compact Fuchsian abelianizations.
17-/
19open scoped BigOperators
21namespace FenchelNielsen
23def ellipticAbelianizationHom (σ : FuchsianSignature) :
24 FuchsianPresentedGroup σ →* Multiplicative (PeriodAbelianization σ) :=
26 (fun i => Multiplicative.ofAdd (periodClass σ i))
27 (by
28 intro i
29 simpa using congrArg Multiplicative.ofAdd (periodClass_nsmul_eq_zero σ i))
30 (by
31 simpa using congrArg Multiplicative.ofAdd (sum_periodClass_eq_zero σ))
33@[simp] theorem ellipticAbelianizationHom_elliptic
34 (σ : FuchsianSignature) (i : Fin σ.numPeriods) :
35 ellipticAbelianizationHom σ (ellipticElement σ i) =
36 Multiplicative.ofAdd (periodClass σ i) := by
40 {σ : FuchsianSignature} {i : Fin σ.numPeriods} :
41 orderOf (ellipticAbelianizationHom σ (ellipticElement σ i)) = σ.periods i ↔
42 σ.periods i ∣ otherPeriodsLcm σ.toFenchelSignature i := by
44 exact periodClass_orderOf_eq_period_iff (σ := σ) (i := i)
47 {σ : FuchsianSignature} :
48 (∀ i : Fin σ.numPeriods,
49 orderOf (ellipticAbelianizationHom σ (ellipticElement σ i)) = σ.periods i) ↔
50 LCMCondition σ.toFenchelSignature := by
51 constructor
52 · intro h i
53 exact (ellipticAbelianizationHom_elliptic_order_eq_period_iff (σ := σ) (i := i)).1 (h i)
54 · intro h i
55 exact (ellipticAbelianizationHom_elliptic_order_eq_period_iff (σ := σ) (i := i)).2 (h i)
58 (σ : FuchsianSignature) {A : Type*} [CommGroup A]
59 (φ : FuchsianPresentedGroup σ →* A) (i : Fin σ.numPeriods) :
60 φ (ellipticElement σ i) ^ otherPeriodsLcm σ.toFenchelSignature i = 1 := by
61 let ξ : Fin σ.numPeriods → A := fun j => φ (ellipticElement σ j)
62 have hpow : ∀ j : Fin σ.numPeriods, ξ j ^ σ.periods j = 1 := by
63 intro j
64 change φ (ellipticElement σ j) ^ σ.periods j = 1
65 rw [← map_pow, ellipticElement_pow_period_eq_one, map_one]
66 have hprod : ∏ j : Fin σ.numPeriods, ξ j = 1 := by
67 have hrel :
68 (∏ j : Fin σ.numPeriods, ξ j) *
69 (∏ j : Fin σ.orbitGenus,
72 = 1 := by
73 simpa [ξ, totalRelation, xWord, aWord, bWord, ellipticElement,
74 Fin.prod_univ_def, MonoidHom.map_mul, MonoidHom.map_list_prod] using
75 congrArg φ
77 (x := totalRelation σ) (Or.inr rfl))
78 have hcomm :
79 ∏ j : Fin σ.orbitGenus,
82 = 1 := by
83 refine Finset.prod_eq_one ?_
84 intro j hj
85 simpa [map_commutatorElement, commutatorElement_eq_one_iff_mul_comm] using
86 (mul_comm
89 rw [hcomm, mul_one] at hrel
90 exact hrel
91 let L := otherPeriodsLcm σ.toFenchelSignature i
92 have hsplit' : ((Finset.univ.erase i).prod ξ) * ξ i = 1 := by
93 calc
94 ((Finset.univ.erase i).prod ξ) * ξ i = ∏ j, ξ j := by
95 exact Finset.prod_erase_mul (s := Finset.univ) (f := ξ) (a := i) (Finset.mem_univ i)
96 _ = 1 := hprod
97 have hsplit : ξ i * ((Finset.univ.erase i).prod ξ) = 1 := by
98 simpa [mul_comm] using hsplit'
99 have hOthers :
100 ((Finset.univ.erase i).prod ξ) ^ L = 1 := by
101 rw [← Finset.prod_pow]
102 refine Finset.prod_eq_one ?_
103 intro j hj
104 obtain ⟨m, hm⟩ := Finset.dvd_lcm (s := Finset.univ.erase i) (f := σ.periods) hj
105 rw [show L = σ.periods j * m by simpa [L, otherPeriodsLcm] using hm,
106 pow_mul, hpow j, one_pow]
107 have hPow : ξ i ^ L = 1 := by
108 have hsplitPow := congrArg (fun a : A => a ^ L) hsplit
109 simp only at hsplitPow
110 rw [mul_pow, hOthers, mul_one] at hsplitPow
111 simpa [L] using hsplitPow
112 simpa [ξ, L] using hPow
115 (σ : FuchsianSignature) {A : Type*} [CommGroup A]
116 (φ : FuchsianPresentedGroup σ →* A) (i : Fin σ.numPeriods) :
117 orderOf (φ (ellipticElement σ i)) ∣
118 otherPeriodsLcm σ.toFenchelSignature i :=
119 orderOf_dvd_of_pow_eq_one
123 (σ : FuchsianSignature) {A : Type*} [CommGroup A]
124 (φ : FuchsianPresentedGroup σ →* A)
125 (hell : ∀ i : Fin σ.numPeriods,
126 orderOf (φ (ellipticElement σ i)) = σ.periods i) :
127 LCMCondition σ.toFenchelSignature := by
128 intro i
129 simpa [hell i] using
132end FenchelNielsen