FenchelNielsenZomorrodian.Discrete.CompactFuchsian.AbelianizationKernel.Periods

4 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.Core.FamilySignature

Imported by

Definition FenchelNielsen.abelianizationKernelPeriodFamily GitHub

def abelianizationKernelPeriodFamily {ι : Type*} [Fintype ι] [DecidableEq ι]
    (periods : ι → ℕ) (i : ι) : ℕ :=
  periods i / Nat.gcd (periods i) (otherPeriodsLcmFamily periods i)

The period family used to describe the abelianization-kernel condition.

Definition FenchelNielsen.abelianizationKernelMultiplicityFamily GitHub

def abelianizationKernelMultiplicityFamily {ι : Type*} [Fintype ι] [DecidableEq ι]
    (periods : ι → ℕ) (i : ι) : ℕ :=
  otherPeriodsProductFamily periods i / otherPeriodsLcmFamily periods i

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

Definition FenchelNielsen.abelianizationKernelRawPeriods GitHub

def abelianizationKernelRawPeriods {ι : Type*} [Fintype ι] [DecidableEq ι]
    (periods : ι → ℕ)
    (x : Sigma fun i : ι => Fin (abelianizationKernelMultiplicityFamily periods i)) : ℕ :=
  abelianizationKernelPeriodFamily periods x.1

The raw period list before forming the abelianization-kernel period family.

Definition FenchelNielsen.abelianizationKernelPeriods GitHub

def abelianizationKernelPeriods (σ : FuchsianSignature) :
    NonOneSubfamilyIndex (abelianizationKernelRawPeriods σ.periods) → ℕ :=
  nonOneSubfamilyPeriods (abelianizationKernelRawPeriods σ.periods)

The compact Fuchsian abelianization kernel uses this period family.

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.AbelianizationKernel.Periods

Declarations