FenchelNielsenZomorrodian/Profinite/PositiveGenusQuotient.lean

1import FenchelNielsenZomorrodian.Discrete.Coordinates.FenchelPeriodCoordinate

2import FenchelNielsenZomorrodian.Discrete.GroupTheory.DerivedSeries

3import FenchelNielsenZomorrodian.Profinite.SmoothQuotient

4import Mathlib.GroupTheory.SemidirectProduct

6/-

7PUBLIC_PAGE_SNAPSHOT

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

9lean_source: lean4/FenchelNielsenZomorrodian/Profinite/PositiveGenusQuotient.lean

10translation_root: data/translation

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

12placement: after imports, never before imports

13-/

14/-!

15# Positive-genus smooth quotients

17Builds finite quotients of derived length at most two in positive genus by assigning surface and inertia generators to a finite solvable target.

18-/

20namespace FenchelNielsen

22universe u

24namespace ProfiniteFGroup

26abbrev PositiveGenusSmoothBase (σ : FenchelSignature) :=

27 Multiplicative (FenchelPeriodCoordinate σ × FenchelPeriodCoordinate σ)

29noncomputable def positiveGenusSmoothSwap

30 (σ : FenchelSignature) :

31 MulAut (PositiveGenusSmoothBase σ) where

32 toFun x :=

33 Multiplicative.ofAdd

34 ((Multiplicative.toAdd x).2, (Multiplicative.toAdd x).1)

35 invFun x :=

36 Multiplicative.ofAdd

37 ((Multiplicative.toAdd x).2, (Multiplicative.toAdd x).1)

38 left_inv := by

39 intro x

40 cases x

41 rfl

42 right_inv := by

43 intro x

44 cases x

45 rfl

46 map_mul' := by

47 intro x y

48 cases x

49 cases y

50 rfl

52theorem zmod_two_eq_zero_or_one (z : ZMod 2) :

53 z = 0 ∨ z = 1 := by

54 have hzlt : z.val < 2 := ZMod.val_lt z

55 have hval : z.val = 0 ∨ z.val = 1 := by omega

56 rcases hval with h | h

57 · left

58 rw [← ZMod.natCast_zmod_val z, h]

59 norm_num

60 · right

61 rw [← ZMod.natCast_zmod_val z, h]

62 norm_num

64noncomputable def positiveGenusSmoothAction

65 (σ : FenchelSignature) :

66 Multiplicative (ZMod 2) →* MulAut (PositiveGenusSmoothBase σ) where

67 toFun t :=

68 if Multiplicative.toAdd t = (0 : ZMod 2) then

69 1

70 else

71 positiveGenusSmoothSwap σ

72 map_one' := by simp only [toAdd_one, ↓reduceIte]

73 map_mul' := by

74 intro a b

75 have ha := zmod_two_eq_zero_or_one (Multiplicative.toAdd a)

76 have hb := zmod_two_eq_zero_or_one (Multiplicative.toAdd b)

77 rcases ha with ha | ha <;> rcases hb with hb | hb

78 · ext x : 1

79 cases x

80 simp only [toAdd_mul, ha, hb, add_zero, ↓reduceIte, MulAut.one_apply, mul_one]

81 · ext x : 1

82 cases x

83 simp only [toAdd_mul, ha, hb, zero_add, one_ne_zero, ↓reduceIte, positiveGenusSmoothSwap, MulEquiv.coe_mk,

84 Equiv.coe_fn_mk, one_mul]

85 · ext x : 1

86 cases x

87 simp only [toAdd_mul, ha, hb, add_zero, one_ne_zero, ↓reduceIte, positiveGenusSmoothSwap, MulEquiv.coe_mk,

88 Equiv.coe_fn_mk, mul_one]

89 · have hsum : (1 : ZMod 2) + 1 = 0 := by

90 simpa using (ZMod.natCast_self 2)

91 ext x : 1

92 cases x

93 simp only [toAdd_mul, ha, hb, hsum, ↓reduceIte, MulAut.one_apply, one_ne_zero, positiveGenusSmoothSwap,

94 MulAut.mul_apply, MulEquiv.coe_mk, Equiv.coe_fn_mk, toAdd_ofAdd, Prod.mk.eta, ofAdd_toAdd]

