FenchelNielsenZomorrodian/Profinite/LowPeriodQuotient.lean
1import FenchelNielsenZomorrodian.Profinite.SmoothQuotient
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Profinite/LowPeriodQuotient.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Low-period compact quotients
14Handles compact zero-genus boundary cases with two periods by constructing the required cyclic smooth quotient.
15-/
17namespace FenchelNielsen
19universe u
21namespace ProfiniteFGroup
23noncomputable def twoPeriodIndexZero
24 (Δ : ProfiniteFGroup.{u}) (hTwo : Δ.signature.numPeriods = 2) :
25 Fin Δ.signature.numPeriods :=
26 Fin.cast hTwo.symm (0 : Fin 2)
28noncomputable def twoPeriodIndexOne
29 (Δ : ProfiniteFGroup.{u}) (hTwo : Δ.signature.numPeriods = 2) :
30 Fin Δ.signature.numPeriods :=
31 Fin.cast hTwo.symm (1 : Fin 2)
33/-- With two periods, the inertia part of the total relation is the product of the two indexed
34inertia generators. -/
35theorem twoPeriod_inertia_list_product
36 (Δ : ProfiniteFGroup.{u}) (hTwo : Δ.signature.numPeriods = 2) :
37 ((List.finRange Δ.signature.numPeriods).map fun k => Δ.inertia k).prod =
38 Δ.inertia (twoPeriodIndexZero Δ hTwo) *
39 Δ.inertia (twoPeriodIndexOne Δ hTwo) := by
40 cases Δ with
43 cases sig with
45 dsimp at hTwo ⊢
46 subst numPeriods
47 norm_num [twoPeriodIndexZero, twoPeriodIndexOne, List.finRange]
49/-- In the compact zero-genus two-period case, the two inertia generators multiply to one. -/
50theorem twoPeriod_inertia_mul_eq_one
51 (Δ : ProfiniteFGroup.{u})
52 (hCompact : Δ.signature.IsCompact)
53 (hZero : Δ.signature.orbitGenus = 0)
54 (hTwo : Δ.signature.numPeriods = 2) :
55 Δ.inertia (twoPeriodIndexZero Δ hTwo) *
56 Δ.inertia (twoPeriodIndexOne Δ hTwo) = 1 := by
57 have hrel := Δ.presentation_relation
58 have hSurface :
59 ((List.finRange Δ.signature.orbitGenus).map fun i =>
60 ⁅Δ.surfaceA i, Δ.surfaceB i⁆).prod = 1 := by
61 apply List.prod_eq_one
62 intro x hx
63 rcases List.mem_map.mp hx with ⟨j, _hj, rfl⟩
64 exfalso
65 rw [hZero] at j
66 exact Nat.not_lt_zero _ j.2
67 have hCusp :
68 ((List.finRange Δ.signature.numCusps).map fun j => Δ.cusp j).prod = 1 := by
69 apply List.prod_eq_one
70 intro x hx
71 rcases List.mem_map.mp hx with ⟨j, _hj, rfl⟩
72 exfalso
73 rw [hCompact] at j
74 exact Nat.not_lt_zero _ j.2
75 rw [profiniteFenchelTotalRelation, hSurface, hCusp, one_mul, one_mul,
76 twoPeriod_inertia_list_product Δ hTwo] at hrel
77 exact hrel
79/-- In the compact zero-genus two-period case, the two periods are equal. -/
80theorem twoPeriod_periods_eq
81 (Δ : ProfiniteFGroup.{u})
82 (hCompact : Δ.signature.IsCompact)
83 (hZero : Δ.signature.orbitGenus = 0)
84 (hTwo : Δ.signature.numPeriods = 2) :
85 Δ.signature.periods (twoPeriodIndexZero Δ hTwo) =
86 Δ.signature.periods (twoPeriodIndexOne Δ hTwo) := by
87 have hmul := twoPeriod_inertia_mul_eq_one Δ hCompact hZero hTwo
88 calc
89 Δ.signature.periods (twoPeriodIndexZero Δ hTwo) =
90 orderOf (Δ.inertia (twoPeriodIndexZero Δ hTwo)) := by
91 rw [Δ.inertia_order]
92 _ = orderOf (Δ.inertia (twoPeriodIndexOne Δ hTwo)) := by
93 rw [eq_inv_of_mul_eq_one_left hmul, orderOf_inv]
94 _ = Δ.signature.periods (twoPeriodIndexOne Δ hTwo) := by
95 rw [Δ.inertia_order]
97instance instTopologicalSpaceMultiplicativeZMod (n : ℕ) :
98 TopologicalSpace (Multiplicative (ZMod n)) :=
99 ⊥
101instance instDiscreteTopologyMultiplicativeZMod (n : ℕ) :
102 DiscreteTopology (Multiplicative (ZMod n)) :=
103 ⟨rfl⟩
105noncomputable instance instFintypeMultiplicativeZMod (n : ℕ) [NeZero n] :
106 Fintype (Multiplicative (ZMod n)) :=
107 Fintype.ofEquiv (ZMod n) Multiplicative.toAdd
109noncomputable instance instFiniteMultiplicativeZMod (n : ℕ) [NeZero n] :
110 Finite (Multiplicative (ZMod n)) :=
111 Finite.of_fintype _
113noncomputable instance instFiniteULiftMultiplicativeZMod (n : ℕ) [NeZero n] :
114 Finite (ULift.{u, 0} (Multiplicative (ZMod n))) := by
115 infer_instance
117noncomputable def twoPeriodCyclicGeneratorImageCore
118 (Δ : ProfiniteFGroup.{u}) (hTwo : Δ.signature.numPeriods = 2) :
119 ProfiniteFenchelGeneratorIndex.{u} Δ.signature →
120 Multiplicative
121 (ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))
122 | ULift.up (.inertia k) =>
123 if (Fin.cast hTwo k).val = 0 then
124 Multiplicative.ofAdd (1 :
125 ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))
126 else
127 (Multiplicative.ofAdd (1 :
128 ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo))))⁻¹
129 | ULift.up (.surfaceA _) => 1
130 | ULift.up (.surfaceB _) => 1
131 | ULift.up (.cusp _) => 1
133noncomputable def twoPeriodCyclicGeneratorImage
134 (Δ : ProfiniteFGroup.{u}) (hTwo : Δ.signature.numPeriods = 2) :
135 ProfiniteFenchelGeneratorIndex.{u} Δ.signature →
136 ULift.{u, 0}
137 (Multiplicative
138 (ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))) :=
139 fun x => ULift.up (twoPeriodCyclicGeneratorImageCore Δ hTwo x)
141private theorem twoPeriodCyclicGeneratorImage_total_relation
142 (Δ : ProfiniteFGroup.{u})
143 (hCompact : Δ.signature.IsCompact)
144 (hZero : Δ.signature.orbitGenus = 0)
145 (hTwo : Δ.signature.numPeriods = 2) :
147 (fun i => twoPeriodCyclicGeneratorImageCore Δ hTwo
148 (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
149 (fun i => twoPeriodCyclicGeneratorImageCore Δ hTwo
150 (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
151 (fun j => twoPeriodCyclicGeneratorImageCore Δ hTwo
152 (ULift.up (ProfiniteFenchelGenerator.cusp j)))
153 (fun k => twoPeriodCyclicGeneratorImageCore Δ hTwo
154 (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1 := by
155 cases Δ with
158 cases sig with
160 dsimp [FenchelSignature.IsCompact] at hCompact
161 dsimp at hZero hTwo ⊢
162 subst orbitGenus
163 subst numCusps
164 subst numPeriods
167 simp only [List.finRange_zero, List.map_nil, List.prod_nil, one_mul]
168 change
169 ((List.finRange 2).map fun k : Fin 2 =>
170 if k = 0 then
171 Multiplicative.ofAdd (1 : ZMod (periods 0))
172 else
173 (Multiplicative.ofAdd (1 : ZMod (periods 0)))⁻¹).prod = 1
174 norm_num [List.finRange]
176private theorem twoPeriodCyclicGeneratorImage_lifted_total_relation
177 (Δ : ProfiniteFGroup.{u})
178 (hCompact : Δ.signature.IsCompact)
179 (hZero : Δ.signature.orbitGenus = 0)
180 (hTwo : Δ.signature.numPeriods = 2) :
182 (fun i => twoPeriodCyclicGeneratorImage Δ hTwo
183 (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
184 (fun i => twoPeriodCyclicGeneratorImage Δ hTwo
185 (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
186 (fun j => twoPeriodCyclicGeneratorImage Δ hTwo
187 (ULift.up (ProfiniteFenchelGenerator.cusp j)))
188 (fun k => twoPeriodCyclicGeneratorImage Δ hTwo
189 (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1 := by
190 apply
191 (MulEquiv.ulift :
192 ULift.{u, 0}
193 (Multiplicative
194 (ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))) ≃*
195 Multiplicative
196 (ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))).injective
198 map_list_prod, Function.comp_def, map_commutatorElement] using
199 twoPeriodCyclicGeneratorImage_total_relation Δ hCompact hZero hTwo
201private theorem twoPeriodCyclicGeneratorImage_period_relation
202 (Δ : ProfiniteFGroup.{u})
203 (hCompact : Δ.signature.IsCompact)
204 (hZero : Δ.signature.orbitGenus = 0)
205 (hTwo : Δ.signature.numPeriods = 2)
206 (k : Fin Δ.signature.numPeriods) :
208 (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
209 Δ.signature.periods k = 1 := by
210 have hEq := twoPeriod_periods_eq Δ hCompact hZero hTwo
211 cases Δ with
214 cases sig with
216 dsimp at hCompact hZero hTwo hEq k ⊢
217 subst numPeriods
218 fin_cases k
219 · have horder :
220 orderOf
221 (Multiplicative.ofAdd (1 : ZMod (periods 0))) =
222 periods 0 := by
223 rw [orderOf_ofAdd_eq_addOrderOf, ZMod.addOrderOf_one]
225 horder] using
226 pow_orderOf_eq_one
227 (Multiplicative.ofAdd (1 : ZMod (periods 0)))
228 · have h10 : periods 1 = periods 0 := by
229 simpa [twoPeriodIndexZero, twoPeriodIndexOne] using hEq.symm
230 have horder :
231 orderOf
232 ((Multiplicative.ofAdd (1 : ZMod (periods 0)))⁻¹) =
233 periods 1 := by
234 rw [orderOf_inv, orderOf_ofAdd_eq_addOrderOf,
235 ZMod.addOrderOf_one, h10]
237 horder] using
238 pow_orderOf_eq_one
239 ((Multiplicative.ofAdd (1 : ZMod (periods 0)))⁻¹)
241private theorem twoPeriodCyclicGeneratorImage_lifted_period_relation
242 (Δ : ProfiniteFGroup.{u})
243 (hCompact : Δ.signature.IsCompact)
244 (hZero : Δ.signature.orbitGenus = 0)
245 (hTwo : Δ.signature.numPeriods = 2)
246 (k : Fin Δ.signature.numPeriods) :
247 twoPeriodCyclicGeneratorImage Δ hTwo
248 (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
249 Δ.signature.periods k = 1 := by
250 apply
251 (MulEquiv.ulift :
252 ULift.{u, 0}
253 (Multiplicative
254 (ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))) ≃*
255 Multiplicative
256 (ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))).injective
257 simpa [twoPeriodCyclicGeneratorImage] using
258 twoPeriodCyclicGeneratorImage_period_relation Δ hCompact hZero hTwo k
260private theorem twoPeriodCyclicGeneratorImage_inertia_order
261 (Δ : ProfiniteFGroup.{u})
262 (hCompact : Δ.signature.IsCompact)
263 (hZero : Δ.signature.orbitGenus = 0)
264 (hTwo : Δ.signature.numPeriods = 2)
265 (k : Fin Δ.signature.numPeriods) :
266 orderOf
267 (twoPeriodCyclicGeneratorImageCore Δ hTwo
268 (ULift.up (ProfiniteFenchelGenerator.inertia k))) =
269 Δ.signature.periods k := by
270 have hEq := twoPeriod_periods_eq Δ hCompact hZero hTwo
271 cases Δ with
274 cases sig with
276 dsimp at hCompact hZero hTwo hEq k ⊢
277 subst numPeriods
278 fin_cases k
279 · simp only [twoPeriodIndexZero, Fin.isValue, Fin.cast_eq_self, twoPeriodCyclicGeneratorImageCore, Fin.zero_eta,
280 Fin.coe_ofNat_eq_mod, Nat.zero_mod, ↓reduceIte, orderOf_ofAdd_eq_addOrderOf, ZMod.addOrderOf_one]
281 · have h10 : periods 1 = periods 0 := by
282 simpa [twoPeriodIndexZero, twoPeriodIndexOne] using hEq.symm
283 simp only [twoPeriodIndexZero, Fin.isValue, Fin.cast_eq_self, twoPeriodCyclicGeneratorImageCore, Fin.mk_one,
284 Fin.coe_ofNat_eq_mod, Nat.mod_succ, one_ne_zero, ↓reduceIte, orderOf_inv, orderOf_ofAdd_eq_addOrderOf,
285 ZMod.addOrderOf_one, h10]
287private theorem twoPeriodCyclicGeneratorImage_lifted_inertia_order
288 (Δ : ProfiniteFGroup.{u})
289 (hCompact : Δ.signature.IsCompact)
290 (hZero : Δ.signature.orbitGenus = 0)
291 (hTwo : Δ.signature.numPeriods = 2)
292 (k : Fin Δ.signature.numPeriods) :
293 orderOf
294 (twoPeriodCyclicGeneratorImage Δ hTwo
295 (ULift.up (ProfiniteFenchelGenerator.inertia k))) =
296 Δ.signature.periods k := by
297 have horder :=
298 orderOf_injective
299 ((MulEquiv.ulift :
300 ULift.{u, 0}
301 (Multiplicative
302 (ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))) ≃*
303 Multiplicative
304 (ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))).toMonoidHom)
305 (MulEquiv.ulift :
306 ULift.{u, 0}
307 (Multiplicative
308 (ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))) ≃*
309 Multiplicative
310 (ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))).injective
311 (twoPeriodCyclicGeneratorImage Δ hTwo
312 (ULift.up (ProfiniteFenchelGenerator.inertia k)))
313 rw [← horder]
314 exact twoPeriodCyclicGeneratorImage_inertia_order Δ hCompact hZero hTwo k
316noncomputable def twoPeriodCyclicSmoothQuotientData
317 (Δ : ProfiniteFGroup.{u})
318 (hCompact : Δ.signature.IsCompact)
319 (hZero : Δ.signature.orbitGenus = 0)
320 (hTwo : Δ.signature.numPeriods = 2) :
321 ProfiniteSmoothQuotientData Δ 1 :=
322 have hpos :
323 0 < Δ.signature.periods (twoPeriodIndexZero Δ hTwo) :=
324 lt_of_lt_of_le (by decide : 0 < 2)
325 (Δ.signature.period_ge_two (twoPeriodIndexZero Δ hTwo))
326 letI : NeZero (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)) :=
327 ⟨Nat.pos_iff_ne_zero.mp hpos⟩
328 ProfiniteSmoothQuotientData.ofPresentationLiftToFiniteOfRelations
329 Δ (twoPeriodCyclicGeneratorImage Δ hTwo)
331 Δ hCompact hZero hTwo)
333 Δ hCompact hZero hTwo)
335 (ULift.{u, 0}
336 (Multiplicative
337 (ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo))))))
339 Δ hCompact hZero hTwo)
343end FenchelNielsen