Source: FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/TransportMaps.lean

1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.QuotientAndBasis

2

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/TransportMaps.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

18noncomputable def secondReductionCanonicalTransportToSchreierGenerator

19 {tailLen p q : ℕ}

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

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

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

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

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

25 let σ :=

26 secondReductionCanonicalSourceSignature

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

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

29 let hT :=

30 secondReductionCanonicalSchreierTransversal_isRightSchreierTransversal

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

32 SecondReductionTransportIndex tailLen p q → FreeGroup ↥(schreierGeneratorSet hT) := by

33 classical

34 dsimp

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

36 let σ :=

37 secondReductionCanonicalSourceSignature

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

39 let φ :=

40 secondReductionCanonicalSourceFreeQuotientHom

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

42 let x : FuchsianGenerator σ :=

43 secondReductionCanonicalDistinguishedGenerator

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

45 let y : FuchsianGenerator σ :=

46 FuchsianGenerator.elliptic

47 (secondReductionCanonicalSourceMiddleIndex

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

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

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

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

52 let hT :=

53 secondReductionCanonicalSchreierTransversal_isRightSchreierTransversal

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

55 let e :=

56 secondReductionCanonicalSchreierBasisEquiv

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

58 let distinguishedPos : φ.ker := ⟨(FreeGroup.of x) ^ q, by

59 rw [MonoidHom.mem_ker, map_pow, hx]

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

61 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩

62 let distinguishedNeg : φ.ker := ⟨(FreeGroup.of y) ^ q, by

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

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

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

66 secondReductionCanonicalSourceQuotientImage, Nat.succ_ne_self, ↓reduceIte, ofAdd_neg, φ, y]

67 rw [MonoidHom.mem_ker, map_pow, hy]

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

69 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,

70 neg_zero, toAdd_one]⟩

71 let zeroConjugateKernel :

72 (i : Fin σ.numPeriods) →

73 φ (xWord σ i) = 1 → Fin q → φ.ker := fun i hi k =>

74 ⟨(FreeGroup.of x) ^ k.val * xWord σ i * ((FreeGroup.of x) ^ k.val)⁻¹, by

75 change

76 φ ((FreeGroup.of x) ^ k.val * xWord σ i *

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

78 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hx, hi, mul_one, map_inv, mul_inv_cancel]⟩

79 intro idx

80 rcases idx with ⟨src, k⟩

81 cases src with

82 | inl head =>

83 by_cases h0 : head.val = 0

84 · let i :=

85 secondReductionCanonicalSourceZeroIndex

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

87 exact e.symm (zeroConjugateKernel i (by

88 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq, xWord,

89 secondReductionCanonicalSourceZeroIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,

90 secondReductionCanonicalSourceQuotientImage, OfNat.zero_ne_ofNat, ↓reduceIte, φ, i]) k)

91 · have h1 : head.val = 1 := by omega

92 let i :=

93 secondReductionCanonicalSourceOneIndex

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

95 exact e.symm (zeroConjugateKernel i (by

96 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq, xWord,

97 secondReductionCanonicalSourceOneIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,

98 secondReductionCanonicalSourceQuotientImage, OfNat.one_ne_ofNat, ↓reduceIte, φ, i]) k)

99 | inr rest =>

100 cases rest with

101 | inl distinguished =>

102 by_cases h0 : distinguished.val = 0

103 · exact e.symm distinguishedPos

104 · have h1 : distinguished.val = 1 := by omega

105 exact e.symm distinguishedNeg

106 | inr rest =>

107 cases rest with

108 | inl r =>

109 let i :=

110 secondReductionCanonicalSourceMiddleIndex

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

112 ⟨2 + r.val, by omega⟩

113 exact e.symm (zeroConjugateKernel i (by

114 have hnot3 : ¬ 2 + (2 + r.val) = 3 := by omega

115 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq, xWord,

116 secondReductionCanonicalSourceMiddleIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,

117 secondReductionCanonicalSourceQuotientImage, Nat.add_eq_left, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and,

118 ↓reduceIte, hnot3, φ, i]) k)