96abbrev PositiveGenusSmoothQuotient (σ : FenchelSignature) :=

97 PositiveGenusSmoothBase σ ⋊[positiveGenusSmoothAction σ]

98 Multiplicative (ZMod 2)

100instance instTopologicalSpacePositiveGenusSmoothQuotient (σ : FenchelSignature) :

101 TopologicalSpace (PositiveGenusSmoothQuotient σ) :=

102 ⊥

103

104instance instDiscreteTopologyPositiveGenusSmoothQuotient (σ : FenchelSignature) :

105 DiscreteTopology (PositiveGenusSmoothQuotient σ) :=

106 ⟨rfl⟩

107

108/-- The base-coordinate value assigned to a positive-genus inertia generator. -/

109def positiveGenusSmoothEllipticBase

110 (σ : FenchelSignature) (i : Fin σ.numPeriods) :

111 PositiveGenusSmoothBase σ :=

112 Multiplicative.ofAdd

113 (fenchelPeriodBasisVector σ i, -fenchelPeriodBasisVector σ i)

114

115/-- The sum of the period-coordinate basis vectors. -/

116def positiveGenusSmoothSumBasis

117 (σ : FenchelSignature) :

118 FenchelPeriodCoordinate σ :=

119 ∑ i : Fin σ.numPeriods, fenchelPeriodBasisVector σ i

120

121/-- The product of the base-coordinate values assigned to all inertia generators. -/

122def positiveGenusSmoothEllipticProductBase

123 (σ : FenchelSignature) :

124 PositiveGenusSmoothBase σ :=

125 Multiplicative.ofAdd

126 (positiveGenusSmoothSumBasis σ,

127 -positiveGenusSmoothSumBasis σ)

128

129/-- The base-coordinate value used for the first positive-genus surface generator. -/

130def positiveGenusSmoothSurfaceBase

131 (σ : FenchelSignature) :

132 PositiveGenusSmoothBase σ :=

133 Multiplicative.ofAdd (0, positiveGenusSmoothSumBasis σ)

134

135/-- The nontrivial top-coordinate generator of the positive-genus quotient. -/

136def positiveGenusSmoothTopGenerator :

137 Multiplicative (ZMod 2) :=

138 Multiplicative.ofAdd (1 : ZMod 2)

139

140/-- Each positive-genus inertia base value has exponent dividing its period. -/

141theorem positiveGenusSmoothEllipticBase_pow_period

142 (σ : FenchelSignature) (i : Fin σ.numPeriods) :

143 positiveGenusSmoothEllipticBase σ i ^ σ.periods i = 1 := by

144 rw [positiveGenusSmoothEllipticBase, ← ofAdd_nsmul]

145 apply congrArg Multiplicative.ofAdd

146 ext j

147 · by_cases hji : j = i

148 · subst hji

149 simp only [fenchelPeriodBasisVector, zmodBasisVector, Prod.smul_mk, nsmul_eq_mul, smul_neg, Pi.mul_apply,

150 Pi.natCast_apply, CharP.cast_eq_zero, Pi.single_eq_same, mul_one, Prod.fst_zero, Pi.zero_apply]

151 · simp only [fenchelPeriodBasisVector, zmodBasisVector, Prod.smul_mk, nsmul_eq_mul, smul_neg, Pi.mul_apply,

152 Pi.natCast_apply, ne_eq, hji, not_false_eq_true, Pi.single_eq_of_ne, mul_zero, Prod.fst_zero, Pi.zero_apply]

153 · by_cases hji : j = i

154 · subst hji

155 simp only [fenchelPeriodBasisVector, zmodBasisVector, Prod.smul_mk, nsmul_eq_mul, smul_neg, Pi.neg_apply,

156 Pi.mul_apply, Pi.natCast_apply, CharP.cast_eq_zero, Pi.single_eq_same, mul_one, neg_zero, Prod.snd_zero,

157 Pi.zero_apply]

158 · simp only [fenchelPeriodBasisVector, zmodBasisVector, Prod.smul_mk, nsmul_eq_mul, smul_neg, Pi.neg_apply,

159 Pi.mul_apply, Pi.natCast_apply, ne_eq, hji, not_false_eq_true, Pi.single_eq_of_ne, mul_zero, neg_zero,

160 Prod.snd_zero, Pi.zero_apply]

