FenchelNielsenZomorrodian.Discrete.Abelianization.PeriodQuotient

2 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.Abelianization.PeriodCoordinate

Imported by

Definition FenchelNielsen.periodCoordinate_finite GitHub

noncomputable def periodCoordinate_finite
    (σ : FuchsianSignature) :
    Finite (PeriodCoordinate σ) := by
  exact zmodCoordinateFamily_finite σ.periods
    (fun i => lt_of_lt_of_le (by decide : 0 < 2) (σ.period_ge_two i))

The period-coordinate quotient used in the abelianized presentation is finite.

Definition FenchelNielsen.periodAbelianization_finite GitHub

noncomputable def periodAbelianization_finite
    (σ : FuchsianSignature) :
    Finite (PeriodAbelianization σ) := by
  haveI : Finite (PeriodCoordinate σ) := periodCoordinate_finite σ
  exact Finite.of_surjective
    (fun v : PeriodCoordinate σ => (v : PeriodAbelianization σ))
    QuotientAddGroup.mk_surjective

The period abelianization attached to the Fuchsian signature is finite, because it is obtained from a finite-rank period-coordinate group by imposing finite period relations.

FenchelNielsenZomorrodian.Discrete.Abelianization.PeriodQuotient

Declarations