Yamaguchi Lean 4 Library
FenchelNielsenZomorrodian/Discrete/Core/EllipticQuotientHom.lean
FenchelNielsenZomorrodian/Discrete/Core/EllipticQuotientHom/Source

FenchelNielsenZomorrodian/Discrete/Core/EllipticQuotientHom.lean

1import FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation
2import Mathlib.Algebra.BigOperators.Fin
3import Mathlib.GroupTheory.Commutator.Basic
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Core/EllipticQuotientHom.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Discrete Fenchel and compact Fuchsian core definitions
16Signatures, generator indices, presentations, elliptic generators, quotient homomorphisms, and family-signature transformations.
17-/
19open scoped BigOperators
21namespace FenchelNielsen
24 (σ : FuchsianSignature) {A : Type*} [CommGroup A]
25 (ξ : Fin σ.numPeriods → A) :
27 | .elliptic i => ξ i
28 | .surfaceA _ => 1
29 | .surfaceB _ => 1
32 (σ : FuchsianSignature) {A : Type*} [CommGroup A]
33 (ξ : Fin σ.numPeriods → A)
34 (hpow : ∀ i, ξ i ^ σ.periods i = 1)
35 (hprod : ∏ i : Fin σ.numPeriods, ξ i = 1) :
36 ∀ r ∈ relators σ, FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ) r = 1 := by
37 intro r hr
38 rcases hr with ⟨i, rfl⟩ | rfl
39 · simpa [xWord, ellipticQuotientGeneratorImage] using hpow i
40 · dsimp [totalRelation]
41 rw [map_mul, map_list_prod, map_list_prod]
42 have hEll :
43 (List.map (⇑(FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ)))
44 (List.map (fun i => xWord σ i) (List.finRange σ.numPeriods))).prod = 1 := by
45 rw [List.map_map]
46 have hEllMap :
47 (⇑(FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ)) ∘
48 fun i : Fin σ.numPeriods => xWord σ i) = ξ := by
49 funext i
50 simp only [xWord, Function.comp_apply, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage]
51 rw [hEllMap]
52 calc
53 (List.map ξ (List.finRange σ.numPeriods)).prod = ∏ i : Fin σ.numPeriods, ξ i := by
54 simpa using (Fin.prod_univ_def (f := ξ)).symm
55 _ = 1 := hprod
56 have hComm :
57 (List.map (⇑(FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ)))
58 (List.map (fun j => ⁅aWord σ j, bWord σ j⁆)
59 (List.finRange σ.orbitGenus))).prod = 1 := by
60 rw [List.map_map]
61 have hCommMap :
62 (⇑(FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ)) ∘
63 fun j : Fin σ.orbitGenus => ⁅aWord σ j, bWord σ j⁆) =
64 fun _ => (1 : A) := by
65 funext j
66 dsimp
67 rw [map_commutatorElement]
68 simp only [aWord, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage, bWord, commutatorElement_self]
69 rw [hCommMap]
70 simp only [List.map_const', List.length_finRange, List.prod_replicate, one_pow]
71 rw [hEll, hComm]
72 simp only [mul_one]
75 (σ : FuchsianSignature) {A : Type*} [CommGroup A]
76 (ξ : Fin σ.numPeriods → A)
77 (hpow : ∀ i, ξ i ^ σ.periods i = 1)
78 (hprod : ∏ i : Fin σ.numPeriods, ξ i = 1) :
80 PresentedGroup.toGroup (rels := relators σ)
85 (σ : FuchsianSignature) {A : Type*} [CommGroup A]
86 (ξ : Fin σ.numPeriods → A)
87 (hpow : ∀ i, ξ i ^ σ.periods i = 1)
88 (hprod : ∏ i : Fin σ.numPeriods, ξ i = 1)
89 (i : Fin σ.numPeriods) :
90 ellipticQuotientHom σ ξ hpow hprod
91 (PresentedGroup.of (rels := relators σ) (FuchsianGenerator.elliptic i)) =
92 ξ i := by
93 simp only [ellipticQuotientHom, PresentedGroup.toGroup.of, ellipticQuotientGeneratorImage]
95end FenchelNielsen