FenchelNielsenZomorrodian/Discrete/Core/EllipticCompact.lean

1import FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Core/EllipticCompact.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

11/-!

12# Discrete Fenchel and compact Fuchsian core definitions

14Signatures, generator indices, presentations, elliptic generators, quotient homomorphisms, and family-signature transformations.

17namespace FenchelNielsen

19def ellipticElement (σ : FuchsianSignature) (i : Fin σ.numPeriods) :

21 PresentedGroup.of (rels := relators σ) (FuchsianGenerator.elliptic i)

24 (σ : FuchsianSignature) (i : Fin σ.numPeriods) :

25 ellipticElement σ i ^ σ.periods i = 1 := by

27 (PresentedGroup.one_of_mem (rels := relators σ)

28 (x := (xWord σ i) ^ σ.periods i) (Or.inl ⟨i, rfl⟩))

31 (σ : FuchsianSignature) (i : Fin σ.numPeriods) {n : ℕ}

32 (hdiv : σ.periods i ∣ n) :

33 ellipticElement σ i ^ n = 1 := by

34 rcases hdiv with ⟨k, rfl⟩

38 (σ : FuchsianSignature) (i : Fin σ.numPeriods) {n : ℤ}

39 (hdiv : (σ.periods i : ℤ) ∣ n) :

40 ellipticElement σ i ^ n = 1 := by

41 rcases hdiv with ⟨k, rfl⟩

42 rw [zpow_mul, zpow_natCast, ellipticElement_pow_period_eq_one, one_zpow]

44end FenchelNielsen