mathlibdocumentation

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.fundamental_domain, 𝒟) for this action and show (modular_group.exists_smul_mem_fundamental_domain) that any point in can be moved inside 𝒟.

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

@[protected, instance]
noncomputable def modular_group.upper_half_plane.mul_action {R : Type u_1} [comm_ring R] [ ] :

For a subring R of , the action of SL(2, R) on the upper half-plane, as a restriction of the SL(2, ℝ)-action defined by upper_half_plane.mul_action.

Equations
theorem modular_group.coe_smul (g : SL(2,)) (z : ) :
(g z) =
theorem modular_group.re_smul (g : SL(2,)) (z : ) :
(g z).re = .re
@[simp]
theorem modular_group.smul_coe (g : SL(2,)) (z : ) :
g z = g z
@[simp]
theorem modular_group.neg_smul (g : SL(2,)) (z : ) :
-g z = g z
theorem modular_group.im_smul (g : SL(2,)) (z : ) :
(g z).im = .im
@[simp]
theorem modular_group.denom_apply (g : SL(2,)) (z : ) :
= ((g 1 0)) * z + (g 1 1)
theorem modular_group.bottom_row_coprime {R : Type u_1} [comm_ring R] (g : SL(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 : SL(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) ) :
= ((p 0)) * g 0 0 + ((p 1)) * g 0 1
theorem modular_group.lc_row0_apply' (a b : ) (c d : ) (v : fin 2) :
(modular_group.lc_row0 ![c, d]) ![![a, b], v] = (c) * a + (d) * b
@[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 {p : fin 2} (hp : is_coprime (p 0) (p 1)) (z : ) {g : SL(2,)} (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 : ) {p : fin 2} (hp : is_coprime (p 0) (p 1)) :
theorem modular_group.exists_max_im (z : ) :
∃ (g : SL(2,)), ∀ (g' : SL(2,)), (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 : ) {cd : fin 2} (hcd : is_coprime (cd 0) (cd 1)) :
∃ (g : SL(2,)), g 1 = cd ∀ (g' : SL(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 T' (= 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

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

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

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

Any z : ℍ can be moved to 𝒟 by an element of SL(2,ℤ)