Source: FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/Relators/SourceMiddleTail.lean

1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Relators.SourceCore

2

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/Relators/SourceMiddleTail.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

10-/

11/-!

12# Second compact zero-genus reduction

13

14The second explicit reduction step, with ordered target signatures, transport maps, source and target relator calculations, and quotient-basis comparison.

15-/

16

17namespace FenchelNielsen

18

19theorem secondReductionToTransportSecondBranch_tail_sourceCase_mem_normalClosure

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) (b : Fin p) (j : Fin tailLen) (k : Fin q) :

25 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

26 let σ :=

27 secondReductionCanonicalSourceSignature

28 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

29 let φ :=

30 secondReductionCanonicalSourceFreeQuotientHom

31 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

32 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

33 let e :=

34 secondReductionCanonicalSchreierBasisEquiv

35 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

36 let η :=

37 secondReductionCanonicalSchreierToTransportSecondBranchHom

38 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

39 let x : FuchsianGenerator σ :=

40 secondReductionCanonicalDistinguishedGenerator

41 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

42 let iTail :=

43 secondReductionCanonicalSourceTailIndex

44 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j

45 η

46 (e.symm

47 (⟨(FreeGroup.of x) ^ k.val * ((xWord σ iTail) ^ σ.periods iTail) *

48 ((FreeGroup.of x) ^ k.val)⁻¹, by

49 change φ

50 ((FreeGroup.of x) ^ k.val * ((xWord σ iTail) ^ σ.periods iTail) *

51 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

52 have hrφ :

53 φ ((xWord σ iTail) ^ σ.periods iTail) = 1 :=

54 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

55 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

56 ((xWord σ iTail) ^ σ.periods iTail) (Or.inl ⟨iTail, rfl⟩)

57 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈

58 Subgroup.normalClosure

59 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

60 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

61 classical

62 dsimp

63 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

64 let σ :=

65 secondReductionCanonicalSourceSignature

66 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

67 let τ :=

68 secondReductionTransportSignature (p := p) hq

69 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail

70 let φ :=

71 secondReductionCanonicalSourceFreeQuotientHom

72 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

73 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

74 let e :=

75 secondReductionCanonicalSchreierBasisEquiv

76 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

77 let η :=

78 secondReductionCanonicalSchreierToTransportSecondBranchHom

79 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

80 let x : FuchsianGenerator σ :=

81 secondReductionCanonicalDistinguishedGenerator

82 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

83 let iTail :=

84 secondReductionCanonicalSourceTailIndex

85 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j

86 let zTail :=

87 secondReductionCanonicalTailZeroKernelElement

88 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k

89 let z : φ.ker :=

90 ⟨(FreeGroup.of x) ^ k.val * ((xWord σ iTail) ^ σ.periods iTail) *

91 ((FreeGroup.of x) ^ k.val)⁻¹, by

92 change φ

93 ((FreeGroup.of x) ^ k.val * ((xWord σ iTail) ^ σ.periods iTail) *

94 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

95 have hrφ : φ ((xWord σ iTail) ^ σ.periods iTail) = 1 :=

96 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

97 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

98 ((xWord σ iTail) ^ σ.periods iTail) (Or.inl ⟨iTail, rfl⟩)

99 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩

100 have hz : z = zTail ^ tail j := by

101 apply Subtype.ext

102 change

103 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *

104 ((xWord σ iTail) ^ σ.periods iTail) *

105 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =

106 ((zTail ^ tail j : φ.ker) : FreeGroup (FuchsianGenerator σ))

107 rw [show ((zTail ^ tail j : φ.ker) : FreeGroup (FuchsianGenerator σ)) =

108 ((zTail : φ.ker) : FreeGroup (FuchsianGenerator σ)) ^ tail j by

109 exact (map_pow (φ.ker.subtype) zTail (tail j))]

110 have hperiod : σ.periods iTail = tail j := by

111 simp only [secondReductionCanonicalSourceSignature_period_tail, σ, iTail]

112 simp only [secondReductionCanonicalDistinguishedGenerator, xWord, hperiod,

113 secondReductionCanonicalTailZeroKernelElement, Lean.Elab.WF.paramLet,

114 secondReductionCanonicalZeroImageKernelElement, id_eq, conj_pow, σ, x, iTail, zTail]

115 have hmain : (η (e.symm zTail)) ^ tail j ∈ Subgroup.normalClosure

116 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

117 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

118 have hword :=

119 secondReductionCanonicalSchreierToTransportSecondBranchHom_tailWord

120 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k

121 have hrel :

122 (secondReductionCanonicalTransportTargetWord (p := p) (q := q)

123 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail

124 (secondReductionCanonicalTransportTailIndex tailLen p q b j k)) ^

125 tail j ∈ Subgroup.normalClosure

126 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

127 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

128 have hmem :

129 (xWord τ

130 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))

131 (secondReductionCanonicalTransportTailIndex tailLen p q b j k))) ^

132 τ.periods

133 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))