119 | inr jk =>

120 rcases jk with ⟨j, b⟩

121 let i :=

122 secondReductionCanonicalSourceTailIndex

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

124 exact e.symm (zeroConjugateKernel i (by

125 have hnot2 : ¬ 2 + p + b.val * tailLen + j.val = 2 := by omega

126 have hnot3 : ¬ 2 + p + b.val * tailLen + j.val = 3 := by omega

127 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq, xWord,

128 secondReductionCanonicalSourceTailIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,

129 secondReductionCanonicalSourceQuotientImage, hnot2, ↓reduceIte, hnot3, φ, i]) k)

130noncomputable def secondReductionCanonicalTransportToSchreierGeneratorImage

131 {tailLen p q : ℕ}

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

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

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

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

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

137 let σ :=

138 secondReductionCanonicalSourceSignature

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

140 let τ :=

141 secondReductionTransportSignature (p := p) hq

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

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

144 let hT :=

145 secondReductionCanonicalSchreierTransversal_isRightSchreierTransversal

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

147 FuchsianGenerator τ → FreeGroup ↥(schreierGeneratorSet hT)

148 | .elliptic i =>

149 secondReductionCanonicalTransportToSchreierGenerator

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

151 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)).symm i)

152 | .surfaceA _ => 1

153 | .surfaceB _ => 1

154noncomputable def secondReductionCanonicalTransportToSchreierHom

155 {tailLen p q : ℕ}

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

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

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

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

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

161 let σ :=

162 secondReductionCanonicalSourceSignature

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

164 let τ :=

165 secondReductionTransportSignature (p := p) hq

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

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

168 let hT :=

169 secondReductionCanonicalSchreierTransversal_isRightSchreierTransversal

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

171 FreeGroup (FuchsianGenerator τ) →* FreeGroup ↥(schreierGeneratorSet hT) :=

172 FreeGroup.lift

173 (secondReductionCanonicalTransportToSchreierGeneratorImage

174 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)

175private theorem secondReductionCanonicalTransportSchreierGenerator_power_mem_normalClosure

176 {tailLen p q : ℕ}

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

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

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

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

181 (idx : SecondReductionTransportIndex tailLen p q) :

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

183 let σ :=

184 secondReductionCanonicalSourceSignature

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

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

187 let e :=

188 secondReductionCanonicalSchreierBasisEquiv

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

190 (secondReductionCanonicalTransportToSchreierGenerator

191 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail idx) ^

192 secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail idx ∈

193 Subgroup.normalClosure

