FenchelNielsenZomorrodian.Profinite

11 sections | 11 files | 190 declarations

This module formalizes the profinite part of the Fenchel--Nielsen--Zomorrodian theorem and uses the named local axiom frontier.

CharacteristicClosure

1 files | 14 declarations | 10 Theorem | 4 Definition

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

CompactFuchsianSignature

1 files | 1 declarations | 1 Definition

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

CuspedQuotient

1 files | 17 declarations | 9 Theorem | 4 Definition | 1 Abbreviation | 3 Instance

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

DiscreteBridge

1 files | 18 declarations | 14 Theorem | 4 Definition

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

FGroup

1 files | 64 declarations | 34 Theorem | 22 Definition | 2 Abbreviation | 1 Structure | 1 Inductive | 4 Instance

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

LowPeriodQuotient

1 files | 19 declarations | 9 Theorem | 5 Definition | 5 Instance

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

MainTheorem

1 files | 5 declarations | 5 Theorem

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

Perfectness

1 files | 5 declarations | 5 Theorem

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

PositiveGenusQuotient

1 files | 29 declarations | 14 Theorem | 10 Definition | 2 Abbreviation | 3 Instance

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

SmoothQuotient

1 files | 11 declarations | 7 Theorem | 3 Definition | 1 Structure

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

TorsionFrontier

1 files | 7 declarations | 4 Theorem | 2 Definition | 1 Axiom

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