161

162/-- The named elliptic product base is the product of the individual inertia base values. -/

163theorem positiveGenusSmoothEllipticProductBase_eq_prod

164 (σ : FenchelSignature) :

165 (∏ i : Fin σ.numPeriods, positiveGenusSmoothEllipticBase σ i) =

166 positiveGenusSmoothEllipticProductBase σ := by

167 calc

168 (∏ i : Fin σ.numPeriods, positiveGenusSmoothEllipticBase σ i)

169 =

170 Multiplicative.ofAdd

171 (∑ i : Fin σ.numPeriods,

172 (fenchelPeriodBasisVector σ i, -fenchelPeriodBasisVector σ i)) := by

173 simp only [positiveGenusSmoothEllipticBase, ofAdd_sum]

174 _ = positiveGenusSmoothEllipticProductBase σ := by

175 apply Multiplicative.ofAdd.injective

176 ext j <;>

177 simp only [ofAdd_sum, toAdd_ofAdd, toAdd_prod, Prod.fst_sum, Prod.snd_sum,

178 Finset.sum_apply, Pi.neg_apply, Finset.sum_neg_distrib,

179 positiveGenusSmoothEllipticProductBase, positiveGenusSmoothSumBasis]

180

181private theorem list_finRange_prod_eq_single_zeroVal

182 {G : Type*} [Monoid G] {n : ℕ} (h : 1 ≤ n) (c : G) :

183 ((List.finRange n).map

184 (fun j : Fin n => if j.val = 0 then c else 1)).prod = c := by

185 cases hn : n with

186 | zero => omega

187 | succ k =>

188 rw [List.finRange_succ]

189 simp only [List.map_cons, List.prod_cons]

190 simp only [Fin.val_zero, ↓reduceIte]

191 have htail' :

192 (List.map

193 (fun j : Fin (k + 1) => if j.val = 0 then c else 1)

194 (List.map Fin.succ (List.finRange k))).prod = 1 := by

