FenchelNielsenZomorrodian/Discrete/Abelianization/PeriodQuotient.lean

1import FenchelNielsenZomorrodian.Discrete.Abelianization.PeriodCoordinate

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Abelianization/PeriodQuotient.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

10-/

11/-!

12# Abelianization of compact Fuchsian presentations

14Finite cyclic coordinate calculations for elliptic generators, period classes, period quotients, and order formulas in compact Fuchsian abelianizations.

15-/

17namespace FenchelNielsen

19noncomputable def periodCoordinate_finite

20 (σ : FuchsianSignature) :

21 Finite (PeriodCoordinate σ) := by

22 exact zmodCoordinateFamily_finite σ.periods

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

25noncomputable def periodAbelianization_finite

26 (σ : FuchsianSignature) :

27 Finite (PeriodAbelianization σ) := by

28 haveI : Finite (PeriodCoordinate σ) := periodCoordinate_finite σ

29 exact Finite.of_surjective

30 (fun v : PeriodCoordinate σ => (v : PeriodAbelianization σ))

31 QuotientAddGroup.mk_surjective

33end FenchelNielsen