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

FenchelNielsenZomorrodian/Discrete/Core/CompactFuchsianPresentation.lean

1import FenchelNielsenZomorrodian.Discrete.Core.Signature
2import Mathlib.Algebra.Group.Commutator
3import Mathlib.Data.Fintype.Sum
4import Mathlib.GroupTheory.PresentedGroup
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Core/CompactFuchsianPresentation.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Discrete Fenchel and compact Fuchsian core definitions
17Signatures, generator indices, presentations, elliptic generators, quotient homomorphisms, and family-signature transformations.
18-/
20open scoped BigOperators
22namespace FenchelNielsen
24structure FuchsianSignature extends FenchelSignature where
25 numCusps_eq_zero : numCusps = 0
26 numPeriods_ge_three : 3 ≤ numPeriods
29 | elliptic : Fin σ.numPeriods → FuchsianGenerator σ
30 | surfaceA : Fin σ.orbitGenus → FuchsianGenerator σ
31 | surfaceB : Fin σ.orbitGenus → FuchsianGenerator σ
33def FuchsianGenerator.equivSum (σ : FuchsianSignature) :
34 FuchsianGenerator σ ≃ Fin σ.numPeriods ⊕ Fin σ.orbitGenus ⊕ Fin σ.orbitGenus where
35 toFun
36 | .elliptic i => .inl i
37 | .surfaceA j => .inr (.inl j)
38 | .surfaceB j => .inr (.inr j)
39 invFun
40 | .inl i => FuchsianGenerator.elliptic i
41 | .inr (.inl j) => FuchsianGenerator.surfaceA j
42 | .inr (.inr j) => FuchsianGenerator.surfaceB j
43 left_inv := by
44 intro x
45 cases x <;> rfl
46 right_inv := by
47 intro x
48 cases x with
49 | inl i => rfl
50 | inr y =>
51 cases y <;> rfl
53instance FuchsianGenerator.instFintype (σ : FuchsianSignature) :
54 Fintype (FuchsianGenerator σ) :=
55 Fintype.ofEquiv (Fin σ.numPeriods ⊕ Fin σ.orbitGenus ⊕ Fin σ.orbitGenus)
56 (FuchsianGenerator.equivSum σ).symm
58def xWord (σ : FuchsianSignature) (i : Fin σ.numPeriods) :
59 FreeGroup (FuchsianGenerator σ) :=
60 FreeGroup.of <| FuchsianGenerator.elliptic i
62def aWord (σ : FuchsianSignature) (j : Fin σ.orbitGenus) :
63 FreeGroup (FuchsianGenerator σ) :=
64 FreeGroup.of <| FuchsianGenerator.surfaceA j
66def bWord (σ : FuchsianSignature) (j : Fin σ.orbitGenus) :
67 FreeGroup (FuchsianGenerator σ) :=
68 FreeGroup.of <| FuchsianGenerator.surfaceB j
71 FreeGroup (FuchsianGenerator σ) :=
72 ((List.finRange σ.numPeriods).map fun i => xWord σ i).prod *
73 ((List.finRange σ.orbitGenus).map fun j => ⁅aWord σ j, bWord σ j⁆).prod
75def relators (σ : FuchsianSignature) : Set (FreeGroup (FuchsianGenerator σ)) :=
76 {w | (∃ i : Fin σ.numPeriods, w = (xWord σ i) ^ σ.periods i) ∨ w = totalRelation σ}
79 PresentedGroup (relators σ)
83 inferInstance
85end FenchelNielsen