FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/Reindexing.lean

1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.ZeroGenus.CleanupData

2import FenchelNielsenZomorrodian.Discrete.Singerman.CyclicSchreierKernel

4/-

5PUBLIC_PAGE_SNAPSHOT

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

7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/Reindexing.lean

8translation_root: data/translation

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

10placement: after imports, never before imports

11-/

12/-!

13# Compact zero-genus three-step proof data

15Organizes first and second reduction data, perfectness numerics, reindexing, cleanup data, and the final zero-genus three-step finite-index theorem.

16-/

18namespace FenchelNielsen

19private theorem fin_eq_zero_elim {n : ℕ} (h : n = 0) (i : Fin n) : False := by

20 exact Nat.not_lt_zero i (by simpa [h] using i.2)

21private theorem fin_eq_zero_or_one_or_succ_succ_of_eq_add_two

22 {m n : ℕ} (h : m = n + 2) (i : Fin m) :

23 i = Fin.cast h.symm (0 : Fin (n + 2)) ∨

24 i = Fin.cast h.symm (1 : Fin (n + 2)) ∨

25 ∃ k : Fin n, i = Fin.cast h.symm k.succ.succ := by

26 generalize hj : Fin.cast h i = j

27 have hij : i = Fin.cast h.symm j := by

28 rw [← hj]

29 simp only [Fin.cast_cast, Fin.cast_eq_self]

30 cases j using Fin.cases with

31 | zero =>

32 left

33 exact hij

34 | succ j =>

35 cases j using Fin.cases with

36 | zero =>

37 right

38 left

39 exact hij

40 | succ k =>

41 right

42 right

43 exact ⟨k, hij⟩

44private theorem fin_eq_prefix_or_zero_or_one_or_tail_of_eq_add_two

45 {m k n : ℕ} (h : m = k + (n + 2)) (i : Fin m) :

46 (∃ j : Fin k, i = Fin.cast h.symm (Fin.castAdd (n + 2) j)) ∨

47 i = Fin.cast h.symm (Fin.natAdd k (0 : Fin (n + 2))) ∨

48 i = Fin.cast h.symm (Fin.natAdd k (1 : Fin (n + 2))) ∨

49 ∃ t : Fin n, i = Fin.cast h.symm (Fin.natAdd k t.succ.succ) := by

50 generalize hj : Fin.cast h i = j

51 have hij : i = Fin.cast h.symm j := by

52 rw [← hj]

53 simp only [Fin.cast_cast, Fin.cast_eq_self]

54 cases j using Fin.addCases with

55 | left j =>

56 left

57 exact ⟨j, hij⟩

58 | right j =>

59 rcases fin_eq_zero_or_one_or_succ_succ_of_eq_add_two rfl j with rfl | rfl | ⟨t, rfl⟩

60 · right

61 left

62 exact hij

63 · right

64 right

65 left

66 exact hij

67 · right

68 right

69 right

70 exact ⟨t, hij⟩

71private theorem List.map_finRange_fin_cast {α : Type*} {m n : ℕ} (h : m = n)

72 (f : Fin n → α) :

73 (List.finRange m).map (fun i => f (Fin.cast h i)) = (List.finRange n).map f := by

74 cases h

75 rfl

76private noncomputable def zeroGenusOrderedGeneratorEquiv

77 (σ τ : FuchsianSignature)

78 (hσZero : σ.orbitGenus = 0) (hτZero : τ.orbitGenus = 0)

79 (hNum : σ.numPeriods = τ.numPeriods) :

80 FuchsianGenerator σ ≃ FuchsianGenerator τ where

81 toFun

82 | .elliptic i => .elliptic (Fin.cast hNum i)

83 | .surfaceA j => False.elim (fin_eq_zero_elim hσZero j)

84 | .surfaceB j => False.elim (fin_eq_zero_elim hσZero j)

85 invFun

86 | .elliptic i => .elliptic (Fin.cast hNum.symm i)

87 | .surfaceA j => False.elim (fin_eq_zero_elim hτZero j)

88 | .surfaceB j => False.elim (fin_eq_zero_elim hτZero j)

89 left_inv := by

90 intro x

91 cases x with

92 | elliptic i => simp

93 | surfaceA j => exact False.elim (fin_eq_zero_elim hσZero j)

94 | surfaceB j => exact False.elim (fin_eq_zero_elim hσZero j)

95 right_inv := by

96 intro x

97 cases x with

98 | elliptic i => simp

99 | surfaceA j => exact False.elim (fin_eq_zero_elim hτZero j)

100 | surfaceB j => exact False.elim (fin_eq_zero_elim hτZero j)

101private theorem zeroGenusOrderedGeneratorEquiv_totalRelation

102 (σ τ : FuchsianSignature)

103 (hσZero : σ.orbitGenus = 0) (hτZero : τ.orbitGenus = 0)

104 (hNum : σ.numPeriods = τ.numPeriods) :

105 FreeGroup.freeGroupCongr

106 (zeroGenusOrderedGeneratorEquiv σ τ hσZero hτZero hNum)

107 (totalRelation σ) =

108 totalRelation τ := by

109 let eGen := zeroGenusOrderedGeneratorEquiv σ τ hσZero hτZero hNum

110 have hEll :

111 (List.map

112 (fun i : Fin σ.numPeriods =>

113 xWord τ (Fin.cast hNum i))

114 (List.finRange σ.numPeriods)).prod =

115 (List.map (fun i : Fin τ.numPeriods => xWord τ i)

116 (List.finRange τ.numPeriods)).prod := by

117 rw [List.map_finRange_fin_cast hNum (fun i : Fin τ.numPeriods => xWord τ i)]

118 rw [totalRelation, map_mul, map_list_prod, map_list_prod, List.map_map, List.map_map]

119 have hEllMap :

120 ((fun x : FreeGroup (FuchsianGenerator σ) => FreeGroup.freeGroupCongr eGen x) ∘

121 (fun i : Fin σ.numPeriods => xWord σ i)) =

122 fun i : Fin σ.numPeriods => xWord τ (Fin.cast hNum i) := by

123 funext i

124 simp only [zeroGenusOrderedGeneratorEquiv, FreeGroup.freeGroupCongr_apply, Equiv.coe_fn_mk, xWord,

125 Function.comp_apply, FreeGroup.map.of, eGen]

126 rw [hEllMap, hEll]

127 have hSurfaceRangeSource :

128 (List.finRange σ.orbitGenus : List (Fin σ.orbitGenus)) = [] := by

129 apply List.eq_nil_iff_forall_not_mem.2

130 intro j _hj

131 exact fin_eq_zero_elim hσZero j

132 have hSurfaceRangeTarget :

133 (List.finRange τ.orbitGenus : List (Fin τ.orbitGenus)) = [] := by

134 apply List.eq_nil_iff_forall_not_mem.2

135 intro j _hj

136 exact fin_eq_zero_elim hτZero j

137 have hSurfaceSource :