195 simp only [Fin.val_eq_zero_iff, List.map_map, Function.comp_def, Fin.succ_ne_zero, ↓reduceIte,

196 List.map_const', List.length_finRange, List.prod_replicate, one_pow]

197 rw [htail', mul_one]

198

199/-- The elliptic product cancels the chosen surface commutator in the positive-genus quotient. -/

200theorem positiveGenusSmoothEllipticProduct_mul_surfaceCommutator

201 (σ : FenchelSignature) :

202 (SemidirectProduct.inl (positiveGenusSmoothEllipticProductBase σ) :

203 PositiveGenusSmoothQuotient σ) *

204 ⁅(SemidirectProduct.inl (positiveGenusSmoothSurfaceBase σ) :

205 PositiveGenusSmoothQuotient σ),

206 SemidirectProduct.inr positiveGenusSmoothTopGenerator⁆ =

207 1 := by

208 ext <;>

209 simp only [positiveGenusSmoothAction, toAdd_eq_zero, positiveGenusSmoothSwap,

210 positiveGenusSmoothEllipticProductBase, positiveGenusSmoothSumBasis,

211 positiveGenusSmoothSurfaceBase, positiveGenusSmoothTopGenerator, commutatorElement_def,

212 SemidirectProduct.mul_left, SemidirectProduct.mul_right, SemidirectProduct.left_inl,

213 SemidirectProduct.left_inr, SemidirectProduct.right_inl, SemidirectProduct.right_inr,

214 one_mul, SemidirectProduct.inv_left, SemidirectProduct.inv_right, inv_one, mul_one,

215 mul_inv_cancel, toAdd_one, SemidirectProduct.one_left, SemidirectProduct.one_right,

216 ofAdd_eq_one, inv_eq_one, one_ne_zero, ↓reduceIte, MulAut.one_apply, MulEquiv.coe_mk,

217 Equiv.coe_fn_mk, MonoidHom.coe_mk, OneHom.coe_mk, toAdd_mul, toAdd_inv, toAdd_ofAdd,

218 Prod.fst_add, Prod.snd_add, Prod.fst_neg, Prod.snd_neg, Prod.fst_zero, Prod.snd_zero,

219 Pi.add_apply, Pi.neg_apply, Pi.zero_apply, Finset.sum_apply, neg_zero, add_assoc,

220 neg_add_cancel, add_neg_cancel, zero_add, add_zero]

221

222noncomputable def positiveGenusGeneratorImageCore

223 (Δ : ProfiniteFGroup.{u}) :

224 ProfiniteFenchelGeneratorIndex.{u} Δ.signature →

225 PositiveGenusSmoothQuotient Δ.signature

226 | ULift.up (.inertia i) =>

227 SemidirectProduct.inl

228 (positiveGenusSmoothEllipticBase Δ.signature i)

229 | ULift.up (.surfaceA j) =>

230 if j.val = 0 then

231 SemidirectProduct.inl

232 (positiveGenusSmoothSurfaceBase Δ.signature)

233 else

234 1

235 | ULift.up (.surfaceB j) =>

236 if j.val = 0 then

237 SemidirectProduct.inr positiveGenusSmoothTopGenerator

238 else

239 1

240 | ULift.up (.cusp _) => 1

241

242noncomputable def positiveGenusGeneratorImage

243 (Δ : ProfiniteFGroup.{u}) :

244 ProfiniteFenchelGeneratorIndex.{u} Δ.signature →

245 ULift.{u, 0} (PositiveGenusSmoothQuotient Δ.signature) :=

246 fun x => ULift.up (positiveGenusGeneratorImageCore Δ x)

247

248private theorem positiveGenus_inertia_list_product

249 (σ : FenchelSignature) :

250 ((List.finRange σ.numPeriods).map fun i =>

251 (SemidirectProduct.inl (positiveGenusSmoothEllipticBase σ i) :

252 PositiveGenusSmoothQuotient σ)).prod =

253 (SemidirectProduct.inl

254 (positiveGenusSmoothEllipticProductBase σ) :

255 PositiveGenusSmoothQuotient σ) := by

256 calc

257 (List.map

258 (fun i : Fin σ.numPeriods =>

259 (SemidirectProduct.inl (positiveGenusSmoothEllipticBase σ i) :

260 PositiveGenusSmoothQuotient σ))

261 (List.finRange σ.numPeriods)).prod

262 =

263 SemidirectProduct.inl

264 ((List.map

265 (fun i : Fin σ.numPeriods =>

266 positiveGenusSmoothEllipticBase σ i)

267 (List.finRange σ.numPeriods)).prod) := by

268 simpa [List.map_map] using

269 (map_list_prod

270 (SemidirectProduct.inl :

271 PositiveGenusSmoothBase σ →*

272 PositiveGenusSmoothQuotient σ)

273 (List.map

274 (fun i : Fin σ.numPeriods =>

275 positiveGenusSmoothEllipticBase σ i)

276 (List.finRange σ.numPeriods))).symm

277 _ =

278 SemidirectProduct.inl

279 (∏ i : Fin σ.numPeriods,

280 positiveGenusSmoothEllipticBase σ i) := by

281 exact congrArg SemidirectProduct.inl

282 ((Fin.prod_univ_def

283 (f := fun i : Fin σ.numPeriods =>

284 positiveGenusSmoothEllipticBase σ i)).symm)

285 _ =

286 SemidirectProduct.inl

287 (positiveGenusSmoothEllipticProductBase σ) := by

288 rw [positiveGenusSmoothEllipticProductBase_eq_prod]

289

290private theorem positiveGenusGeneratorImage_total_relation

291 (Δ : ProfiniteFGroup.{u}) (hGenus : 1 ≤ Δ.signature.orbitGenus) :

292 profiniteFenchelTotalRelation

293 (fun i => positiveGenusGeneratorImageCore Δ

294 (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))

295 (fun i => positiveGenusGeneratorImageCore Δ

296 (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))

297 (fun j => positiveGenusGeneratorImageCore Δ

298 (ULift.up (ProfiniteFenchelGenerator.cusp j)))

299 (fun k => positiveGenusGeneratorImageCore Δ

300 (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1 := by

301 let e : PositiveGenusSmoothQuotient Δ.signature :=

302 ((List.finRange Δ.signature.numPeriods).map fun i =>

303 positiveGenusGeneratorImageCore Δ

304 (ULift.up (ProfiniteFenchelGenerator.inertia i))).prod

305 let c : PositiveGenusSmoothQuotient Δ.signature :=

306 ((List.finRange Δ.signature.orbitGenus).map fun j =>

307 ⁅positiveGenusGeneratorImageCore Δ

308 (ULift.up (ProfiniteFenchelGenerator.surfaceA j)),

309 positiveGenusGeneratorImageCore Δ

310 (ULift.up (ProfiniteFenchelGenerator.surfaceB j))⁆).prod

311 have he :

312 e =

313 (SemidirectProduct.inl

314 (positiveGenusSmoothEllipticProductBase Δ.signature) :

315 PositiveGenusSmoothQuotient Δ.signature) := by

316 simpa [e, positiveGenusGeneratorImageCore] using

317 positiveGenus_inertia_list_product Δ.signature

318 have hc :

319 c =

320 ⁅(SemidirectProduct.inl

321 (positiveGenusSmoothSurfaceBase Δ.signature) :

322 PositiveGenusSmoothQuotient Δ.signature),

323 SemidirectProduct.inr positiveGenusSmoothTopGenerator⁆ := by

324 let c0 : PositiveGenusSmoothQuotient Δ.signature :=

325 ⁅(SemidirectProduct.inl

326 (positiveGenusSmoothSurfaceBase Δ.signature) :

327 PositiveGenusSmoothQuotient Δ.signature),

328 SemidirectProduct.inr positiveGenusSmoothTopGenerator⁆

329 have hmap :

330 (fun j : Fin Δ.signature.orbitGenus =>

331 ⁅positiveGenusGeneratorImageCore Δ

332 (ULift.up (ProfiniteFenchelGenerator.surfaceA j)),

333 positiveGenusGeneratorImageCore Δ

334 (ULift.up (ProfiniteFenchelGenerator.surfaceB j))⁆) =

335 fun j : Fin Δ.signature.orbitGenus =>

336 if j.val = 0 then c0 else 1 := by

337 funext j

338 by_cases hj : j.val = 0

339 · simp only [positiveGenusGeneratorImageCore, hj, ↓reduceIte, c0]

340 · simp only [positiveGenusGeneratorImageCore, hj, ↓reduceIte, commutatorElement_self, c0]

341 dsimp [c]

342 rw [hmap]

343 exact list_finRange_prod_eq_single_zeroVal hGenus c0

344 have hCusp :

345 ((List.finRange Δ.signature.numCusps).map fun j =>

346 positiveGenusGeneratorImageCore Δ

347 (ULift.up (ProfiniteFenchelGenerator.cusp j))).prod = 1 := by

348 simp only [positiveGenusGeneratorImageCore, List.map_const', List.length_finRange,

349 List.prod_replicate, one_pow]

350 have hec : e * c = 1 := by

351 rw [he, hc]

352 exact positiveGenusSmoothEllipticProduct_mul_surfaceCommutator

353 Δ.signature

354 have hce : c * e = 1 := by

355 have h' := congrArg (fun x => e⁻¹ * x * e) hec

356 simpa [mul_assoc] using h'

357 dsimp [profiniteFenchelTotalRelation]

358 rw [hCusp]

359 simpa [e, c, mul_assoc] using hce

360

361private theorem positiveGenusGeneratorImage_lifted_total_relation

362 (Δ : ProfiniteFGroup.{u}) (hGenus : 1 ≤ Δ.signature.orbitGenus) :

363 profiniteFenchelTotalRelation

364 (fun i => positiveGenusGeneratorImage Δ

365 (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))

366 (fun i => positiveGenusGeneratorImage Δ

367 (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))

368 (fun j => positiveGenusGeneratorImage Δ

369 (ULift.up (ProfiniteFenchelGenerator.cusp j)))

370 (fun k => positiveGenusGeneratorImage Δ

371 (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1 := by

372 apply

373 (MulEquiv.ulift :

374 ULift.{u, 0} (PositiveGenusSmoothQuotient Δ.signature) ≃*

375 PositiveGenusSmoothQuotient Δ.signature).injective

376 simpa [positiveGenusGeneratorImage, profiniteFenchelTotalRelation,

377 map_list_prod, Function.comp_def, map_commutatorElement] using

378 positiveGenusGeneratorImage_total_relation Δ hGenus

379

380private theorem positiveGenusGeneratorImage_period_relation

381 (Δ : ProfiniteFGroup.{u}) (k : Fin Δ.signature.numPeriods) :

382 positiveGenusGeneratorImageCore Δ

383 (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^

384 Δ.signature.periods k = 1 := by

385 change

386 (SemidirectProduct.inl

387 (positiveGenusSmoothEllipticBase Δ.signature k) :

388 PositiveGenusSmoothQuotient Δ.signature) ^

389 Δ.signature.periods k = 1

390 rw [← map_pow

391 (SemidirectProduct.inl :

392 PositiveGenusSmoothBase Δ.signature →*

393 PositiveGenusSmoothQuotient Δ.signature)]

394 simp only [positiveGenusSmoothEllipticBase_pow_period, map_one]

395

396private theorem positiveGenusGeneratorImage_lifted_period_relation

397 (Δ : ProfiniteFGroup.{u}) (k : Fin Δ.signature.numPeriods) :

398 positiveGenusGeneratorImage Δ

399 (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^

400 Δ.signature.periods k = 1 := by

401 apply

402 (MulEquiv.ulift :

403 ULift.{u, 0} (PositiveGenusSmoothQuotient Δ.signature) ≃*

404 PositiveGenusSmoothQuotient Δ.signature).injective

405 simpa [positiveGenusGeneratorImage] using

406 positiveGenusGeneratorImage_period_relation Δ k

407

408private theorem positiveGenusGeneratorImage_inertia_order

409 (Δ : ProfiniteFGroup.{u}) (k : Fin Δ.signature.numPeriods) :

410 orderOf

411 (positiveGenusGeneratorImageCore Δ

412 (ULift.up (ProfiniteFenchelGenerator.inertia k))) =

413 Δ.signature.periods k := by

414 change

415 orderOf

416 ((SemidirectProduct.inl

417 (positiveGenusSmoothEllipticBase Δ.signature k)) :

418 PositiveGenusSmoothQuotient Δ.signature) =

419 Δ.signature.periods k

420 rw [orderOf_injective

421 (SemidirectProduct.inl :

422 PositiveGenusSmoothBase Δ.signature →*

423 PositiveGenusSmoothQuotient Δ.signature)

424 SemidirectProduct.inl_injective

425 (positiveGenusSmoothEllipticBase Δ.signature k)]

426 rw [positiveGenusSmoothEllipticBase, orderOf_ofAdd_eq_addOrderOf]

427 exact zmodBasisVector_pair_neg_addOrderOf Δ.signature.periods k

428

429private theorem positiveGenusGeneratorImage_lifted_inertia_order

430 (Δ : ProfiniteFGroup.{u}) (k : Fin Δ.signature.numPeriods) :

431 orderOf

432 (positiveGenusGeneratorImage Δ

433 (ULift.up (ProfiniteFenchelGenerator.inertia k))) =

434 Δ.signature.periods k := by

435 have horder :=

436 orderOf_injective

437 ((MulEquiv.ulift :

438 ULift.{u, 0} (PositiveGenusSmoothQuotient Δ.signature) ≃*

439 PositiveGenusSmoothQuotient Δ.signature).toMonoidHom)

440 (MulEquiv.ulift :

441 ULift.{u, 0} (PositiveGenusSmoothQuotient Δ.signature) ≃*

442 PositiveGenusSmoothQuotient Δ.signature).injective

443 (positiveGenusGeneratorImage Δ

444 (ULift.up (ProfiniteFenchelGenerator.inertia k)))

445 rw [← horder]

446 exact positiveGenusGeneratorImage_inertia_order Δ k

447

448/-- The positive-genus smooth quotient is finite. -/

449theorem positiveGenusSmoothQuotient_finite

450 (σ : FenchelSignature) :

451 Finite (PositiveGenusSmoothQuotient σ) := by

452 classical

453 letI : Finite (FenchelPeriodCoordinate σ) :=

454 zmodCoordinateFamily_finite σ.periods

455 (fun i => lt_of_lt_of_le (by decide : 0 < 2) (σ.period_ge_two i))

456 haveI : Finite (PositiveGenusSmoothBase σ) := by

457 infer_instance

458 haveI : Finite (Multiplicative (ZMod 2)) := by

459 infer_instance

460 exact Finite.of_injective

461 (fun q : PositiveGenusSmoothQuotient σ => (q.left, q.right))

462 (by

463 intro q r h

464 exact SemidirectProduct.ext

465 (congrArg Prod.fst h) (congrArg Prod.snd h))

466

467/-- The positive-genus smooth quotient has derived length at most two. -/

468theorem positiveGenusSmoothQuotient_derivedSeries_two_eq_bot

469 (σ : FenchelSignature) :

470 derivedSeries (PositiveGenusSmoothQuotient σ) 2 = ⊥ := by

471 let ρ : PositiveGenusSmoothQuotient σ →*

472 Multiplicative (ZMod 2) :=

473 SemidirectProduct.rightHom

474 have hfirst :

475 derivedSeries (PositiveGenusSmoothQuotient σ) 1 ≤ ρ.ker := by

476 rw [derivedSeries_one]

477 exact Abelianization.commutator_subset_ker ρ

478 have hkerComm :

479 ⁅ρ.ker, ρ.ker⁆ =

480 (⊥ : Subgroup (PositiveGenusSmoothQuotient σ)) := by

481 rw [Subgroup.commutator_eq_bot_iff_le_centralizer]

482 intro x hx

483 rw [Subgroup.mem_centralizer_iff]

484 intro y hy

485 have hxright : x.right = 1 := by

486 simpa [ρ] using MonoidHom.mem_ker.mp hx

487 have hyright : y.right = 1 := by

488 simpa [ρ] using MonoidHom.mem_ker.mp hy

489 ext

490 · simp only [SemidirectProduct.mul_left, hyright, map_one, MulAut.one_apply,

491 mul_comm, toAdd_mul, Prod.fst_add, Pi.add_apply, hxright]

492 · simp only [SemidirectProduct.mul_left, hyright, map_one, MulAut.one_apply,

493 mul_comm, toAdd_mul, Prod.snd_add, Pi.add_apply, hxright]

494 · simp only [SemidirectProduct.mul_right, hyright, hxright, mul_one, toAdd_one]

495 apply le_antisymm

496 · calc

497 derivedSeries (PositiveGenusSmoothQuotient σ) 2 =

498 ⁅derivedSeries (PositiveGenusSmoothQuotient σ) 1,

499 derivedSeries (PositiveGenusSmoothQuotient σ) 1⁆ := by

500 change derivedSeries (PositiveGenusSmoothQuotient σ) (1 + 1) =

501 ⁅derivedSeries (PositiveGenusSmoothQuotient σ) 1,

502 derivedSeries (PositiveGenusSmoothQuotient σ) 1⁆

503 rw [derivedSeries_succ]

504 _ ≤ ⁅ρ.ker, ρ.ker⁆ := Subgroup.commutator_mono hfirst hfirst

505 _ = ⊥ := hkerComm

506 · exact bot_le

507

508noncomputable instance instFiniteULiftPositiveGenusSmoothQuotient (σ : FenchelSignature) :

509 Finite (ULift.{u, 0} (PositiveGenusSmoothQuotient σ)) := by

510 letI : Finite (PositiveGenusSmoothQuotient σ) :=

511 positiveGenusSmoothQuotient_finite σ

512 infer_instance

513

514noncomputable def positiveGenusSmoothQuotientData

515 (Δ : ProfiniteFGroup.{u}) (hGenus : 1 ≤ Δ.signature.orbitGenus) :

516 ProfiniteSmoothQuotientData Δ 2 :=

517 ProfiniteSmoothQuotientData.ofPresentationLiftToFiniteOfRelationsOfDerivedSeries

518 Δ (positiveGenusGeneratorImage Δ)

519 (positiveGenusGeneratorImage_lifted_total_relation Δ hGenus)

520 (positiveGenusGeneratorImage_lifted_period_relation Δ)

521 (derivedSeries_ulift_eq_bot_of

522 (positiveGenusSmoothQuotient_derivedSeries_two_eq_bot

523 Δ.signature))

524 (positiveGenusGeneratorImage_lifted_inertia_order Δ)

525

526end ProfiniteFGroup

527

528end FenchelNielsen