194 (ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet

195 (f := ellipticQuotientGeneratorImage σ

196 (secondReductionCanonicalSourceQuotientImage

197 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))

198 (rels := relators σ)

199 (secondReductionCanonicalSchreierTransversal

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

201 classical

202 dsimp

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

204 let σ :=

205 secondReductionCanonicalSourceSignature

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

207 let φ :=

208 secondReductionCanonicalSourceFreeQuotientHom

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

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

211 let hT :=

212 secondReductionCanonicalSchreierTransversal_isRightSchreierTransversal

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

214 let e :=

215 secondReductionCanonicalSchreierBasisEquiv

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

217 let hrels :=

218 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

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

220 let x : FuchsianGenerator σ :=

221 secondReductionCanonicalDistinguishedGenerator

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

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

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

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

226 rcases idx with ⟨src, k⟩

227 cases src with

228 | inl head =>

229 fin_cases head

230 · let i :=

231 secondReductionCanonicalSourceZeroIndex

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

233 let z : φ.ker :=

234 ⟨(FreeGroup.of x) ^ k.val * xWord σ i * ((FreeGroup.of x) ^ k.val)⁻¹, by

235 change

236 φ ((FreeGroup.of x) ^ k.val * xWord σ i *

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

238 have hi : φ (xWord σ i) = 1 := by

239 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq, xWord,

240 secondReductionCanonicalSourceZeroIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,

241 secondReductionCanonicalSourceQuotientImage, OfNat.zero_ne_ofNat, ↓reduceIte, φ, i]

242 simp only [Lean.Elab.WF.paramLet, Fin.zero_eta, Fin.isValue, map_mul, map_pow, hx, hi, mul_one, map_inv,

243 mul_inv_cancel]⟩

244 have hpowRel : (xWord σ i) ^ m₁' ∈ relators σ := by

245 have hrel : (xWord σ i) ^ σ.periods i ∈ relators σ := Or.inl ⟨i, rfl⟩

246 simpa [σ, i] using hrel

247 have hkSource : ((z ^ m₁' : φ.ker) : FreeGroup (FuchsianGenerator σ)) ∈

248 Subgroup.normalClosure (relators σ) := by

249 change

250 ((FreeGroup.of x) ^ k.val * xWord σ i *

251 ((FreeGroup.of x) ^ k.val)⁻¹) ^ m₁' ∈

252 Subgroup.normalClosure (relators σ)

253 exact conjugate_pow_mem_normalClosure_of_pow_mem

254 (G := FreeGroup (FuchsianGenerator σ)) (R := relators σ)

255 (x := xWord σ i) (g := (FreeGroup.of x) ^ k.val) (n := m₁') hpowRel

256 have hmem :

257 (e.symm z) ^ m₁' ∈

258 Subgroup.normalClosure

259 (ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e

260 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet

261 (f := ellipticQuotientGeneratorImage σ

262 (secondReductionCanonicalSourceQuotientImage

263 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))

264 (rels := relators σ)

265 (secondReductionCanonicalSchreierTransversal

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

267 rw [← map_pow]

268 exact

269 ReidemeisterSchreier.Discrete.Presentations.freeGroupPullback_transversalRelator_mem_normalClosure_of_mem_normalClosure

270 hrels hT.1 e hkSource

271 simpa [σ, φ, hT, e, hrels, x, hx, i, z,

272 secondReductionCanonicalTransportToSchreierGenerator,

273 secondReductionTransportPeriods, singermanTransportPeriodsFamily,

274 secondReductionSourceTransportPeriods, secondReductionSourceCycleCount, twoPeriods]

275 using hmem

276 · let i :=

277 secondReductionCanonicalSourceOneIndex

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

279 let z : φ.ker :=

280 ⟨(FreeGroup.of x) ^ k.val * xWord σ i * ((FreeGroup.of x) ^ k.val)⁻¹, by

281 change

282 φ ((FreeGroup.of x) ^ k.val * xWord σ i *

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

284 have hi : φ (xWord σ i) = 1 := by

285 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq, xWord,

286 secondReductionCanonicalSourceOneIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,

287 secondReductionCanonicalSourceQuotientImage, OfNat.one_ne_ofNat, ↓reduceIte, φ, i]

288 simp only [Lean.Elab.WF.paramLet, Fin.mk_one, Fin.isValue, map_mul, map_pow, hx, hi, mul_one, map_inv,

289 mul_inv_cancel]⟩

290 have hpowRel : (xWord σ i) ^ m₂' ∈ relators σ := by

291 have hrel : (xWord σ i) ^ σ.periods i ∈ relators σ := Or.inl ⟨i, rfl⟩

292 simpa [σ, i] using hrel

293 have hkSource : ((z ^ m₂' : φ.ker) : FreeGroup (FuchsianGenerator σ)) ∈

294 Subgroup.normalClosure (relators σ) := by

295 change

296 ((FreeGroup.of x) ^ k.val * xWord σ i *

297 ((FreeGroup.of x) ^ k.val)⁻¹) ^ m₂' ∈

298 Subgroup.normalClosure (relators σ)

299 exact conjugate_pow_mem_normalClosure_of_pow_mem

300 (G := FreeGroup (FuchsianGenerator σ)) (R := relators σ)

301 (x := xWord σ i) (g := (FreeGroup.of x) ^ k.val) (n := m₂') hpowRel

302 have hmem :

303 (e.symm z) ^ m₂' ∈

304 Subgroup.normalClosure

305 (ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e

306 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet

307 (f := ellipticQuotientGeneratorImage σ

308 (secondReductionCanonicalSourceQuotientImage

309 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))

310 (rels := relators σ)

311 (secondReductionCanonicalSchreierTransversal

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

313 rw [← map_pow]

314 exact

315 ReidemeisterSchreier.Discrete.Presentations.freeGroupPullback_transversalRelator_mem_normalClosure_of_mem_normalClosure

316 hrels hT.1 e hkSource

317 simpa [σ, φ, hT, e, hrels, x, hx, i, z,

318 secondReductionCanonicalTransportToSchreierGenerator,

319 secondReductionTransportPeriods, singermanTransportPeriodsFamily,

320 secondReductionSourceTransportPeriods, secondReductionSourceCycleCount, twoPeriods]

321 using hmem

322 | inr rest =>

323 cases rest with

324 | inl distinguished =>

325 fin_cases distinguished

326 · let i :=

327 secondReductionCanonicalSourceMiddleIndex

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

329 let z : φ.ker := ⟨(FreeGroup.of x) ^ q, by

330 rw [MonoidHom.mem_ker, map_pow, hx]

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

332 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩

333 have hpowRel : (xWord σ i) ^ (q * m₃') ∈ relators σ := by

334 have hrel : (xWord σ i) ^ σ.periods i ∈ relators σ := Or.inl ⟨i, rfl⟩

335 simpa [σ, i] using hrel

336 have hkSource : ((z ^ m₃' : φ.ker) : FreeGroup (FuchsianGenerator σ)) ∈

337 Subgroup.normalClosure (relators σ) := by

338 change ((FreeGroup.of x) ^ q) ^ m₃' ∈ Subgroup.normalClosure (relators σ)

339 have hxword : FreeGroup.of x = xWord σ i := by

340 simp only [secondReductionCanonicalDistinguishedGenerator, xWord, x, i]

341 rw [← pow_mul]

342 simpa [hxword] using Subgroup.subset_normalClosure hpowRel

343 have hmem :

344 (e.symm z) ^ m₃' ∈

345 Subgroup.normalClosure

346 (ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e

347 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet

348 (f := ellipticQuotientGeneratorImage σ

349 (secondReductionCanonicalSourceQuotientImage

350 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))

351 (rels := relators σ)

352 (secondReductionCanonicalSchreierTransversal

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

354 rw [← map_pow]

355 exact

356 ReidemeisterSchreier.Discrete.Presentations.freeGroupPullback_transversalRelator_mem_normalClosure_of_mem_normalClosure

357 hrels hT.1 e hkSource

358 simpa [σ, φ, hT, e, hrels, x, hx, i, z,

359 secondReductionCanonicalTransportToSchreierGenerator,

360 secondReductionTransportPeriods, singermanTransportPeriodsFamily,

361 secondReductionSourceTransportPeriods, secondReductionSourceCycleCount]

362 using hmem

363 · let i :=

364 secondReductionCanonicalSourceMiddleIndex

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

366 let y : FuchsianGenerator σ := FuchsianGenerator.elliptic i

367 let z : φ.ker := ⟨(FreeGroup.of y) ^ q, by

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

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

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

371 secondReductionCanonicalSourceQuotientImage, Nat.succ_ne_self, ↓reduceIte, ofAdd_neg, φ, y, i]

372 rw [MonoidHom.mem_ker, map_pow, hy]

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

374 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,

375 neg_zero, toAdd_one]⟩

376 have hpowRel : (xWord σ i) ^ (q * m₃') ∈ relators σ := by

377 have hrel : (xWord σ i) ^ σ.periods i ∈ relators σ := Or.inl ⟨i, rfl⟩

378 simpa [σ, i] using hrel

379 have hkSource : ((z ^ m₃' : φ.ker) : FreeGroup (FuchsianGenerator σ)) ∈

380 Subgroup.normalClosure (relators σ) := by

381 change ((FreeGroup.of y) ^ q) ^ m₃' ∈ Subgroup.normalClosure (relators σ)

382 have hyword : FreeGroup.of y = xWord σ i := by

383 simp only [xWord, y]

384 rw [← pow_mul]

385 simpa [hyword] using Subgroup.subset_normalClosure hpowRel

386 have hmem :

387 (e.symm z) ^ m₃' ∈

388 Subgroup.normalClosure

389 (ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e

390 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet

391 (f := ellipticQuotientGeneratorImage σ

392 (secondReductionCanonicalSourceQuotientImage

393 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))

394 (rels := relators σ)

395 (secondReductionCanonicalSchreierTransversal

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

397 rw [← map_pow]

398 exact

399 ReidemeisterSchreier.Discrete.Presentations.freeGroupPullback_transversalRelator_mem_normalClosure_of_mem_normalClosure

400 hrels hT.1 e hkSource

401 simpa [σ, φ, hT, e, hrels, x, hx, i, y, z,

402 secondReductionCanonicalTransportToSchreierGenerator,

403 secondReductionTransportPeriods, singermanTransportPeriodsFamily,

404 secondReductionSourceTransportPeriods, secondReductionSourceCycleCount]

405 using hmem

406 | inr rest =>

407 cases rest with

408 | inl r =>

409 let i :=

410 secondReductionCanonicalSourceMiddleIndex

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

412 ⟨2 + r.val, by omega⟩

413 let z : φ.ker :=

414 ⟨(FreeGroup.of x) ^ k.val * xWord σ i *

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

416 change

417 φ ((FreeGroup.of x) ^ k.val * xWord σ i *

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

419 have hi : φ (xWord σ i) = 1 := by

420 have hnot3 : ¬ 2 + (2 + r.val) = 3 := by omega

421 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq, xWord,

422 secondReductionCanonicalSourceMiddleIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,

423 secondReductionCanonicalSourceQuotientImage, Nat.add_eq_left, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and,

424 ↓reduceIte, hnot3, φ, i]

425 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hx, hi, mul_one, map_inv, mul_inv_cancel]⟩

426 have hpowRel : (xWord σ i) ^ (q * m₃') ∈ relators σ := by

427 have hrel : (xWord σ i) ^ σ.periods i ∈ relators σ := Or.inl ⟨i, rfl⟩

428 simpa [σ, i] using hrel

429 have hkSource : ((z ^ (q * m₃') : φ.ker) :

430 FreeGroup (FuchsianGenerator σ)) ∈

431 Subgroup.normalClosure (relators σ) := by

432 change

433 ((FreeGroup.of x) ^ k.val * xWord σ i *

434 ((FreeGroup.of x) ^ k.val)⁻¹) ^ (q * m₃') ∈

435 Subgroup.normalClosure (relators σ)

436 exact conjugate_pow_mem_normalClosure_of_pow_mem

437 (G := FreeGroup (FuchsianGenerator σ)) (R := relators σ)

438 (x := xWord σ i) (g := (FreeGroup.of x) ^ k.val)

439 (n := q * m₃') hpowRel

440 have hmem :

441 (e.symm z) ^ (q * m₃') ∈

442 Subgroup.normalClosure

443 (ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e

444 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet

445 (f := ellipticQuotientGeneratorImage σ

446 (secondReductionCanonicalSourceQuotientImage

447 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))

448 (rels := relators σ)

449 (secondReductionCanonicalSchreierTransversal

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

451 rw [← map_pow]

452 exact

453 ReidemeisterSchreier.Discrete.Presentations.freeGroupPullback_transversalRelator_mem_normalClosure_of_mem_normalClosure

454 hrels hT.1 e hkSource

455 simpa [σ, φ, hT, e, hrels, x, hx, i, z,

456 secondReductionCanonicalTransportToSchreierGenerator,

457 secondReductionTransportPeriods, singermanTransportPeriodsFamily,

458 secondReductionSourceTransportPeriods, secondReductionSourceCycleCount]

459 using hmem

460 | inr jk =>

461 rcases jk with ⟨j, b⟩

462 let i :=

463 secondReductionCanonicalSourceTailIndex

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

465 let z : φ.ker :=

466 ⟨(FreeGroup.of x) ^ k.val * xWord σ i *

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

468 change

469 φ ((FreeGroup.of x) ^ k.val * xWord σ i *

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

471 have hi : φ (xWord σ i) = 1 := by

472 have hnot2 : ¬ 2 + p + b.val * tailLen + j.val = 2 := by omega

473 have hnot3 : ¬ 2 + p + b.val * tailLen + j.val = 3 := by omega

474 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq, xWord,

475 secondReductionCanonicalSourceTailIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,

476 secondReductionCanonicalSourceQuotientImage, hnot2, ↓reduceIte, hnot3, φ, i]

477 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hx, hi, mul_one, map_inv, mul_inv_cancel]⟩

478 have hpowRel : (xWord σ i) ^ tail j ∈ relators σ := by

479 have hrel : (xWord σ i) ^ σ.periods i ∈ relators σ := Or.inl ⟨i, rfl⟩

480 simpa [σ, i] using hrel

481 have hkSource : ((z ^ tail j : φ.ker) : FreeGroup (FuchsianGenerator σ)) ∈

482 Subgroup.normalClosure (relators σ) := by

483 change

484 ((FreeGroup.of x) ^ k.val * xWord σ i *

485 ((FreeGroup.of x) ^ k.val)⁻¹) ^ tail j ∈

486 Subgroup.normalClosure (relators σ)

487 exact conjugate_pow_mem_normalClosure_of_pow_mem

488 (G := FreeGroup (FuchsianGenerator σ)) (R := relators σ)

489 (x := xWord σ i) (g := (FreeGroup.of x) ^ k.val)

490 (n := tail j) hpowRel

491 have hmem :

492 (e.symm z) ^ tail j ∈

493 Subgroup.normalClosure

494 (ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e

495 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet

496 (f := ellipticQuotientGeneratorImage σ

497 (secondReductionCanonicalSourceQuotientImage

498 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))

499 (rels := relators σ)

500 (secondReductionCanonicalSchreierTransversal

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

502 rw [← map_pow]

503 exact

504 ReidemeisterSchreier.Discrete.Presentations.freeGroupPullback_transversalRelator_mem_normalClosure_of_mem_normalClosure

505 hrels hT.1 e hkSource

506 simpa [σ, φ, hT, e, hrels, x, hx, i, z,

507 secondReductionCanonicalTransportToSchreierGenerator,

508 secondReductionTransportPeriods, singermanTransportPeriodsFamily,

509 secondReductionSourceTransportPeriods, secondReductionSourceCycleCount]

510 using hmem

511theorem secondReductionCanonicalTransportToSchreier_powerRelator_mem_normalClosure

512 {tailLen p q : ℕ}

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

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

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

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

517 (i :

518 Fin

519 (secondReductionTransportSignature (p := p) hq

520 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail).numPeriods) :

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

522 let σ :=

523 secondReductionCanonicalSourceSignature

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

525 let τ :=

526 secondReductionTransportSignature (p := p) hq

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

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

529 let e :=

530 secondReductionCanonicalSchreierBasisEquiv

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

532 secondReductionCanonicalTransportToSchreierHom

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

534 ((xWord τ i) ^ τ.periods i) ∈

535 Subgroup.normalClosure

536 (ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet

537 (f := ellipticQuotientGeneratorImage σ

538 (secondReductionCanonicalSourceQuotientImage

539 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))

540 (rels := relators σ)

541 (secondReductionCanonicalSchreierTransversal

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

543 classical

544 dsimp

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

546 let τ :=

547 secondReductionTransportSignature (p := p) hq

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

549 let idx : SecondReductionTransportIndex tailLen p q :=

550 (Fintype.equivFin (SecondReductionTransportIndex tailLen p q)).symm i

551 have hi : (Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx = i := by

552 simp only [Equiv.apply_symm_apply, idx]

553 rw [← hi]

554 simpa [τ, idx, secondReductionCanonicalTransportToSchreierHom,

555 secondReductionCanonicalTransportToSchreierGeneratorImage,

556 secondReductionTransportSignature, familyFuchsianSignature_periods, xWord] using

557 secondReductionCanonicalTransportSchreierGenerator_power_mem_normalClosure

558 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail idx

559end FenchelNielsen