138 (List.map

139 ((fun x : FreeGroup (FuchsianGenerator σ) => FreeGroup.freeGroupCongr eGen x) ∘

140 fun j : Fin σ.orbitGenus => ⁅aWord σ j, bWord σ j⁆)

141 (List.finRange σ.orbitGenus)).prod = 1 := by

142 rw [hSurfaceRangeSource]

143 simp only [FreeGroup.freeGroupCongr_apply, List.map_nil, List.prod_nil]

144 have hSurfaceTarget :

145 (List.map (fun j : Fin τ.orbitGenus => ⁅aWord τ j, bWord τ j⁆)

146 (List.finRange τ.orbitGenus)).prod = 1 := by

147 rw [hSurfaceRangeTarget]

148 simp only [List.map_nil, List.prod_nil]

149 rw [totalRelation, hSurfaceSource, hSurfaceTarget]

150private theorem zeroGenusFuchsianPresentedGroupEquivOfOrderedPeriods

151 (σ τ : FuchsianSignature)

152 (hσZero : σ.orbitGenus = 0) (hτZero : τ.orbitGenus = 0)

153 (hNum : σ.numPeriods = τ.numPeriods)

154 (hPeriods : ∀ i, σ.periods i = τ.periods (Fin.cast hNum i)) :

155 Nonempty (FuchsianPresentedGroup σ ≃* FuchsianPresentedGroup τ) := by

156 classical

157 let eGen := zeroGenusOrderedGeneratorEquiv σ τ hσZero hτZero hNum

158 have hRelators :

159 FreeGroup.freeGroupCongr eGen '' relators σ = relators τ := by

160 ext w

161 constructor

162 · rintro ⟨r, hr, rfl⟩

163 rcases hr with ⟨i, rfl⟩ | rfl

164 · left

165 refine ⟨Fin.cast hNum i, ?_⟩

166 simp only [zeroGenusOrderedGeneratorEquiv, xWord, hPeriods i, FreeGroup.freeGroupCongr_apply, Equiv.coe_fn_mk,

167 map_pow, FreeGroup.map.of, eGen]

168 · right

169 simpa [eGen] using

170 zeroGenusOrderedGeneratorEquiv_totalRelation σ τ hσZero hτZero hNum

171 · intro hw

172 rcases hw with ⟨i, rfl⟩ | rfl

173 · refine ⟨(xWord σ (Fin.cast hNum.symm i)) ^ σ.periods (Fin.cast hNum.symm i),

174 Or.inl ⟨Fin.cast hNum.symm i, rfl⟩, ?_⟩

175 have hperiod := hPeriods (Fin.cast hNum.symm i)

176 simp only [zeroGenusOrderedGeneratorEquiv, xWord, hperiod, Fin.cast_cast, Fin.cast_eq_self,

177 FreeGroup.freeGroupCongr_apply, Equiv.coe_fn_mk, map_pow, FreeGroup.map.of, eGen]

178 · refine ⟨totalRelation σ, Or.inr rfl, ?_⟩

179 simpa [eGen] using

180 zeroGenusOrderedGeneratorEquiv_totalRelation σ τ hσZero hτZero hNum

181 exact

182 ⟨(PresentedGroup.equivPresentedGroup (relators σ) eGen).trans

183 (QuotientGroup.quotientMulEquivOfEq (by rw [hRelators]))⟩

184theorem conjugate_mem_normalClosure_of_mem

185 {G : Type*} [Group G] {R : Set G} {r g : G}

186 (h : r ∈ R) :

187 g * r * g⁻¹ ∈ Subgroup.normalClosure R := by

188 let N : Subgroup G := Subgroup.normalClosure R

189 have hr : r ∈ N := Subgroup.subset_normalClosure h

190 simpa [N, MulAut.conj_apply] using

191 (Subgroup.normalClosure_normal.conj_mem r hr g)

192theorem conjugate_pow_mem_normalClosure_of_pow_mem

193 {G : Type*} [Group G] {R : Set G} {x g : G} {n : ℕ}

194 (h : x ^ n ∈ R) :

195 (g * x * g⁻¹) ^ n ∈ Subgroup.normalClosure R := by

196 rw [conj_pow]

197 exact conjugate_mem_normalClosure_of_mem h

198private theorem image_powerRelator_mem_normalClosure_of_conjugate_xWord

199 (σ τ : FuchsianSignature)

200 (η : FreeGroup (FuchsianGenerator σ) →* FreeGroup (FuchsianGenerator τ))

201 (i : Fin σ.numPeriods) (j : Fin τ.numPeriods)

202 (g : FreeGroup (FuchsianGenerator τ))

203 (hImage : η (xWord σ i) = g * xWord τ j * g⁻¹)

204 (hPeriod : σ.periods i = τ.periods j) :

205 η ((xWord σ i) ^ σ.periods i) ∈ Subgroup.normalClosure (relators τ) := by

206 rw [map_pow, hImage, hPeriod]

207 exact conjugate_pow_mem_normalClosure_of_pow_mem

208 (G := FreeGroup (FuchsianGenerator τ)) (R := relators τ)

209 (x := xWord τ j) (g := g) (n := τ.periods j)

210 (Or.inl ⟨j, rfl⟩)

211private theorem image_totalRelation_mem_normalClosure_of_eq

212 (σ τ : FuchsianSignature)

213 (η : FreeGroup (FuchsianGenerator σ) →* FreeGroup (FuchsianGenerator τ))

214 (hImage : η (totalRelation σ) = totalRelation τ) :

215 η (totalRelation σ) ∈ Subgroup.normalClosure (relators τ) := by

216 rw [hImage]

217 exact Subgroup.subset_normalClosure (Or.inr rfl)

218private theorem freeGroup_hom_mul_inv_mem_of_generator_mul_inv

219 {X G : Type*} [Group G] {N : Subgroup G} [N.Normal]

220 (f g : FreeGroup X →* G)

221 (hgen : ∀ x : X, f (FreeGroup.of x) * (g (FreeGroup.of x))⁻¹ ∈ N) :

222 ∀ x : FreeGroup X, f x * (g x)⁻¹ ∈ N := by

223 let q : G →* G ⧸ N := QuotientGroup.mk' N

224 have hq : q.comp f = q.comp g := by

225 apply FreeGroup.ext_hom

226 intro x

227 have hx : (f (FreeGroup.of x) * (g (FreeGroup.of x))⁻¹ : G ⧸ N) = 1 :=

228 (QuotientGroup.eq_one_iff _).2 (hgen x)

229 have hx' : q (f (FreeGroup.of x)) * (q (g (FreeGroup.of x)))⁻¹ = 1 := by

230 simpa [q] using hx

231 exact mul_inv_eq_one.mp hx'

232 intro x

233 have hx : q (f x) = q (g x) :=

234 DFunLike.congr_fun hq x

235 apply (QuotientGroup.eq_one_iff (f x * (g x)⁻¹)).1

236 have hxone : q (f x * (g x)⁻¹) = 1 := by

237 rw [map_mul, map_inv, hx, mul_inv_cancel]

238 simpa [q] using hxone

239private theorem freeGroup_hom_mul_inv_mem_normalClosure_of_generator_mul_inv

