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

FenchelNielsenZomorrodian.Discrete.Core

5 sections | 5 files | 34 declarations

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

CompactFuchsianPresentation

1 files | 11 declarations | 6 Definition | 1 Abbreviation | 1 Structure | 1 Inductive | 2 Instance
Signature data for a compact Fuchsian presentation.

EllipticCompact

1 files | 4 declarations | 3 Theorem | 1 Definition
An elliptic element of a compact Fuchsian signature is one of the specified elliptic generators.

EllipticQuotientHom

1 files | 4 declarations | 2 Theorem | 2 Definition
The elliptic quotient sends each generator to the prescribed elliptic image.

FamilySignature

1 files | 3 declarations | 2 Theorem | 1 Definition
The Fuchsian signature assembled from a family of period data.

Signature

1 files | 12 declarations | 2 Theorem | 9 Definition | 1 Structure
The signature data for a Fenchel--Nielsen compact Fuchsian presentation.