FenchelNielsenZomorrodian/Discrete/CompactFuchsian/AbelianizationKernel/Periods.lean

1import FenchelNielsenZomorrodian.Discrete.Core.FamilySignature

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/AbelianizationKernel/Periods.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

11/-!

12# Abelianization-kernel conditions for compact Fuchsian groups

14Numerical and period-family criteria ensuring that abelianization kernels satisfy the conditions needed for torsion-free finite-index subgroups.

17namespace FenchelNielsen

19def abelianizationKernelPeriodFamily {ι : Type*} [Fintype ι] [DecidableEq ι]

20 (periods : ι → ℕ) (i : ι) : ℕ :=

21 periods i / Nat.gcd (periods i) (otherPeriodsLcmFamily periods i)

23def abelianizationKernelMultiplicityFamily {ι : Type*} [Fintype ι] [DecidableEq ι]

24 (periods : ι → ℕ) (i : ι) : ℕ :=

27def abelianizationKernelRawPeriods {ι : Type*} [Fintype ι] [DecidableEq ι]

28 (periods : ι → ℕ)

29 (x : Sigma fun i : ι => Fin (abelianizationKernelMultiplicityFamily periods i)) : ℕ :=

36end FenchelNielsen