240 {X G : Type*} [Group G] {R : Set G}

241 (f g : FreeGroup X →* G)

242 (hgen :

243 ∀ x : X, f (FreeGroup.of x) * (g (FreeGroup.of x))⁻¹ ∈

244 Subgroup.normalClosure R) :

245 ∀ x : FreeGroup X, f x * (g x)⁻¹ ∈ Subgroup.normalClosure R :=

246 freeGroup_hom_mul_inv_mem_of_generator_mul_inv f g hgen

247private theorem zeroGenusFuchsianPresentedGroupEquivOfConjugateEllipticMutualMaps_memTotal

248 (σ τ : FuchsianSignature)

249 (hσZero : σ.orbitGenus = 0) (hτZero : τ.orbitGenus = 0)

250 (η : FreeGroup (FuchsianGenerator σ) →* FreeGroup (FuchsianGenerator τ))

251 (θ : FreeGroup (FuchsianGenerator τ) →* FreeGroup (FuchsianGenerator σ))

252 (ηIndex : Fin σ.numPeriods → Fin τ.numPeriods)

253 (ηConj : Fin σ.numPeriods → FreeGroup (FuchsianGenerator τ))

254 (hηX :

255 ∀ i, η (xWord σ i) = ηConj i * xWord τ (ηIndex i) * (ηConj i)⁻¹)

256 (hηPeriod : ∀ i, σ.periods i = τ.periods (ηIndex i))

257 (hηTotal : η (totalRelation σ) ∈ Subgroup.normalClosure (relators τ))

258 (θIndex : Fin τ.numPeriods → Fin σ.numPeriods)

259 (θConj : Fin τ.numPeriods → FreeGroup (FuchsianGenerator σ))

260 (hθX :

261 ∀ i, θ (xWord τ i) = θConj i * xWord σ (θIndex i) * (θConj i)⁻¹)

262 (hθPeriod : ∀ i, τ.periods i = σ.periods (θIndex i))

263 (hθTotal : θ (totalRelation τ) ∈ Subgroup.normalClosure (relators σ))

264 (hθηEll :

265 ∀ i : Fin σ.numPeriods,

266 θ (η (xWord σ i)) * (xWord σ i)⁻¹ ∈ Subgroup.normalClosure (relators σ))

267 (hηθEll :

268 ∀ i : Fin τ.numPeriods,

269 η (θ (xWord τ i)) * (xWord τ i)⁻¹ ∈ Subgroup.normalClosure (relators τ)) :

270 Nonempty (FuchsianPresentedGroup σ ≃* FuchsianPresentedGroup τ) := by

271 refine ⟨ReidemeisterSchreier.Discrete.Presentations.quotientEquivOfRelatorsByMutualMaps

272 (relators σ) (relators τ) η θ ?_ ?_ ?_ ?_⟩

273 · rintro r (⟨i, rfl⟩ | rfl)

274 · exact image_powerRelator_mem_normalClosure_of_conjugate_xWord

275 σ τ η i (ηIndex i) (ηConj i) (hηX i) (hηPeriod i)

276 · exact hηTotal

277 · rintro s (⟨i, rfl⟩ | rfl)

278 exact image_powerRelator_mem_normalClosure_of_conjugate_xWord

279 τ σ θ i (θIndex i) (θConj i) (hθX i) (hθPeriod i)

280 · exact hθTotal

281 · exact freeGroup_hom_mul_inv_mem_normalClosure_of_generator_mul_inv

282 (θ.comp η) (MonoidHom.id (FreeGroup (FuchsianGenerator σ))) (by

283 intro x

284 cases x with

285 | elliptic i => simpa [xWord] using hθηEll i

286 | surfaceA j => exact False.elim (fin_eq_zero_elim hσZero j)

287 | surfaceB j => exact False.elim (fin_eq_zero_elim hσZero j))

288 · exact freeGroup_hom_mul_inv_mem_normalClosure_of_generator_mul_inv

289 (η.comp θ) (MonoidHom.id (FreeGroup (FuchsianGenerator τ))) (by

290 intro y

291 cases y with

292 | elliptic i => simpa [xWord] using hηθEll i

293 | surfaceA j => exact False.elim (fin_eq_zero_elim hτZero j)

294 | surfaceB j => exact False.elim (fin_eq_zero_elim hτZero j))

295private theorem zeroGenusAdjacentSwapFuchsianPresentedGroupEquiv

296 {k n : ℕ} (σ τ : FuchsianSignature)

297 (hσZero : σ.orbitGenus = 0) (hτZero : τ.orbitGenus = 0)

298 (hσNum : σ.numPeriods = k + (n + 2)) (hτNum : τ.numPeriods = k + (n + 2))

299 (hPeriodPrefix :

300 ∀ j : Fin k,

301 σ.periods (Fin.cast hσNum.symm (Fin.castAdd (n + 2) j)) =

302 τ.periods (Fin.cast hτNum.symm (Fin.castAdd (n + 2) j)))

303 (hPeriod0 :

304 σ.periods (Fin.cast hσNum.symm (Fin.natAdd k (0 : Fin (n + 2)))) =

305 τ.periods (Fin.cast hτNum.symm (Fin.natAdd k (1 : Fin (n + 2)))))

306 (hPeriod1 :

307 σ.periods (Fin.cast hσNum.symm (Fin.natAdd k (1 : Fin (n + 2)))) =

308 τ.periods (Fin.cast hτNum.symm (Fin.natAdd k (0 : Fin (n + 2)))))

309 (hPeriodTail :

310 ∀ t : Fin n,

311 σ.periods (Fin.cast hσNum.symm (Fin.natAdd k t.succ.succ)) =

312 τ.periods (Fin.cast hτNum.symm (Fin.natAdd k t.succ.succ))) :

313 Nonempty (FuchsianPresentedGroup σ ≃* FuchsianPresentedGroup τ) := by

314 let σ0 : Fin σ.numPeriods := Fin.cast hσNum.symm (Fin.natAdd k (0 : Fin (n + 2)))

315 let σ1 : Fin σ.numPeriods := Fin.cast hσNum.symm (Fin.natAdd k (1 : Fin (n + 2)))

316 let τ0 : Fin τ.numPeriods := Fin.cast hτNum.symm (Fin.natAdd k (0 : Fin (n + 2)))

317 let τ1 : Fin τ.numPeriods := Fin.cast hτNum.symm (Fin.natAdd k (1 : Fin (n + 2)))

318 let sameτ : Fin σ.numPeriods → Fin τ.numPeriods := fun i =>

319 Fin.cast hτNum.symm (Fin.cast hσNum i)

320 let sameσ : Fin τ.numPeriods → Fin σ.numPeriods := fun i =>

321 Fin.cast hσNum.symm (Fin.cast hτNum i)

322 have hσ10 : σ1 ≠ σ0 := by

323 intro h

324 have := congrArg (fun i : Fin σ.numPeriods => (Fin.cast hσNum i).val) h

325 simp only [Fin.cast_cast, Fin.cast_eq_self, Fin.val_natAdd, Fin.coe_ofNat_eq_mod, Nat.one_mod, Nat.zero_mod,

326 add_zero, Nat.add_eq_left, one_ne_zero, σ1, σ0] at this

