Yamaguchi Lean 4 Library
FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/KernelEquivalence.lean
FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/KernelEquivalence/Source

FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/KernelEquivalence.lean

1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.RelatorProofs
2import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Relators.SourceHead
3import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Relators.SourceMiddleTail
4import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Relators.SourceTotal
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/KernelEquivalence.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Second compact zero-genus reduction
17The second explicit reduction step, with ordered target signatures, transport maps, source and target relator calculations, and quotient-basis comparison.
18-/
20namespace FenchelNielsen
22 {tailLen p q : ℕ}
23 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
24 (hp : 2 ≤ p) (hq : 2 ≤ q)
25 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
26 (htail : ∀ j, 2 ≤ tail j) : Type :=
27 (letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
28 let σ :=
30 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
31 let τ :=
33 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
34 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
35 let e :=
37 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
38 let hrels :=
40 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
45 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
46 (rels := relators σ)
48 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)))
50 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)
52 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
54 {tailLen p q : ℕ}
55 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
56 (hp : 2 ≤ p) (hq : 2 ≤ q)
57 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
58 (htail : ∀ j, 2 ≤ tail j)
59 (hMapsRelators :
60 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
61 let σ :=
63 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
64 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
65 let e :=
67 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
68 let η :=
70 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
71 ∀ r ∈
75 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
76 (rels := relators σ)
78 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)),
79 η r ∈ Subgroup.normalClosure
81 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail))
82 (hInvGenerators :
83 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
84 let σ :=
86 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
87 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
88 let e :=
90 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
91 let θ :=
93 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
94 let η :=
96 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
99 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)),
100 θ (η (FreeGroup.of z)) * (FreeGroup.of z)⁻¹ ∈
101 Subgroup.normalClosure
105 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
106 (rels := relators σ)
108 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))))
109 :
111 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail := by
112 classical
113 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
114 let σ :=
116 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
117 let τ :=
119 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
120 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
121 let e :=
123 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
124 let hrels :=
126 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
127 let θ :=
129 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
130 let η :=
132 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
133 let R :=
137 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
138 (rels := relators σ)
140 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
141 let F : FreeGroup ↥(schreierGeneratorSet
143 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)) →*
146 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)) :=
147 θ.comp η
148 refine
149 { toHom := η
150 mapsRelators := ?_
151 inv_toHom := ?_
152 to_invHom := ?_ }
153 · intro r hr
154 simpa [SecondReductionCanonicalTransportBlockForwardMapData, σ, τ, e, hrels, η] using
155 hMapsRelators r hr
156 · intro x
157 simpa [SecondReductionCanonicalTransportBlockForwardMapData, R, F, σ, τ, e, hrels, θ, η] using
158 ReidemeisterSchreier.Discrete.Presentations.freeGroup_endomorph_mul_inv_mem_normalClosure_of_generator_mul_inv
159 R F
160 (by
161 intro z
162 simpa [R, F, σ, e, hrels, θ, η] using hInvGenerators z)
163 x
164 · intro y
167 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y
169 {tailLen p q : ℕ}
170 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
171 (hp : 2 ≤ p) (hq : 2 ≤ q)
172 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
173 (htail : ∀ j, 2 ≤ tail j)
174 (hMapsRelators :
175 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
176 let σ :=
178 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
179 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
180 let e :=
182 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
183 let η :=
185 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
186 ∀ r ∈
190 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
191 (rels := relators σ)
193 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)),
194 η r ∈ Subgroup.normalClosure
196 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail))
197 :
199 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail := by
200 classical
201 refine
203 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
204 hMapsRelators ?_
205 dsimp
206 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
207 let σ :=
209 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
210 let φ :=
212 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
213 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
214 let e :=
216 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
217 let hrels :=
219 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
220 let hT :=
222 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
223 let θ :=
225 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
226 let η :=
228 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
229 let R :=
233 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
234 (rels := relators σ)
236 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
237 intro z
238 rcases
240 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail z with
241 hFirst | hSecond | hZero
242 · let zFirst : ↥(schreierGeneratorSet hT) :=
244 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail,
246 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail⟩
247 have hz : z = zFirst := Subtype.ext hFirst
248 subst z
249 let τ :=
251 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
252 let A :=
254 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))
256 have hzWord :
257 e.symm
259 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) =
260 (FreeGroup.of zFirst)⁻¹ := by
261 simpa [σ, φ, hT, e, zFirst] using
263 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail zFirst
264 have hηA : η (FreeGroup.of zFirst) = A⁻¹ := by
265 have h :=
267 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
268 have h' := congrArg Inv.inv h
269 simpa [σ, e, η, A, hzWord] using h'
270 have hθA :
271 θ A =
272 e.symm
274 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) := by
275 simpa [σ, τ, e, θ, A] using
277 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
278 have hθ : θ (η (FreeGroup.of zFirst)) = FreeGroup.of zFirst := by
279 calc
280 θ (η (FreeGroup.of zFirst)) = θ A⁻¹ := by rw [hηA]
281 _ = (θ A)⁻¹ := by simp only [Lean.Elab.WF.paramLet, map_inv]
282 _ =
283 (e.symm
285 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))⁻¹ := by
286 rw [hθA]
287 _ = ((FreeGroup.of zFirst)⁻¹)⁻¹ := by rw [hzWord]
288 _ = FreeGroup.of zFirst := by simp only [inv_inv]
289 rw [hθ]
290 simp only [mul_inv_cancel, one_mem]
291 · rcases hSecond with ⟨k, hz⟩
292 let zSecond : ↥(schreierGeneratorSet hT) :=
294 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k,
296 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k⟩
297 have hz' : z = zSecond := Subtype.ext hz
298 subst z
299 simpa [R, σ, e, hrels, hT, θ, η, zSecond] using
301 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k
302 · rcases hZero with ⟨y, hy, k, hz⟩
303 let x : FuchsianGenerator σ :=
305 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
306 have hxy : x ≠ y := by
307 intro hEq
308 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
309 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
310 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
311 have hyx : φ (FreeGroup.of x) = 1 := by
312 simpa [hEq] using hy
313 have hOne : (Multiplicative.ofAdd (1 : ZMod q)) = 1 := hx.symm.trans hyx
314 have hZ : (1 : ZMod q) = 0 := Multiplicative.ofAdd.injective hOne
315 have hval := congrArg ZMod.val hZ
316 letI : Fact (1 < q) := ⟨lt_of_lt_of_le (by decide : 1 < 2) hq⟩
317 rw [ZMod.val_one] at hval
318 simp only [ZMod.val_zero, one_ne_zero] at hval
319 let zZero : ↥(schreierGeneratorSet hT) :=
321 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k,
323 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k hxy⟩
324 have hz' : z = zZero := Subtype.ext hz
325 subst z
326 simpa [R, σ, φ, e, hrels, x, hT, θ, η, zZero] using
328 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k hxy
330 {tailLen p q : ℕ}
331 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
332 (hp : 2 ≤ p) (hq : 2 ≤ q)
333 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
334 (htail : ∀ j, 2 ≤ tail j)
335 (D :
337 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) :
339 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).ker ≃*
340 PresentedGroup
342 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by
343 classical
344 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
345 let σ :=
347 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
348 let τ :=
350 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
351 let ξ :=
353 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
354 let hpow : ∀ i, ξ i ^ σ.periods i = 1 :=
356 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
357 let hprod : ∏ i : Fin σ.numPeriods, ξ i = 1 :=
359 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
360 let i₀ : Fin σ.numPeriods :=
362 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨0, by omega⟩
363 have hi₀ : ξ i₀ = Multiplicative.ofAdd (1 : ZMod q) := by
365 ↓reduceIte, ξ, i₀]
366 let e :=
368 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
369 let R :=
373 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
374 (rels := relators σ)
376 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
377 let S : Set (FreeGroup (FuchsianGenerator τ)) :=
379 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail
380 let θ :=
382 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
383 have hTarget :
384 ∀ s ∈ S, θ s ∈ Subgroup.normalClosure R := by
385 intro s hs
386 simpa [S, R, σ, τ, e, θ] using
388 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail s hs
389 let data :
390 FuchsianEllipticCyclicRelatorData σ ξ i₀ hi₀ S := by
392 σ, τ, ξ, i₀, hi₀, e, R, S, θ,
397 (R := R) (S := S) (invHom := θ) hTarget D)
399 σ, τ, ξ, hpow, hprod, S] using
401 σ ξ hpow hprod i₀ hi₀ S data
403 {tailLen p q : ℕ}
404 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
405 (hp : 2 ≤ p) (hq : 2 ≤ q)
406 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
407 (htail : ∀ j, 2 ≤ tail j) :
408 Nonempty
410 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).ker ≃*
413 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)) := by
414 let D :=
416 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
418 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
419 (by
420 classical
421 have hNegative :=
423 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
424 have hTotal :=
426 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
430 refine ⟨?_, ?_, ?_, ?_, hTotal⟩
431 · intro k
432 simpa using
434 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k
435 · intro k
436 simpa using
438 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k
439 · intro r k
440 by_cases h0 : r.val = 0
441 · have hr : r = ⟨0, by omega⟩ := Fin.ext h0
442 rw [hr]
443 simpa using
445 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k
446 · by_cases h1 : r.val = 1
447 · have hr : r = ⟨1, by omega⟩ := Fin.ext h1
448 rw [hr]
449 simpa using hNegative k
450 · let rRest : Fin (p - 2) := ⟨r.val - 2, by omega⟩
451 have hr : r = (⟨2 + rRest.val, by omega⟩ : Fin p) := by
452 ext
453 simp only [rRest]
454 omega
455 rw [hr]
456 simpa [rRest] using
458 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail rRest k
459 · intro b j k
460 simpa using
462 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k))
463 let eBlock :=
465 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail D
466 let eBlockOrdered :=
468 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
469 rcases
471 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail with
472 ⟨eOrderedTransport⟩
473 exact ⟨eBlock.trans (eBlockOrdered.trans eOrderedTransport)⟩
474end FenchelNielsen