FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/Relators/Target.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.TransportMaps
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/Relators/Target.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14The second explicit reduction step, with ordered target signatures, transport maps, source and target relator calculations, and quotient-basis comparison.
15-/
17namespace FenchelNielsen
20 {tailLen p q : ℕ}
21 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
22 (hp : 2 ≤ p) (hq : 2 ≤ q)
23 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
24 (htail : ∀ j, 2 ≤ tail j) :
25 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
26 let σ :=
28 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
29 let τ :=
30 secondReductionTransportSignature (p := p) hq
31 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
32 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
33 let e :=
35 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
36 let θ :=
38 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
39 let idx :=
40 secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨0, by decide⟩
41 let A :=
42 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
43 θ A =
44 e.symm
46 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) := by
47 classical
48 dsimp
49 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
50 let σ :=
52 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
53 let τ :=
54 secondReductionTransportSignature (p := p) hq
55 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
56 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
57 let e :=
59 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
60 let θ :=
62 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
63 let idx :=
64 secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨0, by decide⟩
65 let A :=
66 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
67 simp only [secondReductionCanonicalTransportToSchreierHom, xWord,
68 secondReductionCanonicalTransportDistinguishedIndex, Fin.isValue, Fin.zero_eta, FreeGroup.lift_apply_of,
69 secondReductionCanonicalTransportToSchreierGeneratorImage, secondReductionCanonicalTransportToSchreierGenerator,
70 Lean.Elab.WF.paramLet, Fin.val_eq_zero_iff, dite_eq_ite, Equiv.symm_apply_apply, id_eq, ↓reduceIte,
73 {tailLen p q : ℕ}
74 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
75 (hp : 2 ≤ p) (hq : 2 ≤ q)
76 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
77 (htail : ∀ j, 2 ≤ tail j) :
78 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
79 let σ :=
81 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
82 let τ :=
83 secondReductionTransportSignature (p := p) hq
84 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
85 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
86 let e :=
88 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
89 let θ :=
91 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
92 let idx :=
93 secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨1, by decide⟩
94 let B :=
95 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
96 θ B =
97 e.symm
99 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) := by
100 classical
101 dsimp
102 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
103 let σ :=
105 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
106 let τ :=
107 secondReductionTransportSignature (p := p) hq
108 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
109 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
110 let e :=
112 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
113 let θ :=
115 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
116 let idx :=
117 secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨1, by decide⟩
118 let B :=
119 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
120 simp only [secondReductionCanonicalTransportToSchreierHom, xWord,
121 secondReductionCanonicalTransportDistinguishedIndex, Fin.isValue, Fin.zero_eta, FreeGroup.lift_apply_of,
122 secondReductionCanonicalTransportToSchreierGeneratorImage, secondReductionCanonicalTransportToSchreierGenerator,
123 Lean.Elab.WF.paramLet, Fin.val_eq_zero_iff, dite_eq_ite, Equiv.symm_apply_apply, id_eq, one_ne_zero, ↓reduceIte,
126 {tailLen p q : ℕ}
127 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
128 (hp : 2 ≤ p) (hq : 2 ≤ q)
129 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
130 (htail : ∀ j, 2 ≤ tail j)
131 (k : Fin q) :
132 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
133 let σ :=
135 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
136 let τ :=
137 secondReductionTransportSignature (p := p) hq
138 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
139 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
140 let e :=
142 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
143 let θ :=
145 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
146 let idx :=
147 secondReductionCanonicalTransportHeadIndex tailLen p q ⟨0, by decide⟩ k
148 let C :=
149 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
150 θ C =
151 e.symm
153 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k) := by
154 classical
155 dsimp
156 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
157 let σ :=
159 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
160 let τ :=
161 secondReductionTransportSignature (p := p) hq
162 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
163 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
164 let e :=
166 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
167 let θ :=
169 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
170 let idx :=
171 secondReductionCanonicalTransportHeadIndex tailLen p q ⟨0, by decide⟩ k
172 let C :=
173 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
174 simp only [secondReductionCanonicalTransportToSchreierHom, xWord, secondReductionCanonicalTransportHeadIndex,
175 Fin.isValue, id_eq, FreeGroup.lift_apply_of, secondReductionCanonicalTransportToSchreierGeneratorImage,
176 secondReductionCanonicalTransportToSchreierGenerator, Lean.Elab.WF.paramLet, Fin.val_eq_zero_iff, dite_eq_ite,
177 Equiv.symm_apply_apply, ↓reduceIte, secondReductionCanonicalHeadZeroKernelElement,
180 {tailLen p q : ℕ}
181 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
182 (hp : 2 ≤ p) (hq : 2 ≤ q)
183 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
184 (htail : ∀ j, 2 ≤ tail j)
185 (k : Fin q) :
186 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
187 let σ :=
189 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
190 let τ :=
191 secondReductionTransportSignature (p := p) hq
192 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
193 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
194 let e :=
196 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
197 let θ :=
199 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
200 let idx :=
201 secondReductionCanonicalTransportHeadIndex tailLen p q ⟨1, by decide⟩ k
202 let C :=
203 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
204 θ C =
205 e.symm
207 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k) := by
208 classical
209 dsimp
210 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
211 let σ :=
213 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
214 let τ :=
215 secondReductionTransportSignature (p := p) hq
216 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
217 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
218 let e :=
220 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
221 let θ :=
223 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
224 let idx :=
225 secondReductionCanonicalTransportHeadIndex tailLen p q ⟨1, by decide⟩ k
226 let C :=
227 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
228 simp only [secondReductionCanonicalTransportToSchreierHom, xWord, secondReductionCanonicalTransportHeadIndex,
229 Fin.isValue, id_eq, FreeGroup.lift_apply_of, secondReductionCanonicalTransportToSchreierGeneratorImage,
230 secondReductionCanonicalTransportToSchreierGenerator, Lean.Elab.WF.paramLet, Fin.val_eq_zero_iff, dite_eq_ite,
231 Equiv.symm_apply_apply, one_ne_zero, ↓reduceIte, secondReductionCanonicalHeadOneKernelElement,
234 {tailLen p q : ℕ}
235 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
236 (hp : 2 ≤ p) (hq : 2 ≤ q)
237 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
238 (htail : ∀ j, 2 ≤ tail j)
239 (r : Fin (p - 2)) (k : Fin q) :
240 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
241 let σ :=
243 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
244 let τ :=
245 secondReductionTransportSignature (p := p) hq
246 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
247 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
248 let e :=
250 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
251 let θ :=
253 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
254 let idx :=
255 secondReductionCanonicalTransportMiddleRestIndex tailLen p q r k
256 let C :=
257 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
258 θ C =
259 e.symm
261 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r k) := by
262 classical
263 dsimp
264 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
265 let σ :=
267 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
268 let τ :=
269 secondReductionTransportSignature (p := p) hq
270 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
271 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
272 let e :=
274 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
275 let θ :=
277 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
278 let idx :=
279 secondReductionCanonicalTransportMiddleRestIndex tailLen p q r k
280 let C :=
281 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
282 simp only [secondReductionCanonicalTransportToSchreierHom, xWord,
283 secondReductionCanonicalTransportMiddleRestIndex, id_eq, FreeGroup.lift_apply_of,
284 secondReductionCanonicalTransportToSchreierGeneratorImage, secondReductionCanonicalTransportToSchreierGenerator,
285 Lean.Elab.WF.paramLet, Fin.val_eq_zero_iff, Fin.isValue, dite_eq_ite, Equiv.symm_apply_apply,
286 secondReductionCanonicalMiddleRestZeroKernelElement, secondReductionCanonicalZeroImageKernelElement]
288 {tailLen p q : ℕ}
289 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
290 (hp : 2 ≤ p) (hq : 2 ≤ q)
291 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
292 (htail : ∀ j, 2 ≤ tail j)
293 (b : Fin p) (j : Fin tailLen) (k : Fin q) :
294 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
295 let σ :=
297 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
298 let τ :=
299 secondReductionTransportSignature (p := p) hq
300 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
301 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
302 let e :=
304 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
305 let θ :=
307 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
308 let idx :=
309 secondReductionCanonicalTransportTailIndex tailLen p q b j k
310 let C :=
311 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
312 θ C =
313 e.symm
315 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k) := by
316 classical
317 dsimp
318 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
319 let σ :=
321 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
322 let τ :=
323 secondReductionTransportSignature (p := p) hq
324 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
325 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
326 let e :=
328 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
329 let θ :=
331 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
332 let idx :=
333 secondReductionCanonicalTransportTailIndex tailLen p q b j k
334 let C :=
335 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
336 simp only [secondReductionCanonicalTransportToSchreierHom, xWord, secondReductionCanonicalTransportTailIndex,
337 id_eq, FreeGroup.lift_apply_of, secondReductionCanonicalTransportToSchreierGeneratorImage,
338 secondReductionCanonicalTransportToSchreierGenerator, Lean.Elab.WF.paramLet, Fin.val_eq_zero_iff, Fin.isValue,
339 dite_eq_ite, Equiv.symm_apply_apply, secondReductionCanonicalTailZeroKernelElement,
341noncomputable def secondReductionCanonicalTransportZeroBlockWord
342 {tailLen p q : ℕ}
343 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
344 (hq : 2 ≤ q)
345 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
346 (htail : ∀ j, 2 ≤ tail j) :
347 let τ :=
348 secondReductionTransportSignature (p := p) hq
349 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
350 Fin q → FreeGroup (FuchsianGenerator τ) := by
351 classical
352 dsimp
353 let τ :=
354 secondReductionTransportSignature (p := p) hq
355 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
356 let targetWord :=
357 secondReductionCanonicalTransportTargetWord (p := p) (q := q)
358 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail
359 intro k
360 exact
361 (List.ofFn (fun r : Fin (p - 2) =>
362 targetWord (secondReductionCanonicalTransportMiddleRestIndex tailLen p q r k))).prod *
363 (List.ofFn (fun b : Fin p =>
364 (List.ofFn (fun j : Fin tailLen =>
365 targetWord (secondReductionCanonicalTransportTailIndex tailLen p q b j k))).prod)).prod *
366 targetWord (secondReductionCanonicalTransportHeadIndex tailLen p q ⟨0, by decide⟩ k) *
367 targetWord (secondReductionCanonicalTransportHeadIndex tailLen p q ⟨1, by decide⟩ k)
368noncomputable def secondReductionCanonicalTransportBlockTotalWord
369 {tailLen p q : ℕ}
370 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
371 (hq : 2 ≤ q)
372 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
373 (htail : ∀ j, 2 ≤ tail j) :
374 let τ :=
375 secondReductionTransportSignature (p := p) hq
376 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
377 FreeGroup (FuchsianGenerator τ) := by
378 classical
379 dsimp
380 let τ :=
381 secondReductionTransportSignature (p := p) hq
382 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
383 let A :=
385 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))
386 (secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨0, by decide⟩))
387 let B :=
389 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))
390 (secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨1, by decide⟩))
391 let C :=
392 (List.ofFn (fun k : Fin q =>
393 secondReductionCanonicalTransportZeroBlockWord (p := p) (q := q)
394 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail k)).prod
395 exact A * B * C
396noncomputable def secondReductionCanonicalTransportBlockRelators
397 {tailLen p q : ℕ}
398 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
399 (hq : 2 ≤ q)
400 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
401 (htail : ∀ j, 2 ≤ tail j) :
402 let τ :=
403 secondReductionTransportSignature (p := p) hq
404 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
405 Set (FreeGroup (FuchsianGenerator τ)) := by
406 classical
407 dsimp
408 let τ :=
409 secondReductionTransportSignature (p := p) hq
410 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
411 exact
413 r =
414 secondReductionCanonicalTransportBlockTotalWord (p := p) (q := q)
415 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail}
417 {tailLen p q : ℕ}
418 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
419 (hq : 2 ≤ q)
420 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
421 (htail : ∀ j, 2 ≤ tail j)
422 (i : Fin
423 (secondReductionTransportSignature (p := p) hq
424 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail).numPeriods) :
426 (secondReductionTransportSignature (p := p) hq
427 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail) i) ^
428 (secondReductionTransportSignature (p := p) hq
429 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail).periods i ∈
430 secondReductionCanonicalTransportBlockRelators (p := p) (q := q)
431 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail := by
432 classical
433 left
434 exact ⟨i, rfl⟩
436 {tailLen p q : ℕ}
437 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
438 (hq : 2 ≤ q)
439 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
440 (htail : ∀ j, 2 ≤ tail j) :
441 secondReductionCanonicalTransportBlockTotalWord (p := p) (q := q)
442 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail ∈
443 secondReductionCanonicalTransportBlockRelators (p := p) (q := q)
444 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail := by
445 classical
446 right
447 rfl
449 {tailLen p q : ℕ}
450 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
451 (hp : 2 ≤ p) (hq : 2 ≤ q)
452 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
453 (htail : ∀ j, 2 ≤ tail j) :
454 let υ :=
456 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
457 FreeGroup.freeGroupCongr
459 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
460 (secondReductionCanonicalTransportBlockTotalWord (p := p) (q := q)
461 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) =
462 totalRelation υ := by
463 classical
464 dsimp
465 let τ :=
466 secondReductionTransportSignature (p := p) hq
467 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
468 let υ :=
470 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
471 let eGen :=
473 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
474 have hTotal :
475 totalRelation υ =
478 ⟨0, by decide⟩) *
481 ⟨1, by decide⟩) *
482 (List.ofFn (fun k : Fin q =>
484 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k)).prod := by
485 simpa [υ] using
487 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
488 have hZero :
489 ∀ k : Fin q,
491 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k =
492 (List.ofFn (fun r : Fin (p - 2) =>
493 xWord υ (secondReductionCanonicalOrderedTargetMiddleRestIndex tailLen p q r k))).prod *
494 (List.ofFn (fun b : Fin p =>
495 (List.ofFn (fun j : Fin tailLen =>
497 (secondReductionCanonicalOrderedTargetTailIndex tailLen p q b j k))).prod)).prod *
499 (secondReductionCanonicalOrderedTargetHeadIndex tailLen p q ⟨0, by decide⟩ k) *
501 (secondReductionCanonicalOrderedTargetHeadIndex tailLen p q ⟨1, by decide⟩ k) := by
502 intro k
503 simpa [υ] using
505 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k
506 rw [hTotal]
507 simp only [secondReductionCanonicalTransportGeneratorEquivOrderedTarget, Equiv.coe_fn_mk,
508 secondReductionCanonicalTransportBlockTotalWord, Lean.Elab.WF.paramLet, xWord, Fin.zero_eta, Fin.isValue,
509 Fin.mk_one, secondReductionCanonicalTransportZeroBlockWord, secondReductionCanonicalTransportTargetWord, id_eq,
510 mul_assoc, map_mul, FreeGroup.map.of, secondReductionCanonicalTransportFinEquivOrderedTargetFin_apply,
511 secondReductionTransportIndexEquivCanonicalOrderedTargetFin_distinguished, map_list_prod, List.map_ofFn,
512 Function.comp_def, secondReductionTransportIndexEquivCanonicalOrderedTargetFin_middleRest,
515noncomputable def secondReductionCanonicalTransportBlockRelatorsEquivOrderedTarget
516 {tailLen p q : ℕ}
517 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
518 (hp : 2 ≤ p) (hq : 2 ≤ q)
519 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
520 (htail : ∀ j, 2 ≤ tail j) :
521 PresentedGroup
522 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)
523 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) ≃*
526 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) := by
527 classical
528 let τ :=
529 secondReductionTransportSignature (p := p) hq
530 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
531 let υ :=
533 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
534 let eFin :=
536 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
537 let eGen :=
539 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
540 let eFG : FreeGroup (FuchsianGenerator τ) ≃*
541 FreeGroup (FuchsianGenerator υ) :=
542 FreeGroup.freeGroupCongr eGen
543 let R : Set (FreeGroup (FuchsianGenerator τ)) :=
544 secondReductionCanonicalTransportBlockRelators (p := p) (q := q)
545 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail
546 let S : Set (FreeGroup (FuchsianGenerator υ)) := relators υ
547 refine
549 (ReidemeisterSchreier.Discrete.Presentations.relatorQuotientMutualMapDataOfRelatorImagesMemNormalClosure eFG R S ?_ ?_)
550 · intro r hr
551 change
553 r =
554 secondReductionCanonicalTransportBlockTotalWord (p := p) (q := q)
555 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) at hr
556 rcases hr with ⟨i, rfl⟩ | htotal
557 · have hperiod :
558 τ.periods i = υ.periods (eFin i) := by
559 simpa [τ, υ, eFin] using
561 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i
562 have hx :
564 simpa [τ, υ, eFin, eGen, eFG] using
566 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i
567 have hrel :
570 rw [map_pow, hx, hperiod]
571 rw [hrel]
572 exact Subgroup.subset_normalClosure (Or.inl ⟨eFin i, rfl⟩)
573 · rw [htotal]
574 have htotalMap :
575 eFG
576 (secondReductionCanonicalTransportBlockTotalWord (p := p) (q := q)
577 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) =
578 totalRelation υ := by
579 simpa [τ, υ, eGen, eFG] using
581 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
582 rw [htotalMap]
583 exact Subgroup.subset_normalClosure (Or.inr rfl)
584 · intro s hs
585 rcases hs with ⟨i, rfl⟩ | htotal
586 · let j := eFin.symm i
587 have hji : eFin j = i := by
588 simp only [Equiv.apply_symm_apply, j]
589 have hperiod : υ.periods i = τ.periods j := by
590 rw [← hji]
591 simpa [τ, υ, eFin, j] using
593 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail j).symm
594 have hx :
596 simpa [τ, υ, eFin, eGen, eFG, j] using
598 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i
599 have hrel :
602 rw [map_pow, hx, hperiod]
603 rw [hrel]
604 exact Subgroup.subset_normalClosure (Or.inl ⟨j, rfl⟩)
605 · rw [htotal]
606 have htotalMap :
607 eFG
608 (secondReductionCanonicalTransportBlockTotalWord (p := p) (q := q)
609 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) =
610 totalRelation υ := by
611 simpa [τ, υ, eGen, eFG] using
613 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
614 have hsymm :
615 eFG.symm (totalRelation υ) =
616 secondReductionCanonicalTransportBlockTotalWord (p := p) (q := q)
617 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail := by
618 rw [← htotalMap]
619 exact eFG.left_inv
620 (secondReductionCanonicalTransportBlockTotalWord (p := p) (q := q)
621 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)
622 rw [hsymm]
623 exact Subgroup.subset_normalClosure (Or.inr rfl)
625end FenchelNielsen