327 have hτ10 : τ1 ≠ τ0 := by

328 intro h

329 have := congrArg (fun i : Fin τ.numPeriods => (Fin.cast hτNum i).val) h

330 simp only [Fin.cast_cast, Fin.cast_eq_self, Fin.val_natAdd, Fin.coe_ofNat_eq_mod, Nat.one_mod, Nat.zero_mod,

331 add_zero, Nat.add_eq_left, one_ne_zero, τ1, τ0] at this

332 have hprefix_ne_zero :

333 ∀ j : Fin k, (Fin.castAdd (n + 2) j : Fin (k + (n + 2))) ≠

334 Fin.natAdd k (0 : Fin (n + 2)) := by

335 intro j h

336 have := congrArg Fin.val h

337 simp only [Fin.val_castAdd, Fin.val_natAdd, Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero] at this

338 omega

339 have hprefix_ne_one :

340 ∀ j : Fin k, (Fin.castAdd (n + 2) j : Fin (k + (n + 2))) ≠

341 Fin.natAdd k (1 : Fin (n + 2)) := by

342 intro j h

343 have := congrArg Fin.val h

344 simp only [Fin.val_castAdd, Fin.val_natAdd, Fin.coe_ofNat_eq_mod, Nat.one_mod] at this

345 omega

346 have htail_ne_zero : ∀ t : Fin n, (t.succ.succ : Fin (n + 2)) ≠ 0 := by

347 intro t h

348 have := congrArg Fin.val h

349 simp only [Fin.val_succ, Fin.coe_ofNat_eq_mod, Nat.zero_mod, Nat.add_eq_zero_iff, one_ne_zero, and_false,

350 and_self] at this

351 have htail_ne_one : ∀ t : Fin n, (t.succ.succ : Fin (n + 2)) ≠ 1 := by

352 intro t h

353 have := congrArg Fin.val h

354 simp only [Fin.val_succ, Fin.coe_ofNat_eq_mod, Nat.one_mod, Nat.add_eq_right, Nat.add_eq_zero_iff,

355 one_ne_zero, and_false] at this

356 let η : FreeGroup (FuchsianGenerator σ) →* FreeGroup (FuchsianGenerator τ) :=

357 FreeGroup.lift fun

358 | .elliptic i =>

359 if i = σ0 then xWord τ τ1

360 else if i = σ1 then (xWord τ τ1)⁻¹ * xWord τ τ0 * xWord τ τ1

361 else xWord τ (sameτ i)

362 | .surfaceA j => False.elim (fin_eq_zero_elim hσZero j)

363 | .surfaceB j => False.elim (fin_eq_zero_elim hσZero j)

364 let θ : FreeGroup (FuchsianGenerator τ) →* FreeGroup (FuchsianGenerator σ) :=

365 FreeGroup.lift fun

366 | .elliptic i =>

367 if i = τ0 then xWord σ σ0 * xWord σ σ1 * (xWord σ σ0)⁻¹

368 else if i = τ1 then xWord σ σ0

369 else xWord σ (sameσ i)

370 | .surfaceA j => False.elim (fin_eq_zero_elim hτZero j)

371 | .surfaceB j => False.elim (fin_eq_zero_elim hτZero j)

372 let ηIndex : Fin σ.numPeriods → Fin τ.numPeriods := fun i =>

373 if i = σ0 then τ1 else if i = σ1 then τ0 else sameτ i

374 let ηConj : Fin σ.numPeriods → FreeGroup (FuchsianGenerator τ) := fun i =>

375 if i = σ1 then (xWord τ τ1)⁻¹ else 1

376 let θIndex : Fin τ.numPeriods → Fin σ.numPeriods := fun i =>

377 if i = τ0 then σ1 else if i = τ1 then σ0 else sameσ i

378 let θConj : Fin τ.numPeriods → FreeGroup (FuchsianGenerator σ) := fun i =>

379 if i = τ0 then xWord σ σ0 else 1

380 refine zeroGenusFuchsianPresentedGroupEquivOfConjugateEllipticMutualMaps_memTotal

381 σ τ hσZero hτZero η θ ηIndex ηConj ?_ ?_ ?_ θIndex θConj ?_ ?_ ?_ ?_ ?_

382 · intro i

383 rcases fin_eq_prefix_or_zero_or_one_or_tail_of_eq_add_two hσNum i with

384 ⟨j, rfl⟩ | rfl | rfl | ⟨t, rfl⟩

385 · simp only [xWord, Fin.cast_cast, FreeGroup.lift_apply_of, Fin.cast_inj, hprefix_ne_zero j, ↓reduceIte,

386 hprefix_ne_one j, one_mul, inv_one, mul_one, η, σ0, σ1, sameτ, ηConj, ηIndex]

387 · simp only [xWord, FreeGroup.lift_apply_of, ↓reduceIte, Fin.cast_inj, Fin.natAdd_inj, zero_ne_one, one_mul,

388 inv_one, mul_one, η, σ0, σ1, ηConj, ηIndex]

389 · simp only [xWord, FreeGroup.lift_apply_of, hσ10, ↓reduceIte, inv_inv, η, σ0, σ1, ηConj, ηIndex]

390 · simp only [xWord, Fin.cast_cast, FreeGroup.lift_apply_of, Fin.cast_inj, Fin.natAdd_inj, htail_ne_zero t,

391 ↓reduceIte, htail_ne_one t, one_mul, inv_one, mul_one, η, σ0, σ1, sameτ, ηConj, ηIndex]

392 · intro i

393 rcases fin_eq_prefix_or_zero_or_one_or_tail_of_eq_add_two hσNum i with

394 ⟨j, rfl⟩ | rfl | rfl | ⟨t, rfl⟩

395 · simpa [ηIndex, σ0, σ1, sameτ, hprefix_ne_zero j, hprefix_ne_one j] using

396 hPeriodPrefix j

397 · simpa [ηIndex, σ0, σ1] using hPeriod0

398 · simpa [ηIndex, σ0, σ1, hσ10] using hPeriod1

399 · simpa [ηIndex, σ0, σ1, sameτ, htail_ne_zero t, htail_ne_one t] using

400 hPeriodTail t

401 · apply image_totalRelation_mem_normalClosure_of_eq

402 rw [totalRelation, map_mul, map_list_prod]

403 have hSourceSurfaceRange : (List.finRange σ.orbitGenus : List (Fin σ.orbitGenus)) = [] := by

404 apply List.eq_nil_iff_forall_not_mem.2

405 intro j _hj

406 exact fin_eq_zero_elim hσZero j

407 have hTargetSurfaceRange : (List.finRange τ.orbitGenus : List (Fin τ.orbitGenus)) = [] := by

408 apply List.eq_nil_iff_forall_not_mem.2

409 intro j _hj

410 exact fin_eq_zero_elim hτZero j

411 rw [hSourceSurfaceRange]

412 rw [totalRelation, hTargetSurfaceRange]

