mathlib documentation

number_theory.modular

The action of the modular group SL(2, ℤ) on the upper half-plane #

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 : matrix.special_linear_group (fin 2) 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 : matrix.special_linear_group (fin 2) R), 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) ) :
(modular_group.lc_row0 p) g = (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) :
@[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) :
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)) :

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 : matrix.special_linear_group (fin 2) } (z : upper_half_plane) {p : fin 2} (hp : is_coprime (p 0) (p 1)) (hg : g 1 = p) :
(g z) = ((modular_group.lc_row0 p) 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)) :

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 : matrix.special_linear_group (fin 2) ), g 1 = cd ∀ (g' : matrix.special_linear_group (fin 2) ), 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|.

The matrix T = [[1,1],[0,1]] as an element of SL(2,ℤ)

Equations

The matrix S = [[0,-1],[1,0]] as an element of SL(2,ℤ)

Equations
theorem modular_group.coe_S  :
modular_group.S = ![![0, -1], ![1, 0]]
theorem modular_group.coe_T  :
modular_group.T = ![![1, 1], ![0, 1]]
theorem modular_group.coe_T_inv  :
modular_group.T⁻¹ = ![![1, -1], ![0, 1]]
theorem modular_group.coe_T_zpow (n : ) :
(modular_group.T ^ n) = ![![1, n], ![0, 1]]

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,ℤ)

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.