Fundamental domains, covolume, and cofinite Fuchsian groups #
Let Γ ≤ PSL(2, ℝ) be a discrete subgroup, acting on the upper half-plane ℍ with Mathlib's
invariant measure volume (density y⁻² dx dy). This file shows that Γ has a measurable
fundamental domain, so that the covolume MeasureTheory.covolume Γ ℍ — the hyperbolic area of
the quotient Γ \ ℍ — is the area of any measurable fundamental domain
(MeasureTheory.IsFundamentalDomain.covolume_eq_volume), and defines the cofinite Fuchsian
groups as the discrete subgroups of finite covolume.
The fundamental domain comes from the general construction
MeasureTheory.Measure.exists_isFundamentalDomain_of_properlyDiscontinuousSMul. Its hypothesis,
that the points with nontrivial stabilizer are null, holds because a nontrivial element of
PSL(2, ℝ) fixes at most one point of ℍ and a discrete subgroup is countable, so these points
form a countable set.
Main declarations #
Subgroup.instCountableOfDiscreteTopology: a discrete subgroup ofPSL(2, ℝ)is countable.Subgroup.countable_compl_freeLocus: the points ofℍwith nontrivial stabilizer in a countableΓform a countable set.Subgroup.freeLocus_nonempty: some point ofℍhas trivial stabilizer in a countableΓ.Subgroup.exists_isFundamentalDomain: a discreteΓhas a measurable fundamental domain whose translates are pairwise disjoint.Subgroup.IsCofinite: a discrete subgroup of finite covolume.Subgroup.IsCofinite.volume_ne_top,MeasureTheory.IsFundamentalDomain.isCofinite_of_volume_ne_top: a discrete subgroup is cofinite exactly when one, equivalently every, fundamental domain has finite area.Subgroup.isCofinite_conjAct_smul_iff: cofiniteness is invariant under conjugation.Subgroup.isCofinite_iff_isCofinite_and_finiteIndex: a subgroup of a discrete group is cofinite exactly when the larger group is cofinite and the index is finite.
Positivity, conjugation invariance and index multiplicativity of the covolume are the generic
MeasureTheory.covolume_pos, MeasureTheory.covolume_conjAct_smul and
MeasureTheory.covolume_eq_card_mul_covolume, which apply directly to PSL(2, ℝ) acting on ℍ.
References #
- Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §§3.1 and 4.1.
- Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §§9.1 and 10.4.
A discrete subgroup of PSL(2, ℝ) is countable, since it acts properly discontinuously on
the σ-compact space ℍ.
The points of ℍ with nontrivial stabilizer in a countable subgroup of PSL(2, ℝ) form a
countable set: each nontrivial element fixes at most one point.
For a countable subgroup of PSL(2, ℝ), the points of ℍ with nontrivial stabilizer form a
null set.
A countable subgroup of PSL(2, ℝ) has a point of ℍ with trivial stabilizer.
A Fuchsian group has a measurable fundamental domain. For a discrete subgroup
Γ ≤ PSL(2, ℝ) there is a measurable fundamental domain for its action on ℍ whose translates
by distinct elements of Γ are disjoint.
A discrete subgroup of PSL(2, ℝ) has a fundamental domain, so that its covolume is the area
of any of its fundamental domains.
A subgroup Γ ≤ PSL(2, ℝ) is cofinite (a lattice) when it is discrete and the quotient
Γ \ ℍ has finite hyperbolic area, that is, Γ has finite covolume.
- discreteTopology : DiscreteTopology ↥Γ
Instances For
A discrete subgroup is cofinite exactly when its covolume is finite.
Cofiniteness is a conjugacy invariant: a conjugate g Γ g⁻¹ of a subgroup
Γ ≤ PSL(2, ℝ) is cofinite exactly when Γ is.
A cofinite subgroup has fundamental domains of finite area.
Cofiniteness and finite index: a subgroup Δ of a discrete subgroup Γ ≤ PSL(2, ℝ)
is cofinite exactly when Γ is cofinite and Δ has finite index in Γ.
A discrete subgroup of PSL(2, ℝ) with a fundamental domain of finite area is cofinite.