413 rw [List.map_map, ← List.ofFn_eq_map]

414 rw [List.ofFn_congr hσNum]

415 rw [← List.ofFn_eq_map]

416 rw [List.ofFn_congr hτNum]

417 have hSourceList :

418 List.ofFn

419 (fun i : Fin (k + (n + 2)) =>

420 η (xWord σ (Fin.cast hσNum.symm i))) =

421 List.ofFn

422 (fun j : Fin k =>

423 η (xWord σ (Fin.cast hσNum.symm (Fin.castAdd (n + 2) j)))) ++

424 List.ofFn

425 (fun j : Fin (n + 2) =>

426 η (xWord σ (Fin.cast hσNum.symm (Fin.natAdd k j)))) := by

427 rw [← List.ofFn_fin_append]

428 congr

429 funext i

430 cases i using Fin.addCases <;> simp only [Fin.append_left, Fin.append_right]

431 have hTargetList :

432 List.ofFn

433 (fun i : Fin (k + (n + 2)) =>

434 xWord τ (Fin.cast hτNum.symm i)) =

435 List.ofFn

436 (fun j : Fin k =>

437 xWord τ (Fin.cast hτNum.symm (Fin.castAdd (n + 2) j))) ++

438 List.ofFn

439 (fun j : Fin (n + 2) =>

440 xWord τ (Fin.cast hτNum.symm (Fin.natAdd k j))) := by

441 rw [← List.ofFn_fin_append]

442 congr

443 funext i

444 cases i using Fin.addCases <;> simp only [Fin.append_left, Fin.append_right]

445 simp only [Function.comp_apply]

446 rw [hSourceList, hTargetList]

447 rw [List.ofFn_succ]

448 rw [List.ofFn_succ]

449 simp only [xWord, Fin.cast_cast, FreeGroup.lift_apply_of, Fin.cast_inj, hprefix_ne_zero, ↓reduceIte,

450 hprefix_ne_one, Fin.succ_zero_eq_one, Fin.natAdd_inj, one_ne_zero, Fin.succ_ne_zero, htail_ne_one, List.prod_append,

451 List.prod_cons, List.map_nil, List.prod_nil, map_one, mul_one, List.ofFn_succ, mul_right_inj, η, σ0, τ1, σ1, τ0,

452 sameτ]

453 group

454 · intro i

455 rcases fin_eq_prefix_or_zero_or_one_or_tail_of_eq_add_two hτNum i with

456 ⟨j, rfl⟩ | rfl | rfl | ⟨t, rfl⟩

457 · simp only [xWord, Fin.cast_cast, FreeGroup.lift_apply_of, Fin.cast_inj, hprefix_ne_zero j, ↓reduceIte,

458 hprefix_ne_one j, one_mul, inv_one, mul_one, θ, τ0, τ1, sameσ, θConj, θIndex]

459 · simp only [xWord, FreeGroup.lift_apply_of, ↓reduceIte, θ, τ0, τ1, θConj, θIndex]

460 · simp only [xWord, FreeGroup.lift_apply_of, hτ10, ↓reduceIte, one_mul, inv_one, mul_one, θ, τ0, τ1, θConj,

461 θIndex]

462 · simp only [xWord, Fin.cast_cast, FreeGroup.lift_apply_of, Fin.cast_inj, Fin.natAdd_inj, htail_ne_zero t,

463 ↓reduceIte, htail_ne_one t, one_mul, inv_one, mul_one, θ, τ0, τ1, sameσ, θConj, θIndex]

464 · intro i

465 rcases fin_eq_prefix_or_zero_or_one_or_tail_of_eq_add_two hτNum i with

466 ⟨j, rfl⟩ | rfl | rfl | ⟨t, rfl⟩

467 · simpa [θIndex, τ0, τ1, sameσ, hprefix_ne_zero j, hprefix_ne_one j] using

468 (hPeriodPrefix j).symm

469 · simpa [θIndex, τ0, τ1] using hPeriod1.symm

470 · simpa [θIndex, τ0, τ1, hτ10] using hPeriod0.symm

471 · simpa [θIndex, τ0, τ1, sameσ, htail_ne_zero t, htail_ne_one t] using

472 (hPeriodTail t).symm

473 · apply image_totalRelation_mem_normalClosure_of_eq

474 rw [totalRelation, map_mul, map_list_prod]

475 have hSourceSurfaceRange : (List.finRange τ.orbitGenus : List (Fin τ.orbitGenus)) = [] := by

476 apply List.eq_nil_iff_forall_not_mem.2

477 intro j _hj

478 exact fin_eq_zero_elim hτZero j

479 have hTargetSurfaceRange : (List.finRange σ.orbitGenus : List (Fin σ.orbitGenus)) = [] := by

480 apply List.eq_nil_iff_forall_not_mem.2

481 intro j _hj

482 exact fin_eq_zero_elim hσZero j

483 rw [hSourceSurfaceRange]

484 rw [totalRelation, hTargetSurfaceRange]

485 rw [List.map_map, ← List.ofFn_eq_map]

486 rw [List.ofFn_congr hτNum]

487 rw [← List.ofFn_eq_map]

488 rw [List.ofFn_congr hσNum]

489 have hSourceList :

490 List.ofFn

491 (fun i : Fin (k + (n + 2)) =>

492 θ (xWord τ (Fin.cast hτNum.symm i))) =

493 List.ofFn

494 (fun j : Fin k =>

495 θ (xWord τ (Fin.cast hτNum.symm (Fin.castAdd (n + 2) j)))) ++

496 List.ofFn

497 (fun j : Fin (n + 2) =>

498 θ (xWord τ (Fin.cast hτNum.symm (Fin.natAdd k j)))) := by

499 rw [← List.ofFn_fin_append]

500 congr

501 funext i

502 cases i using Fin.addCases <;> simp only [Fin.append_left, Fin.append_right]

503 have hTargetList :

504 List.ofFn

505 (fun i : Fin (k + (n + 2)) =>

506 xWord σ (Fin.cast hσNum.symm i)) =

507 List.ofFn

508 (fun j : Fin k =>

509 xWord σ (Fin.cast hσNum.symm (Fin.castAdd (n + 2) j))) ++

510 List.ofFn

511 (fun j : Fin (n + 2) =>

512 xWord σ (Fin.cast hσNum.symm (Fin.natAdd k j))) := by

513 rw [← List.ofFn_fin_append]

514 congr

515 funext i

516 cases i using Fin.addCases <;> simp only [Fin.append_left, Fin.append_right]

517 simp only [Function.comp_apply]

518 rw [hSourceList, hTargetList]

519 rw [List.ofFn_succ]

520 rw [List.ofFn_succ]

521 simp only [xWord, Fin.cast_cast, FreeGroup.lift_apply_of, Fin.cast_inj, hprefix_ne_zero, ↓reduceIte,

522 hprefix_ne_one, Fin.succ_zero_eq_one, Fin.natAdd_inj, one_ne_zero, Fin.succ_ne_zero, htail_ne_one, List.prod_append,

523 List.prod_cons, List.map_nil, List.prod_nil, map_one, mul_one, List.ofFn_succ, mul_right_inj, θ, τ0, σ0, σ1, τ1,

524 sameσ]