134 (secondReductionCanonicalTransportTailIndex tailLen p q b j k)) ∈

135 secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

136 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail :=

137 secondReductionCanonicalTransport_powerRelator_mem_blockRelators

138 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail _

139 simpa [τ, secondReductionCanonicalTransportTargetWord,

140 secondReductionTransportSignature, familyFuchsianSignature_periods,

141 secondReductionTransportPeriods, singermanTransportPeriodsFamily,

142 secondReductionSourceTransportPeriods, secondReductionSourceCycleCount] using

143 Subgroup.subset_normalClosure hmem

144 simpa [σ, e, η, zTail, hword] using hrel

145 change η (e.symm z) ∈ Subgroup.normalClosure

146 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

147 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)

148 rw [hz, map_pow]

149 simpa [zTail] using hmain

150theorem secondReductionToTransportSecondBranch_middleRest_sourceCase_mem_normalClosure

151 {tailLen p q : ℕ}

152 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)

153 (hp : 2 ≤ p) (hq : 2 ≤ q)

154 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')

155 (htail : ∀ j, 2 ≤ tail j) (r : Fin (p - 2)) (k : Fin q) :

156 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

157 let σ :=

158 secondReductionCanonicalSourceSignature

159 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

160 let φ :=

161 secondReductionCanonicalSourceFreeQuotientHom

162 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

163 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

164 let e :=

165 secondReductionCanonicalSchreierBasisEquiv

166 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

167 let η :=

168 secondReductionCanonicalSchreierToTransportSecondBranchHom

169 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

170 let x : FuchsianGenerator σ :=

171 secondReductionCanonicalDistinguishedGenerator

172 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

173 let rSource : Fin p := ⟨2 + r.val, by omega⟩

174 let iMiddle :=

175 secondReductionCanonicalSourceMiddleIndex

176 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail rSource

177 η

