Yamaguchi Lean 4 Library
FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation
FenchelNielsenZomorrodian/Discrete/Core/CompactFuchsianPresentation

FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation

6 Definition | 1 Abbreviation | 1 Structure | 1 Inductive | 2 Instance

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

Declarations

Structure FenchelNielsen.FuchsianSignature GitHub 
structure FuchsianSignature extends FenchelSignature where
  numCusps_eq_zero : numCusps = 0
  numPeriods_ge_three : 3 ≤ numPeriods

Signature data for a compact Fuchsian presentation.

Inductive FenchelNielsen.FuchsianGenerator GitHub 
inductive FuchsianGenerator (σ : FuchsianSignature)
  | elliptic : Fin σ.numPeriods → FuchsianGenerator σ
  | surfaceA : Fin σ.orbitGenus → FuchsianGenerator σ
  | surfaceB : Fin σ.orbitGenus → FuchsianGenerator σ

Generator type for the compact Fuchsian presentation.

Definition FenchelNielsen.FuchsianGenerator.equivSum GitHub 
def FuchsianGenerator.equivSum (σ : FuchsianSignature) :
    FuchsianGenerator σ ≃ Fin σ.numPeriods ⊕ Fin σ.orbitGenus ⊕ Fin σ.orbitGenus where
  toFun
    | .elliptic i => .inl i
    | .surfaceA j => .inr (.inl j)
    | .surfaceB j => .inr (.inr j)
  invFun
    | .inl i => FuchsianGenerator.elliptic i
    | .inr (.inl j) => FuchsianGenerator.surfaceA j
    | .inr (.inr j) => FuchsianGenerator.surfaceB j
  left_inv := by
    intro x
    cases x <;> rfl
  right_inv := by
    intro x
    cases x with
    | inl i => rfl
    | inr y =>
        cases y <;> rfl

The Fuchsian generator type is equivalent to the corresponding sum of generator families.

Instance FenchelNielsen.FuchsianGenerator.instFintype GitHub 
instance FuchsianGenerator.instFintype (σ : FuchsianSignature) :
    Fintype (FuchsianGenerator σ) :=
  Fintype.ofEquiv (Fin σ.numPeriods ⊕ Fin σ.orbitGenus ⊕ Fin σ.orbitGenus)
    (FuchsianGenerator.equivSum σ).symm

The compact Fuchsian generator type is finite.

Definition FenchelNielsen.xWord GitHub 
def xWord (σ : FuchsianSignature) (i : Fin σ.numPeriods) :
    FreeGroup (FuchsianGenerator σ) :=
  FreeGroup.of <| FuchsianGenerator.elliptic i

The elliptic generator word in the compact Fuchsian presentation.

Definition FenchelNielsen.aWord GitHub 
def aWord (σ : FuchsianSignature) (j : Fin σ.orbitGenus) :
    FreeGroup (FuchsianGenerator σ) :=
  FreeGroup.of <| FuchsianGenerator.surfaceA j

The a-generator word in the compact Fuchsian presentation.

Definition FenchelNielsen.bWord GitHub 
def bWord (σ : FuchsianSignature) (j : Fin σ.orbitGenus) :
    FreeGroup (FuchsianGenerator σ) :=
  FreeGroup.of <| FuchsianGenerator.surfaceB j

The b-generator word in the compact Fuchsian presentation.

Definition FenchelNielsen.totalRelation GitHub 
def totalRelation (σ : FuchsianSignature) :
    FreeGroup (FuchsianGenerator σ) :=
  ((List.finRange σ.numPeriods).map fun i => xWord σ i).prod *
    ((List.finRange σ.orbitGenus).map fun j => ⁅aWord σ j, bWord σ j⁆).prod

The total relation word in the compact Fuchsian presentation.

Definition FenchelNielsen.relators GitHub 
def relators (σ : FuchsianSignature) : Set (FreeGroup (FuchsianGenerator σ)) :=
  {w | (∃ i : Fin σ.numPeriods, w = (xWord σ i) ^ σ.periods i) ∨ w = totalRelation σ}

The relator family of the compact Fuchsian presentation.

Abbreviation FenchelNielsen.FuchsianPresentedGroup GitHub 
abbrev FuchsianPresentedGroup (σ : FuchsianSignature) : Type :=
  PresentedGroup (relators σ)

The group presented by the compact Fuchsian generators and relators.

Instance FenchelNielsen.instGroupFuchsianPresentedGroup GitHub 
instance instGroupFuchsianPresentedGroup (σ : FuchsianSignature) :
    Group (FuchsianPresentedGroup σ) :=
  inferInstance

The compact Fuchsian presented group carries the quotient group structure induced by the presentation relators.