FenchelNielsenZomorrodian/Discrete/CompactFuchsian/AbelianizationKernel/Conditions.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.AbelianizationKernel.Periods
2import Mathlib.Data.Fintype.Sigma
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/AbelianizationKernel/Conditions.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Abelianization-kernel conditions for compact Fuchsian groups
15Numerical and period-family criteria ensuring that abelianization kernels satisfy the conditions needed for torsion-free finite-index subgroups.
16-/
18namespace FenchelNielsen
20def AbelianizationKernelConditionFamily {ι : Type*} [Fintype ι] [DecidableEq ι]
21 (periods : ι → ℕ) : Prop :=
22 ∀ i, periods i ∣ otherPeriodsLcmFamily periods i ∨
23 2 * otherPeriodsLcmFamily periods i ≤ otherPeriodsProductFamily periods i
25def AbelianizationKernelCondition (σ : FenchelSignature) : Prop :=
26 AbelianizationKernelConditionFamily σ.periods
28def FenchelSignature.OneStepNumericalCondition (σ : FenchelSignature) : Prop :=
29 σ.HasCusps ∨ σ.IsCompact ∧ σ.AbelianPeriodCondition
31def FenchelSignature.DeltaOneAbelianPeriodCondition (σ : FenchelSignature) : Prop :=
33 (nonOneSubfamilyPeriods (abelianizationKernelRawPeriods σ.periods))
35def FenchelSignature.TwoStepNumericalCondition (σ : FenchelSignature) : Prop :=
36 (σ.orbitGenus, σ.numCusps) ≠ (0, 0) ∨
37 (σ.orbitGenus, σ.numCusps) = (0, 0) ∧
38 σ.DeltaOneAbelianPeriodCondition
40end FenchelNielsen