178 (e.symm

179 (⟨(FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

180 ((FreeGroup.of x) ^ k.val)⁻¹, by

181 change φ

182 ((FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

183 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

184 have hrφ :

185 φ ((xWord σ iMiddle) ^ σ.periods iMiddle) = 1 :=

186 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

187 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

188 ((xWord σ iMiddle) ^ σ.periods iMiddle) (Or.inl ⟨iMiddle, rfl⟩)

189 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈

190 Subgroup.normalClosure

191 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

192 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

193 classical

194 dsimp

195 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

196 let σ :=

197 secondReductionCanonicalSourceSignature

198 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

199 let τ :=

200 secondReductionTransportSignature (p := p) hq

201 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail

202 let φ :=

203 secondReductionCanonicalSourceFreeQuotientHom

204 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

205 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

206 let e :=

207 secondReductionCanonicalSchreierBasisEquiv

208 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

209 let η :=

210 secondReductionCanonicalSchreierToTransportSecondBranchHom

211 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

212 let x : FuchsianGenerator σ :=

213 secondReductionCanonicalDistinguishedGenerator

214 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

215 let rSource : Fin p := ⟨2 + r.val, by omega⟩

216 let iMiddle :=

217 secondReductionCanonicalSourceMiddleIndex

218 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail rSource

219 let zMiddle :=

220 secondReductionCanonicalMiddleRestZeroKernelElement

221 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r k

222 let z : φ.ker :=

223 ⟨(FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

224 ((FreeGroup.of x) ^ k.val)⁻¹, by

225 change φ

226 ((FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

227 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

228 have hrφ : φ ((xWord σ iMiddle) ^ σ.periods iMiddle) = 1 :=

229 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

230 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

231 ((xWord σ iMiddle) ^ σ.periods iMiddle) (Or.inl ⟨iMiddle, rfl⟩)

232 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩

233 have hz : z = zMiddle ^ (q * m₃') := by

234 apply Subtype.ext

235 change

236 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *

237 ((xWord σ iMiddle) ^ σ.periods iMiddle) *

238 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =

239 ((zMiddle ^ (q * m₃') : φ.ker) : FreeGroup (FuchsianGenerator σ))

240 rw [show ((zMiddle ^ (q * m₃') : φ.ker) : FreeGroup (FuchsianGenerator σ)) =

241 ((zMiddle : φ.ker) : FreeGroup (FuchsianGenerator σ)) ^ (q * m₃') by

242 exact (map_pow (φ.ker.subtype) zMiddle (q * m₃'))]

243 have hperiod : σ.periods iMiddle = q * m₃' := by

244 simp only [secondReductionCanonicalSourceSignature_period_middle, σ, iMiddle, rSource]

245 simp only [secondReductionCanonicalDistinguishedGenerator, xWord, hperiod,

246 secondReductionCanonicalMiddleRestZeroKernelElement, Lean.Elab.WF.paramLet,

247 secondReductionCanonicalZeroImageKernelElement, id_eq, conj_pow, σ, x, iMiddle, rSource, zMiddle]

248 have hmain : (η (e.symm zMiddle)) ^ (q * m₃') ∈

249 Subgroup.normalClosure

250 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

251 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

252 have hword :=

253 secondReductionCanonicalSchreierToTransportSecondBranchHom_middleRestWord

254 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r k

255 have hrel :

256 (secondReductionCanonicalTransportTargetWord (p := p) (q := q)

257 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail

258 (secondReductionCanonicalTransportMiddleRestIndex tailLen p q r k)) ^

259 (q * m₃') ∈ Subgroup.normalClosure

260 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

261 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

262 have hmem :

263 (xWord τ

264 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))

265 (secondReductionCanonicalTransportMiddleRestIndex tailLen p q r k))) ^

266 τ.periods

267 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))

268 (secondReductionCanonicalTransportMiddleRestIndex tailLen p q r k)) ∈

269 secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

270 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail :=

271 secondReductionCanonicalTransport_powerRelator_mem_blockRelators

272 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail _

273 simpa [τ, secondReductionCanonicalTransportTargetWord,

274 secondReductionTransportSignature, familyFuchsianSignature_periods,

275 secondReductionTransportPeriods, singermanTransportPeriodsFamily,

276 secondReductionSourceTransportPeriods, secondReductionSourceCycleCount] using

277 Subgroup.subset_normalClosure hmem

278 simpa [σ, e, η, zMiddle, hword] using hrel

279 change η (e.symm z) ∈ Subgroup.normalClosure

280 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

281 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)

282 rw [hz, map_pow]

283 simpa [zMiddle] using hmain

284theorem secondReductionToTransportSecondBranch_posMiddle_sourceCase_mem_normalClosure

285 {tailLen p q : ℕ}

286 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)

287 (hp : 2 ≤ p) (hq : 2 ≤ q)

288 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')

289 (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :

290 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

291 let σ :=

292 secondReductionCanonicalSourceSignature

293 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

294 let φ :=

295 secondReductionCanonicalSourceFreeQuotientHom

296 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

297 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

298 let e :=

299 secondReductionCanonicalSchreierBasisEquiv

300 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

301 let η :=

302 secondReductionCanonicalSchreierToTransportSecondBranchHom

303 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

304 let x : FuchsianGenerator σ :=

305 secondReductionCanonicalDistinguishedGenerator

306 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

307 let iMiddle :=

308 secondReductionCanonicalSourceMiddleIndex

309 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨0, by omega⟩

310 η

311 (e.symm

312 (⟨(FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

313 ((FreeGroup.of x) ^ k.val)⁻¹, by

314 change φ

315 ((FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

316 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

317 have hrφ :

318 φ ((xWord σ iMiddle) ^ σ.periods iMiddle) = 1 :=

319 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

320 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

321 ((xWord σ iMiddle) ^ σ.periods iMiddle) (Or.inl ⟨iMiddle, rfl⟩)

322 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈

323 Subgroup.normalClosure

324 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

325 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

326 classical

327 dsimp

328 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

329 let σ :=

330 secondReductionCanonicalSourceSignature

331 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

332 let τ :=

333 secondReductionTransportSignature (p := p) hq

334 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail

335 let φ :=

336 secondReductionCanonicalSourceFreeQuotientHom

337 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

338 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

339 let e :=

340 secondReductionCanonicalSchreierBasisEquiv

341 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

342 let η :=

343 secondReductionCanonicalSchreierToTransportSecondBranchHom

344 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

345 let x : FuchsianGenerator σ :=

346 secondReductionCanonicalDistinguishedGenerator

347 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

348 let iMiddle :=

349 secondReductionCanonicalSourceMiddleIndex

350 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨0, by omega⟩

351 let zFirst :=

352 secondReductionCanonicalFirstPowerKernel

353 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

354 let z : φ.ker :=

355 ⟨(FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

356 ((FreeGroup.of x) ^ k.val)⁻¹, by

357 change φ

358 ((FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

359 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

360 have hrφ : φ ((xWord σ iMiddle) ^ σ.periods iMiddle) = 1 :=

361 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

362 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

363 ((xWord σ iMiddle) ^ σ.periods iMiddle) (Or.inl ⟨iMiddle, rfl⟩)

364 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩

365 have hz : z = zFirst ^ m₃' := by

366 apply Subtype.ext

367 change

368 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *

369 ((xWord σ iMiddle) ^ σ.periods iMiddle) *

370 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =

371 ((zFirst ^ m₃' : φ.ker) : FreeGroup (FuchsianGenerator σ))

372 rw [show ((zFirst ^ m₃' : φ.ker) : FreeGroup (FuchsianGenerator σ)) =

373 ((zFirst : φ.ker) : FreeGroup (FuchsianGenerator σ)) ^ m₃' by

374 exact (map_pow (φ.ker.subtype) zFirst m₃')]

375 have hperiod : σ.periods iMiddle = q * m₃' := by

376 simp only [secondReductionCanonicalSourceSignature_period_middle, σ, iMiddle]

377 rw [secondReductionCanonicalFirstPowerKernel_coe]

378 rw [hperiod]

379 simp only [secondReductionCanonicalDistinguishedGenerator, secondReductionCanonicalSourceMiddleIndex,

380 add_zero, xWord, pow_mul, σ, x, iMiddle]

381 group

382 have hmain : (η (e.symm zFirst)) ^ m₃' ∈ Subgroup.normalClosure

383 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

384 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

385 have hword :=

386 secondReductionCanonicalSchreierToTransportSecondBranchHom_firstPowerWord

387 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

388 have hrel :

389 (secondReductionCanonicalTransportTargetWord (p := p) (q := q)

390 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail

391 (secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨0, by decide⟩)) ^

392 m₃' ∈ Subgroup.normalClosure

393 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

394 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

395 have hmem :

396 (xWord τ

397 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))

398 (secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨0, by decide⟩))) ^

399 τ.periods

400 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))

401 (secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨0, by decide⟩)) ∈

402 secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

403 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail :=

404 secondReductionCanonicalTransport_powerRelator_mem_blockRelators

405 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail _

406 simpa [τ, secondReductionCanonicalTransportTargetWord,

407 secondReductionTransportSignature, familyFuchsianSignature_periods,

408 secondReductionTransportPeriods, singermanTransportPeriodsFamily,

409 secondReductionSourceTransportPeriods, secondReductionSourceCycleCount] using

410 Subgroup.subset_normalClosure hmem

411 simpa [σ, e, η, zFirst, hword] using hrel

412 change η (e.symm z) ∈ Subgroup.normalClosure

413 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

414 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)

415 rw [hz, map_pow]

416 simpa [zFirst] using hmain

417def SecondReductionCanonicalSecondBranchNegativeMiddleSourceCase

418 {tailLen p q : ℕ}

419 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)

420 (hp : 2 ≤ p) (hq : 2 ≤ q)

421 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')

422 (htail : ∀ j, 2 ≤ tail j) : Prop :=

423 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

424 let σ :=

425 secondReductionCanonicalSourceSignature

426 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

427 let τ :=

428 secondReductionTransportSignature (p := p) hq

429 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail

430 let φ :=

431 secondReductionCanonicalSourceFreeQuotientHom

432 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

433 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

434 let e :=

435 secondReductionCanonicalSchreierBasisEquiv

436 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

437 let η :=

438 secondReductionCanonicalSchreierToTransportSecondBranchHom

439 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

440 let x : FuchsianGenerator σ :=

441 secondReductionCanonicalDistinguishedGenerator

442 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

443 let iMiddle :=

444 secondReductionCanonicalSourceMiddleIndex

445 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩

446 ∀ k : Fin q,

447 η

448 (e.symm

449 (⟨(FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

450 ((FreeGroup.of x) ^ k.val)⁻¹, by

451 change φ

452 ((FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

453 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

454 have hrφ :

455 φ ((xWord σ iMiddle) ^ σ.periods iMiddle) = 1 :=

456 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

457 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

458 ((xWord σ iMiddle) ^ σ.periods iMiddle) (Or.inl ⟨iMiddle, rfl⟩)

459 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈

460 Subgroup.normalClosure

461 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

462 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)

463theorem secondReductionCanonicalSecondBranchNegativeMiddleSourceCase_mem_blockRelators

464 {tailLen p q : ℕ}

465 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)

466 (hp : 2 ≤ p) (hq : 2 ≤ q)

467 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')

468 (htail : ∀ j, 2 ≤ tail j) :

469 SecondReductionCanonicalSecondBranchNegativeMiddleSourceCase

470 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail := by

471 classical

472 dsimp [SecondReductionCanonicalSecondBranchNegativeMiddleSourceCase]

473 intro k

474 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

475 let σ :=

476 secondReductionCanonicalSourceSignature

477 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

478 let τ :=

479 secondReductionTransportSignature (p := p) hq

480 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail

481 let φ :=

482 secondReductionCanonicalSourceFreeQuotientHom

483 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

484 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

485 let e :=

486 secondReductionCanonicalSchreierBasisEquiv

487 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

488 let θ :=

489 secondReductionCanonicalTransportToSchreierHom

490 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

491 let η :=

492 secondReductionCanonicalSchreierToTransportSecondBranchHom

493 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

494 let x : FuchsianGenerator σ :=

495 secondReductionCanonicalDistinguishedGenerator

496 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

497 let iMiddle :=

498 secondReductionCanonicalSourceMiddleIndex

499 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩

500 let y : FuchsianGenerator σ := FuchsianGenerator.elliptic iMiddle

501 let edge : Fin q → φ.ker :=

502 secondReductionCanonicalSecondEdgeKernelElement

503 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

504 let lower :=

505 (List.ofFn (fun i : Fin k.val => edge ⟨k.val - i.val, by omega⟩)).prod

506 let wrap := edge ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hq⟩

507 let upper :=

508 (List.ofFn (fun i : Fin (q - 1 - k.val) => edge ⟨q - 1 - i.val, by omega⟩)).prod

509 let cycle := lower * wrap * upper

510 let base :=

511 secondReductionCanonicalSecondPowerKernel

512 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

513 let z : φ.ker :=

514 ⟨(FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

515 ((FreeGroup.of x) ^ k.val)⁻¹, by

516 change φ

517 ((FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *

518 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

519 have hrφ : φ ((xWord σ iMiddle) ^ σ.periods iMiddle) = 1 :=

520 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

521 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

522 ((xWord σ iMiddle) ^ σ.periods iMiddle) (Or.inl ⟨iMiddle, rfl⟩)

523 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩

524 have hcycleSource :

525 cycle =

526 (⟨(FreeGroup.of x) ^ k.val * (FreeGroup.of y) ^ q *

527 ((FreeGroup.of x) ^ k.val)⁻¹, by

528 rw [MonoidHom.mem_ker]

529 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by

530 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,

531 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]

532 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod q) := by

533 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,

534 secondReductionCanonicalSourceMiddleIndex, Nat.reduceAdd, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,

535 secondReductionCanonicalSourceQuotientImage, Nat.succ_ne_self, ↓reduceIte, ofAdd_neg, φ, y, iMiddle]

536 rw [map_mul, map_inv, map_mul, map_pow, map_pow, hx, hy]

537 apply (Multiplicative.toAdd : Multiplicative (ZMod q) ≃ ZMod q).injective

538 simp only [ofAdd_neg, inv_pow, mul_inv_cancel_comm, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul,

539 CharP.cast_eq_zero, mul_one, neg_zero, toAdd_one]⟩ : φ.ker) := by

540 simpa [σ, φ, x, y, iMiddle, edge, lower, wrap, upper, cycle] using

541 secondReductionCanonicalSecondShiftedCycle_eq_conjugate_secondPower

542 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k

543 have hz : z = cycle ^ m₃' := by

544 apply Subtype.ext

545 change

546 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *

547 ((xWord σ iMiddle) ^ σ.periods iMiddle) *

548 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =

549 ((cycle ^ m₃' : φ.ker) : FreeGroup (FuchsianGenerator σ))

550 rw [show ((cycle ^ m₃' : φ.ker) : FreeGroup (FuchsianGenerator σ)) =

551 ((cycle : φ.ker) : FreeGroup (FuchsianGenerator σ)) ^ m₃' by

552 exact (map_pow (φ.ker.subtype) cycle m₃')]

553 have hcycleCoe :=

554 congrArg (fun u : φ.ker => (u : FreeGroup (FuchsianGenerator σ))) hcycleSource

555 have hcycleCoe' :

556 ((cycle : φ.ker) : FreeGroup (FuchsianGenerator σ)) =

557 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *

558 (FreeGroup.of y) ^ q *

559 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ := by

560 simpa using hcycleCoe

561 rw [hcycleCoe']

562 have hperiod : σ.periods iMiddle = q * m₃' := by

563 simp only [secondReductionCanonicalSourceSignature_period_middle, σ, iMiddle]

564 rw [hperiod]

565 simp only [secondReductionCanonicalDistinguishedGenerator, secondReductionCanonicalSourceMiddleIndex,

566 add_zero, xWord, Nat.reduceAdd, pow_mul, conj_pow, σ, x, iMiddle, y]

567 have hbasePower : (η (e.symm base)) ^ m₃' ∈ Subgroup.normalClosure

568 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

569 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

570 let idxB := secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨1, by decide⟩

571 let B :=

572 xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idxB)

573 have hTheta : θ B = e.symm base := by

574 simpa [σ, τ, e, θ, idxB, B, base] using

575 secondReductionCanonicalTransportToSchreierHom_negativeDistinguished

576 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

577 have hmod :

578 η (e.symm base) * B⁻¹ ∈ Subgroup.normalClosure

579 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

580 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

581 have htoInv :=

582 secondReductionToTransportSecondBranch_toInv_negDist_mem_blockRelators

583 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

584 change η (θ B) * B⁻¹ ∈ Subgroup.normalClosure

585 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

586 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) at htoInv

587 rw [hTheta] at htoInv

588 simpa using htoInv

589 have hBrel : B ^ m₃' ∈ Subgroup.normalClosure

590 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

591 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

592 have hmem :

593 (xWord τ

594 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idxB)) ^

595 τ.periods

596 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idxB) ∈

597 secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

598 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail :=

599 secondReductionCanonicalTransport_powerRelator_mem_blockRelators

600 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail _

601 simpa [τ, B, idxB, secondReductionTransportSignature,

602 familyFuchsianSignature_periods, secondReductionTransportPeriods,

603 singermanTransportPeriodsFamily, secondReductionSourceTransportPeriods,

604 secondReductionSourceCycleCount] using Subgroup.subset_normalClosure hmem

605 exact

606 ReidemeisterSchreier.Discrete.Presentations.pow_mem_normalClosure_of_mul_inv_mem

607 (R := secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

608 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)

609 (u := η (e.symm base)) (v := B) hmod hBrel

610 have htailSplit :

611 (List.ofFn (fun i : Fin (q - 1) => edge ⟨q - 1 - i.val, by omega⟩)).prod =

612 upper * lower := by

613 have hlist := secondReduction_list_ofFn_desc_split (p := q) (k := k.val) k.isLt edge

614 simpa [upper, lower] using congrArg List.prod hlist

615 have hbaseEq : base = (wrap * upper) * lower := by

616 have hdesc :

617 wrap *

618 (List.ofFn (fun i : Fin (q - 1) =>

619 edge ⟨q - 1 - i.val, by omega⟩)).prod =

620 base := by

621 simpa [σ, φ, edge, wrap, base] using

622 secondReductionCanonicalSecondDescendingCycle_eq_secondPowerKernel

623 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

624 rw [htailSplit] at hdesc

625 calc

626 base = wrap * (upper * lower) := hdesc.symm

627 _ = (wrap * upper) * lower := by group

628 let a := η (e.symm (wrap * upper))

629 let b := η (e.symm lower)

630 have hbaseAB : (a * b) ^ m₃' ∈ Subgroup.normalClosure

631 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

632 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

633 rw [hbaseEq] at hbasePower

634 simpa [a, b, map_mul, mul_assoc] using hbasePower

635 have hrot :

636 (b * a) ^ m₃' ∈ Subgroup.normalClosure

637 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

638 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) :=

639 ReidemeisterSchreier.Discrete.Presentations.cyclic_rotation_pow_mem_normalClosure

640 (R := secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

641 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)

642 (a := a) (b := b) hbaseAB

643 have hcycleTarget :

644 (η (e.symm cycle)) ^ m₃' ∈ Subgroup.normalClosure

645 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

646 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

647 have hcycleImage : η (e.symm cycle) = b * a := by

648 simp only [Lean.Elab.WF.paramLet, mul_assoc, map_mul, cycle, b, a]

649 simpa [hcycleImage] using hrot

650 change η (e.symm z) ∈ Subgroup.normalClosure

651 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

652 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)

653 rw [hz, map_pow]

654 simpa [cycle] using hcycleTarget

655

656end FenchelNielsen