FenchelNielsenZomorrodian.Profinite.CompactFuchsianSignature

1 Definition

This module develops Fenchel--Nielsen--Zomorrodian presentation reductions, period relations, reindexings, and quotient maps.

Open this file on GitHub

import

FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation

Imported by

FenchelNielsenZomorrodian.Profinite.DiscreteBridge

Definition FenchelNielsen.ProfiniteFGroup.compactFuchsianSignature GitHub

def compactFuchsianSignature
    (σ : FenchelSignature) (hCompact : σ.IsCompact)
    (hPeriods : 3 ≤ σ.numPeriods) : FuchsianSignature where
  orbitGenus := σ.orbitGenus
  numCusps := σ.numCusps
  numPeriods := σ.numPeriods
  periods := σ.periods
  period_ge_two := σ.period_ge_two
  numCusps_eq_zero := hCompact
  numPeriods_ge_three := hPeriods

Promote a compact Fenchel signature with at least three periods to the compact Fuchsian signature used by the discrete compact three-step theorem.

FenchelNielsenZomorrodian.Profinite.CompactFuchsianSignature

Declarations