# mathlib3documentation

number_theory.modular

# 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).

theorem modular_group.bottom_row_coprime {R : Type u_1} [comm_ring R] (g : R) :
is_coprime (g 1 0) (g 1 1)

The two numbers c, d in the "bottom_row" of g=[[*,*],[c,d]] in SL(2, ℤ) are coprime.

theorem modular_group.bottom_row_surj {R : Type u_1} [comm_ring R] :
set.surj_on (λ (g : , g 1) set.univ {cd : fin 2 R | is_coprime (cd 0) (cd 1)}

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
@[simp]
theorem modular_group.lc_row0_apply (p : fin 2 ) (g : matrix (fin 2) (fin 2) ) :
= (p 0) * g 0 0 + (p 1) * g 0 1
@[simp]
theorem modular_group.lc_row0_extend_apply {cd : fin 2 } (hcd : is_coprime (cd 0) (cd 1)) (f : Π (i : fin 2), (λ (ᾰ : fin 2), fin 2 ) i) (i ᾰ : fin 2) :
i = (![ (matrix.general_linear_group.to_linear (-(cd 1)) _)), (fin 2 )] i) (f i)
@[simp]
theorem modular_group.lc_row0_extend_symm_apply {cd : fin 2 } (hcd : is_coprime (cd 0) (cd 1)) (f : Π (i : fin 2), (λ (ᾰ : fin 2), fin 2 ) i) (i ᾰ : fin 2) :
.symm) f i = ((![ (matrix.general_linear_group.to_linear (-(cd 1)) _)), (fin 2 )] i).symm) (f i)
noncomputable def modular_group.lc_row0_extend {cd : fin 2 } (hcd : is_coprime (cd 0) (cd 1)) :

Linear map sending the matrix [a, b; c, d] to the matrix [ac₀ + bd₀, - ad₀ + bc₀; c, d], for some fixed (c₀, d₀).

Equations
theorem modular_group.tendsto_lc_row0 {cd : fin 2 } (hcd : is_coprime (cd 0) (cd 1)) :
filter.tendsto (λ (g : {g // g 1 = cd}), g) filter.cofinite

The map lc_row0 is proper, that is, preimages of cocompact sets are finite in [[* , *], [c, d]].

theorem modular_group.smul_eq_lc_row0_add {g : } (z : upper_half_plane) {p : fin 2 } (hp : is_coprime (p 0) (p 1)) (hg : g 1 = p) :
(g z) = g) / ((p 0) ^ 2 + (p 1) ^ 2) + ((p 1) * z - (p 0)) / (((p 0) ^ 2 + (p 1) ^ 2) * ((p 0) * z + (p 1)))

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.

theorem modular_group.tendsto_abs_re_smul (z : upper_half_plane) {p : fin 2 } (hp : is_coprime (p 0) (p 1)) :
theorem modular_group.exists_max_im (z : upper_half_plane) :
(g : , (g' : , (g' z).im (g z).im

For z : ℍ, there is a g : SL(2,ℤ) maximizing (g•z).im

theorem modular_group.exists_row_one_eq_and_min_re (z : upper_half_plane) {cd : fin 2 } (hcd : is_coprime (cd 0) (cd 1)) :
(g : , g 1 = cd (g' : , g 1 = g' 1 |(g z).re| |(g' z).re|

Given z : ℍ and a bottom row (c,d), among the g : SL(2,ℤ) with this bottom row, minimize |(g•z).re|.

theorem modular_group.exists_eq_T_zpow_of_c_eq_zero {g : } (hc : g 1 0 = 0) :
(n : ), (z : upper_half_plane), g z =
theorem modular_group.g_eq_of_c_eq_one {g : } (hc : g 1 0 = 1) :

If 1 < |z|, then |S • z| < 1.

theorem modular_group.im_lt_im_S_smul {z : upper_half_plane} (h : < 1) :
z.im < .im

If |z| < 1, then applying S strictly decreases im.

The standard (closed) fundamental domain of the action of SL(2,ℤ) on ℍ.

Equations

The standard open fundamental domain of the action of SL(2,ℤ) on ℍ.

Equations

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.

theorem modular_group.c_eq_zero {g : } {z : upper_half_plane} (hz : z modular_group.fdo) (hg : g z modular_group.fdo) :
g 1 0 = 0

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.