The action of the modular group SL(2, ℤ) on the upper half-plane #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define the action of SL(2,ℤ) on ℍ (via restriction of the SL(2,ℝ) action in
analysis.complex.upper_half_plane). We then define the standard fundamental domain
(modular_group.fd, 𝒟) for this action and show
(modular_group.exists_smul_mem_fd) that any point in ℍ can be
moved inside 𝒟.
Main definitions #
The standard (closed) fundamental domain of the action of SL(2,ℤ) on ℍ, denoted 𝒟:
fd := {z | 1 ≤ (z : ℂ).norm_sq ∧ |z.re| ≤ (1 : ℝ) / 2}
The standard open fundamental domain of the action of SL(2,ℤ) on ℍ, denoted 𝒟ᵒ:
fdo := {z | 1 < (z : ℂ).norm_sq ∧ |z.re| < (1 : ℝ) / 2}
These notations are localized in the modular locale and can be enabled via open_locale modular.
Main results #
Any z : ℍ can be moved to 𝒟 by an element of SL(2,ℤ):
exists_smul_mem_fd (z : ℍ) : ∃ g : SL(2,ℤ), g • z ∈ 𝒟
If both z and γ • z are in the open domain 𝒟ᵒ then z = γ • z:
eq_smul_self_of_mem_fdo_mem_fdo {z : ℍ} {g : SL(2,ℤ)} (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : z = g • z
Discussion #
Standard proofs make use of the identity
g • z = a / c - 1 / (c (cz + d))
for g = [[a, b], [c, d]] in SL(2), but this requires separate handling of whether c = 0.
Instead, our proof makes use of the following perhaps novel identity (see
modular_group.smul_eq_lc_row0_add):
g • z = (a c + b d) / (c^2 + d^2) + (d z - c) / ((c^2 + d^2) (c z + d))
where there is no issue of division by zero.
Another feature is that we delay until the very end the consideration of special matrices
T=[[1,1],[0,1]] (see modular_group.T) and S=[[0,-1],[1,0]] (see modular_group.S), by
instead using abstract theory on the properness of certain maps (phrased in terms of the filters
filter.cocompact, filter.cofinite, etc) to deduce existence theorems, first to prove the
existence of g maximizing (g•z).im (see modular_group.exists_max_im), and then among
those, to minimize |(g•z).re| (see modular_group.exists_row_one_eq_and_min_re).
The two numbers c, d in the "bottom_row" of g=[[*,*],[c,d]] in SL(2, ℤ) are coprime.
Every pair ![c, d] of coprime integers is the "bottom_row" of some element g=[[*,*],[c,d]]
of SL(2,ℤ).
The function (c,d) → |cz+d|^2 is proper, that is, preimages of bounded-above sets are finite.
Given coprime_pair p=(c,d), the matrix [[a,b],[*,*]] is sent to a*c+b*d.
This is the linear map version of this operation.
Equations
- modular_group.lc_row0 p = (↑(p 0) • linear_map.proj 0 + ↑(p 1) • linear_map.proj 1).comp (linear_map.proj 0)
Linear map sending the matrix [a, b; c, d] to the matrix [ac₀ + bd₀, - ad₀ + bc₀; c, d], for
some fixed (c₀, d₀).
Equations
The map lc_row0 is proper, that is, preimages of cocompact sets are finite in
[[* , *], [c, d]].
This replaces (g•z).re = a/c + * in the standard theory with the following novel identity:
g • z = (a c + b d) / (c^2 + d^2) + (d z - c) / ((c^2 + d^2) (c z + d))
which does not need to be decomposed depending on whether c = 0.
For z : ℍ, there is a g : SL(2,ℤ) maximizing (g•z).im
Given z : ℍ and a bottom row (c,d), among the g : SL(2,ℤ) with this bottom row, minimize
|(g•z).re|.
If 1 < |z|, then |S • z| < 1.
If |z| < 1, then applying S strictly decreases im.
The standard (closed) fundamental domain of the action of SL(2,ℤ) on ℍ.
Equations
- modular_group.fd = {z : upper_half_plane | 1 ≤ ⇑complex.norm_sq ↑z ∧ |z.re| ≤ 1 / 2}
The standard open fundamental domain of the action of SL(2,ℤ) on ℍ.
Equations
- modular_group.fdo = {z : upper_half_plane | 1 < ⇑complex.norm_sq ↑z ∧ |z.re| < 1 / 2}
If z ∈ 𝒟ᵒ, and n : ℤ, then |z + n| > 1.
Any z : ℍ can be moved to 𝒟 by an element of SL(2,ℤ)
An auxiliary result en route to modular_group.c_eq_zero.
An auxiliary result en route to modular_group.eq_smul_self_of_mem_fdo_mem_fdo.
Second Main Fundamental Domain Lemma: if both z and g • z are in the open domain 𝒟ᵒ,
where z : ℍ and g : SL(2,ℤ), then z = g • z.