FenchelNielsenZomorrodian.Discrete.CompactFuchsian.AbelianizationKernel.Conditions

5 Definition

This module develops the rewriting and basis constructions behind the subgroup calculations. It tracks words and relations through the chosen transversal to obtain the required presentation or basis statements.

Open this file on GitHub

import

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.AbelianizationKernel.Periods
Mathlib.Data.Fintype.Sigma

Imported by

Definition FenchelNielsen.AbelianizationKernelConditionFamily GitHub

def AbelianizationKernelConditionFamily {ι : Type*} [Fintype ι] [DecidableEq ι]
    (periods : ι → ℕ) : Prop :=
  ∀ i, periods i ∣ otherPeriodsLcmFamily periods i ∨
    2 * otherPeriodsLcmFamily periods i ≤ otherPeriodsProductFamily periods i

The abelianization-kernel condition is rewritten as the corresponding finite presentation relation on elliptic and canonical generators.

Definition FenchelNielsen.AbelianizationKernelCondition GitHub

def AbelianizationKernelCondition (σ : FenchelSignature) : Prop :=
  AbelianizationKernelConditionFamily σ.periods

The abelianization-kernel condition is rewritten as the corresponding finite presentation relation on elliptic and canonical generators.

Definition FenchelNielsen.FenchelSignature.OneStepNumericalCondition GitHub

def FenchelSignature.OneStepNumericalCondition (σ : FenchelSignature) : Prop :=
  σ.HasCusps ∨ σ.IsCompact ∧ σ.AbelianPeriodCondition

This abelianization lemma computes the period-coordinate relation determined by the elliptic generators.

Definition FenchelNielsen.FenchelSignature.DeltaOneAbelianPeriodCondition GitHub

def FenchelSignature.DeltaOneAbelianPeriodCondition (σ : FenchelSignature) : Prop :=
  LCMConditionFamily
    (nonOneSubfamilyPeriods (abelianizationKernelRawPeriods σ.periods))

The delta-one abelian period condition attached to a compact Fuchsian signature.

Definition FenchelNielsen.FenchelSignature.TwoStepNumericalCondition GitHub

def FenchelSignature.TwoStepNumericalCondition (σ : FenchelSignature) : Prop :=
  (σ.orbitGenus, σ.numCusps) ≠ (0, 0) ∨
    (σ.orbitGenus, σ.numCusps) = (0, 0) ∧
      σ.DeltaOneAbelianPeriodCondition

This abelianization lemma computes the period-coordinate relation determined by the elliptic generators.

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.AbelianizationKernel.Conditions

Declarations