Fundamental domains for the two groups acting on ℍ #
A congruence subgroup Γ ≤ SL(2, ℤ) reaches ℍ two ways: through its image in PSL(2, ℤ), the
group that acts faithfully and the one every fundamental-domain statement about ℍ is phrased
for, and through Γ.map (mapGL ℝ) inside GL(2, ℝ), the group a modular form is slashed by and
the only one large enough to contain a Hecke double-coset representative. This file records when a
fundamental domain for the first is one for the second.
There is no coercion PSL(2, ℤ) → GL(2, ℝ) to read that along: opposite lifts γ and -γ of one
class have distinct images under mapGL ℝ. What is true is that each class acts as any of its
lifts does — UpperHalfPlane.pslMk_smul and Matrix.SpecialLinearGroup.pslMk_smul_set.
Main results #
TauCeti.isFundamentalDomain_map_mapGL: forΓ ⊓ center = ⊥, a fundamental domain for the image ofΓinPSL(2, ℤ)is one for its image inGL(2, ℝ).
The hypothesis is not a convenience. Without it the statement is false: if -I ∈ Γ then -I is a
non-identity element of Γ.map (mapGL ℝ) acting trivially on ℍ, so (-I) • S = S and
MeasureTheory.IsFundamentalDomain fails its a.e.-disjointness requirement for every S of
positive measure. Passing to PSL(2, ℤ) is exactly what removes that element. Γ ⊓ center = ⊥
holds for Γ₁(N) and Γ(N) at every level except N = 1 and N = 2, the two where -1 ≡ 1
(so level 0, where the congruence is an equation in ℤ, is on the good side alongside N ≥ 3);
SL(2, ℤ) is the case N = 1, and Γ₀(N) fails at every level.
A fundamental domain for the image of Γ in PSL(2, ℤ) is one for its image in
GL(2, ℝ), provided Γ meets the centre of SL(2, ℤ) trivially.
Without that hypothesis the statement is false: -I ∈ Γ would put a non-identity element of
Γ.map (mapGL ℝ) acting trivially on ℍ, so (-I) • S = S and a.e.-disjointness fails for every
S of positive measure. The module docstring says where each side of the statement is used.