525 group

526 · intro i

527 have hEq : θ (η (xWord σ i)) = xWord σ i := by

528 rcases fin_eq_prefix_or_zero_or_one_or_tail_of_eq_add_two hσNum i with

529 ⟨j, rfl⟩ | rfl | rfl | ⟨t, rfl⟩

530 · simp only [xWord, Fin.cast_cast, FreeGroup.lift_apply_of, Fin.cast_inj, hprefix_ne_zero j, ↓reduceIte,

531 hprefix_ne_one j, θ, τ0, σ0, σ1, τ1, sameσ, η, sameτ]

532 · simp only [xWord, FreeGroup.lift_apply_of, ↓reduceIte, hτ10, θ, σ0, σ1, η]

533 · simp only [xWord, FreeGroup.lift_apply_of, hσ10, ↓reduceIte, map_mul, map_inv, hτ10, θ, σ0, σ1, η]

534 group

535 · simp only [xWord, Fin.cast_cast, FreeGroup.lift_apply_of, Fin.cast_inj, Fin.natAdd_inj, htail_ne_zero t,

536 ↓reduceIte, htail_ne_one t, θ, τ0, σ0, σ1, τ1, sameσ, η, sameτ]

537 rw [hEq]

538 simp only [mul_inv_cancel, one_mem]

539 · intro i

540 have hEq : η (θ (xWord τ i)) = xWord τ i := by

541 rcases fin_eq_prefix_or_zero_or_one_or_tail_of_eq_add_two hτNum i with

542 ⟨j, rfl⟩ | rfl | rfl | ⟨t, rfl⟩

543 · simp only [xWord, Fin.cast_cast, FreeGroup.lift_apply_of, Fin.cast_inj, hprefix_ne_zero j, ↓reduceIte,

544 hprefix_ne_one j, η, σ0, τ1, σ1, τ0, sameτ, θ, sameσ]

545 · simp only [xWord, FreeGroup.lift_apply_of, ↓reduceIte, map_mul, hσ10, map_inv, η, τ1, τ0, θ]

546 group

547 · simp only [xWord, FreeGroup.lift_apply_of, hτ10, ↓reduceIte, η, τ1, τ0, θ]

548 · simp only [xWord, Fin.cast_cast, FreeGroup.lift_apply_of, Fin.cast_inj, Fin.natAdd_inj, htail_ne_zero t,

549 ↓reduceIte, htail_ne_one t, η, σ0, τ1, σ1, τ0, sameτ, θ, sameσ]

550 rw [hEq]

551 simp only [mul_inv_cancel, one_mem]

552private theorem zeroGenusFuchsianPresentedGroupEquivOfIndexedPeriods_of_adjacentSwap

553 (σ τ : FuchsianSignature)

554 (hσZero : σ.orbitGenus = 0) (hτZero : τ.orbitGenus = 0)

555 {ι : Type*}

556 (eσ : ι ≃ Fin σ.numPeriods) (eτ : ι ≃ Fin τ.numPeriods)

557 {k n : ℕ}

558 (hσNum : σ.numPeriods = k + (n + 2)) (hτNum : τ.numPeriods = k + (n + 2))

559 (hAdjacent :

560 let σ0 : Fin σ.numPeriods := Fin.cast hσNum.symm (Fin.natAdd k (0 : Fin (n + 2)))

561 let σ1 : Fin σ.numPeriods := Fin.cast hσNum.symm (Fin.natAdd k (1 : Fin (n + 2)))

562 let τ0 : Fin τ.numPeriods := Fin.cast hτNum.symm (Fin.natAdd k (0 : Fin (n + 2)))

563 let τ1 : Fin τ.numPeriods := Fin.cast hτNum.symm (Fin.natAdd k (1 : Fin (n + 2)))

564 let sameτ : Fin σ.numPeriods → Fin τ.numPeriods := fun i =>

565 Fin.cast hτNum.symm (Fin.cast hσNum i)

566 ∀ x, eτ x = if eσ x = σ0 then τ1 else if eσ x = σ1 then τ0 else sameτ (eσ x))

567 (hPeriods : ∀ x, σ.periods (eσ x) = τ.periods (eτ x)) :

568 Nonempty (FuchsianPresentedGroup σ ≃* FuchsianPresentedGroup τ) := by

569 let σ0 : Fin σ.numPeriods := Fin.cast hσNum.symm (Fin.natAdd k (0 : Fin (n + 2)))

570 let σ1 : Fin σ.numPeriods := Fin.cast hσNum.symm (Fin.natAdd k (1 : Fin (n + 2)))

571 let τ0 : Fin τ.numPeriods := Fin.cast hτNum.symm (Fin.natAdd k (0 : Fin (n + 2)))

572 let τ1 : Fin τ.numPeriods := Fin.cast hτNum.symm (Fin.natAdd k (1 : Fin (n + 2)))

573 let sameτ : Fin σ.numPeriods → Fin τ.numPeriods := fun i =>

574 Fin.cast hτNum.symm (Fin.cast hσNum i)

575 refine zeroGenusAdjacentSwapFuchsianPresentedGroupEquiv

576 (k := k) (n := n) σ τ hσZero hτZero hσNum hτNum ?_ ?_ ?_ ?_

577 · intro j

578 let σj : Fin σ.numPeriods := Fin.cast hσNum.symm (Fin.castAdd (n + 2) j)

579 let τj : Fin τ.numPeriods := Fin.cast hτNum.symm (Fin.castAdd (n + 2) j)

580 let x : ι := eσ.symm σj

581 have hxσ : eσ x = σj := by simp only [Equiv.apply_symm_apply, x]

582 have hprefix_ne_zero :

583 (Fin.castAdd (n + 2) j : Fin (k + (n + 2))) ≠

584 Fin.natAdd k (0 : Fin (n + 2)) := by

585 intro h

586 have := congrArg Fin.val h

587 simp only [Fin.val_castAdd, Fin.val_natAdd, Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero] at this

588 omega

589 have hprefix_ne_one :

590 (Fin.castAdd (n + 2) j : Fin (k + (n + 2))) ≠

591 Fin.natAdd k (1 : Fin (n + 2)) := by

592 intro h

593 have := congrArg Fin.val h

594 simp only [Fin.val_castAdd, Fin.val_natAdd, Fin.coe_ofNat_eq_mod, Nat.one_mod] at this

595 omega

596 have hxτ : eτ x = τj := by

597 simpa [σ0, σ1, τ0, τ1, sameτ, σj, τj, hxσ, hprefix_ne_zero,

598 hprefix_ne_one] using hAdjacent x

599 calc

600 σ.periods (Fin.cast hσNum.symm (Fin.castAdd (n + 2) j)) =

601 σ.periods (eσ x) := by

602 rw [hxσ]

603 _ = τ.periods (eτ x) := hPeriods x

604 _ = τ.periods (Fin.cast hτNum.symm (Fin.castAdd (n + 2) j)) := by

