FenchelNielsenZomorrodian.Discrete.Coordinates.FenchelPeriodCoordinate

2 Definition | 1 Abbreviation

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

Imported by

Abbreviation FenchelNielsen.FenchelPeriodCoordinate GitHub

abbrev FenchelPeriodCoordinate (σ : FenchelSignature) :=
  ZModCoordinateFamily σ.periods

Coordinate data for one Fenchel period.

Definition FenchelNielsen.fenchelPeriodBasisVector GitHub

def fenchelPeriodBasisVector (σ : FenchelSignature) (i : Fin σ.numPeriods) :
    FenchelPeriodCoordinate σ :=
  zmodBasisVector σ.periods i

The basis vector corresponding to a single Fenchel period coordinate.

Definition FenchelNielsen.fenchelPeriodBasisSum GitHub

def fenchelPeriodBasisSum (σ : FenchelSignature) : FenchelPeriodCoordinate σ :=
  ∑ i : Fin σ.numPeriods, fenchelPeriodBasisVector σ i

The finite sum of Fenchel period basis vectors used for the period relation.

FenchelNielsenZomorrodian.Discrete.Coordinates.FenchelPeriodCoordinate

Declarations