FenchelNielsenZomorrodian.Discrete

10 sections | 80 files | 761 declarations

This module formalizes the discrete group-theoretic part of the Fenchel--Nielsen--Zomorrodian theorem.

Abelianization

5 files | 25 declarations | 16 Theorem | 7 Definition | 2 Abbreviation

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

Arithmetic

4 files | 16 declarations | 7 Theorem | 8 Definition | 1 Abbreviation

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

CompactFuchsian

42 files | 601 declarations | 399 Theorem | 185 Definition | 14 Abbreviation | 3 Structure

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

Coordinates

3 files | 9 declarations | 3 Theorem | 4 Definition | 2 Abbreviation

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

Core

6 files | 34 declarations | 9 Theorem | 19 Definition | 1 Abbreviation | 2 Structure | 1 Inductive | 2 Instance

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

FiniteIndex

6 files | 18 declarations | 12 Theorem | 4 Definition | 1 Abbreviation | 1 Structure

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

GroupTheory

3 files | 8 declarations | 6 Theorem | 2 Definition

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

MainTheorem

1 files | 1 declarations | 1 Theorem

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

Singerman

7 files | 43 declarations | 31 Theorem | 12 Definition

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

Torsion

3 files | 6 declarations | 4 Theorem | 1 Definition | 1 Axiom

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