605 rw [hxτ]

606 · let x : ι := eσ.symm σ0

607 have hxσ : eσ x = σ0 := by simp only [Equiv.apply_symm_apply, x]

608 have hxτ : eτ x = τ1 := by

609 simpa [σ0, σ1, τ0, τ1, sameτ, hxσ] using hAdjacent x

610 calc

611 σ.periods (Fin.cast hσNum.symm (Fin.natAdd k (0 : Fin (n + 2)))) =

612 σ.periods (eσ x) := by

613 rw [hxσ]

614 _ = τ.periods (eτ x) := hPeriods x

615 _ = τ.periods (Fin.cast hτNum.symm (Fin.natAdd k (1 : Fin (n + 2)))) := by

616 rw [hxτ]

617 · let x : ι := eσ.symm σ1

618 have hxσ : eσ x = σ1 := by simp only [Equiv.apply_symm_apply, x]

619 have hσ10 : σ1 ≠ σ0 := by

620 intro h

621 have := congrArg (fun i : Fin σ.numPeriods => (Fin.cast hσNum i).val) h

622 simp only [Fin.cast_cast, Fin.cast_eq_self, Fin.val_natAdd, Fin.coe_ofNat_eq_mod, Nat.one_mod, Nat.zero_mod,

623 add_zero, Nat.add_eq_left, one_ne_zero, σ1, σ0] at this

624 have hxτ : eτ x = τ0 := by

625 simpa [σ0, σ1, τ0, τ1, sameτ, hxσ, hσ10] using hAdjacent x

626 calc

627 σ.periods (Fin.cast hσNum.symm (Fin.natAdd k (1 : Fin (n + 2)))) =

628 σ.periods (eσ x) := by

629 rw [hxσ]

630 _ = τ.periods (eτ x) := hPeriods x

631 _ = τ.periods (Fin.cast hτNum.symm (Fin.natAdd k (0 : Fin (n + 2)))) := by

632 rw [hxτ]

633 · intro t

634 let σt : Fin σ.numPeriods := Fin.cast hσNum.symm (Fin.natAdd k t.succ.succ)

635 let x : ι := eσ.symm σt

636 have hxσ : eσ x = σt := by simp only [Equiv.apply_symm_apply, x]

637 have htail_ne_zero : (t.succ.succ : Fin (n + 2)) ≠ 0 := by

638 intro h

639 have := congrArg Fin.val h

640 simp only [Fin.val_succ, Fin.coe_ofNat_eq_mod, Nat.zero_mod, Nat.add_eq_zero_iff, one_ne_zero, and_false,

641 and_self] at this

642 have htail_ne_one : (t.succ.succ : Fin (n + 2)) ≠ 1 := by

643 intro h

644 have := congrArg Fin.val h

645 simp only [Fin.val_succ, Fin.coe_ofNat_eq_mod, Nat.one_mod, Nat.add_eq_right, Nat.add_eq_zero_iff,

646 one_ne_zero, and_false] at this

647 have hxτ : eτ x = Fin.cast hτNum.symm (Fin.natAdd k t.succ.succ) := by

648 simpa [σ0, σ1, τ0, τ1, sameτ, σt, hxσ, htail_ne_zero, htail_ne_one] using

649 hAdjacent x

650 calc

651 σ.periods (Fin.cast hσNum.symm (Fin.natAdd k t.succ.succ)) =

652 σ.periods (eσ x) := by

653 rw [hxσ]

654 _ = τ.periods (eτ x) := hPeriods x

655 _ = τ.periods (Fin.cast hτNum.symm (Fin.natAdd k t.succ.succ)) := by

656 rw [hxτ]

657noncomputable def zeroGenusPermutedSignature

658 (σ : FuchsianSignature) {m : ℕ} (hNum : σ.numPeriods = m)

659 (p : Equiv.Perm (Fin m)) : FuchsianSignature where

660 orbitGenus := 0

661 numCusps := 0

662 numPeriods := m

663 periods := fun i => σ.periods (Fin.cast hNum.symm (p i))

664 period_ge_two := by

665 intro i

666 exact σ.period_ge_two _

667 numCusps_eq_zero := rfl

668 numPeriods_ge_three := by

669 have hge := σ.numPeriods_ge_three

670 omega

671@[local simp]

672theorem zeroGenusPermutedSignature_orbitGenus

673 (σ : FuchsianSignature) {m : ℕ} (hNum : σ.numPeriods = m)

674 (p : Equiv.Perm (Fin m)) :

675 (zeroGenusPermutedSignature σ hNum p).orbitGenus = 0 := rfl

676@[local simp]

677theorem zeroGenusPermutedSignature_numPeriods

678 (σ : FuchsianSignature) {m : ℕ} (hNum : σ.numPeriods = m)

679 (p : Equiv.Perm (Fin m)) :

680 (zeroGenusPermutedSignature σ hNum p).numPeriods = m := rfl

681@[local simp]

682theorem zeroGenusPermutedSignature_periods

683 (σ : FuchsianSignature) {m : ℕ} (hNum : σ.numPeriods = m)

684 (p : Equiv.Perm (Fin m)) (i : Fin m) :

685 (zeroGenusPermutedSignature σ hNum p).periods i =

686 σ.periods (Fin.cast hNum.symm (p i)) := rfl

687private theorem zeroGenusFuchsianPresentedGroupEquivOfPermutedSignature

688 (σ : FuchsianSignature) (hσZero : σ.orbitGenus = 0)

689 {r : ℕ} (hNum : σ.numPeriods = r + 1)

690 (p : Equiv.Perm (Fin (r + 1))) :

691 Nonempty

692 (FuchsianPresentedGroup σ ≃*

693 FuchsianPresentedGroup (zeroGenusPermutedSignature σ hNum p)) := by

694 classical

695 let S : Equiv.Perm (Fin (r + 1)) → FuchsianSignature :=

696 fun p => zeroGenusPermutedSignature σ hNum p

697 let adjacentSet : Set (Equiv.Perm (Fin (r + 1))) :=

698 Set.range fun i : Fin r => Equiv.swap i.castSucc i.succ

699 have htop : Submonoid.closure adjacentSet = ⊤ := by

700 simpa [adjacentSet] using Equiv.Perm.mclosure_swap_castSucc_succ r

701 refine Submonoid.induction_of_closure_eq_top_right

702 (s := adjacentSet) htop p ?_ ?_

703 · refine zeroGenusFuchsianPresentedGroupEquivOfOrderedPeriods

704 σ (S 1) hσZero rfl hNum ?_

705 intro i

706 simp only [zeroGenusPermutedSignature_numPeriods, zeroGenusPermutedSignature_periods, Equiv.Perm.coe_one,

707 id_eq, Fin.cast_cast, Fin.cast_eq_self, S]

708 · intro p s hs ih

709 rcases hs with ⟨i, rfl⟩

710 let sw : Equiv.Perm (Fin (r + 1)) := Equiv.swap i.castSucc i.succ

711 let k : ℕ := i.val

712 let nTail : ℕ := r - i.val - 1

713 have hAdjNum : r + 1 = k + (nTail + 2) := by

714 dsimp [k, nTail]

715 omega

716 have hpos0 :

717 Fin.cast hAdjNum.symm (Fin.natAdd k (0 : Fin (nTail + 2))) =

718 i.castSucc := by

719 ext

720 simp only [Fin.val_cast, Fin.val_natAdd, Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero, Fin.val_castSucc, k,

721 nTail]

722 have hpos1 :

723 Fin.cast hAdjNum.symm (Fin.natAdd k (1 : Fin (nTail + 2))) =

724 i.succ := by

725 ext

726 simp only [Fin.val_cast, Fin.val_natAdd, Fin.coe_ofNat_eq_mod, Nat.one_mod, Fin.val_succ,

727 k, nTail]

728 have hswap_apply :

729 ∀ x : Fin (r + 1),

730 sw x = if x = i.castSucc then i.succ else if x = i.succ then i.castSucc else x := by

731 intro x

732 by_cases hx0 : x = i.castSucc

733 · subst x

734 simp only [Equiv.swap_apply_left, ↓reduceIte, sw]

735 · by_cases hx1 : x = i.succ

736 · subst x

737 simp only [Equiv.swap_apply_right, hx0, ↓reduceIte, sw]

738 · simpa [sw, hx0, hx1] using Equiv.swap_apply_of_ne_of_ne hx0 hx1

739 have hstep :

740 Nonempty (FuchsianPresentedGroup (S p) ≃* FuchsianPresentedGroup (S (p * sw))) := by

741 refine zeroGenusFuchsianPresentedGroupEquivOfIndexedPeriods_of_adjacentSwap

742 (S p) (S (p * sw)) rfl rfl

743 (Equiv.refl (Fin (r + 1))) sw hAdjNum hAdjNum ?_ ?_

744 · dsimp

745 intro x

746 rw [hpos0, hpos1]

747 exact hswap_apply x

748 · intro x

749 simp only [zeroGenusPermutedSignature_numPeriods, Equiv.refl_apply, zeroGenusPermutedSignature_periods,

750 Equiv.Perm.coe_mul, Function.comp_apply, Equiv.swap_apply_self, S, sw]

751 rcases ih with ⟨e₁⟩

752 rcases hstep with ⟨e₂⟩

753 exact ⟨e₁.trans e₂⟩

754theorem zeroGenusFuchsianPresentedGroupEquivOfIndexedPeriods

755 (σ τ : FuchsianSignature)

756 (hσZero : σ.orbitGenus = 0) (hτZero : τ.orbitGenus = 0)

757 {ι : Type*}

758 (eσ : ι ≃ Fin σ.numPeriods) (eτ : ι ≃ Fin τ.numPeriods)

759 (hPeriods : ∀ x, σ.periods (eσ x) = τ.periods (eτ x)) :

760 Nonempty (FuchsianPresentedGroup σ ≃* FuchsianPresentedGroup τ) := by

761 classical

762 letI : Fintype ι := Fintype.ofEquiv (Fin σ.numPeriods) eσ.symm

763 have hσCard : Fintype.card ι = σ.numPeriods := by

764 simpa using Fintype.card_congr eσ

765 have hτCard : Fintype.card ι = τ.numPeriods := by

766 simpa using Fintype.card_congr eτ

767 have hNum : σ.numPeriods = τ.numPeriods := hσCard.symm.trans hτCard

768 let r : ℕ := σ.numPeriods - 1

769 have hσLen : σ.numPeriods = r + 1 := by

770 dsimp [r]

771 have hge := σ.numPeriods_ge_three

772 omega

773 have hτLen : τ.numPeriods = r + 1 := by

774 omega

775 let p : Equiv.Perm (Fin (r + 1)) :=

776 (finCongr hτLen.symm).trans (eτ.symm.trans (eσ.trans (finCongr hσLen)))

777 rcases zeroGenusFuchsianPresentedGroupEquivOfPermutedSignature σ hσZero hσLen p with ⟨e₁⟩

778 have hρτ :

779 Nonempty

780 (FuchsianPresentedGroup (zeroGenusPermutedSignature σ hσLen p) ≃*

781 FuchsianPresentedGroup τ) := by

782 refine zeroGenusFuchsianPresentedGroupEquivOfOrderedPeriods

783 (zeroGenusPermutedSignature σ hσLen p) τ rfl hτZero hτLen.symm ?_

784 intro j

785 let t : Fin τ.numPeriods := Fin.cast hτLen.symm j

786 let x : ι := eτ.symm t

787 have hxτ : eτ x = t := by

788 simp only [Equiv.apply_symm_apply, x]

789 calc

790 (zeroGenusPermutedSignature σ hσLen p).periods j = σ.periods (eσ x) := by

791 simp only [zeroGenusPermutedSignature, Equiv.trans_apply, finCongr_apply, Fin.cast_cast, Fin.cast_eq_self, p,

792 x, t]

793 _ = τ.periods (eτ x) := hPeriods x

794 _ = τ.periods (Fin.cast hτLen.symm j) := by

795 rw [hxτ]

796 rcases hρτ with ⟨e₂⟩

797 exact ⟨e₁.trans e₂⟩

798theorem firstReductionSourceMulEquiv_exists

799 {σ : FuchsianSignature} (D : FirstReductionPeriodData σ)

800 (hZero : σ.orbitGenus = 0) :

801 Nonempty (FuchsianPresentedGroup σ ≃* FuchsianPresentedGroup D.sourceSignature) := by

802 refine

803 zeroGenusFuchsianPresentedGroupEquivOfIndexedPeriods σ D.sourceSignature

804 hZero ?_ D.reindex (originalFirstReductionOrderedIndexEquiv D.tailLen) ?_

805 · simp only [FirstReductionPeriodData.sourceSignature, originalFirstReductionSignature]

806 · intro x

807 rw [← D.periods_eq x]

808 cases x using Sum.casesOn with

809 | inl i =>

810 fin_cases i <;>

811 simp only [originalFirstReductionPeriods, twoPeriods, Nat.reduceAdd, Fin.mk_zero, Fin.mk_one, Fin.isValue,

812 fin_cases_const_one, FirstReductionPeriodData.sourceSignature, originalFirstReductionSignature,

813 originalFirstReductionOrderedIndexEquiv, Fin.val_eq_zero_iff, Equiv.coe_fn_mk, Fin.coe_ofNat_eq_mod, Nat.mod_succ,

814 originalFirstReductionSignaturePeriod, one_ne_zero, ↓reduceDIte, Fin.cases_zero]

815 | inr j =>

816 simp only [originalFirstReductionPeriods, FirstReductionPeriodData.sourceSignature,

817 originalFirstReductionSignature, originalFirstReductionOrderedIndexEquiv, Fin.val_eq_zero_iff, Fin.isValue,

818 Equiv.coe_fn_mk, originalFirstReductionSignaturePeriod, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and,

819 ↓reduceDIte, add_tsub_cancel_left, Fin.eta, dite_eq_ite, right_eq_ite_iff]

820 omega

821

822end FenchelNielsen