# 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.UpperHalfPlane). We then define the standard fundamental domain (ModularGroup.fd, π) for this action and show (ModularGroup.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 : β).normSq β§ |z.re| β€ (1 : β) / 2}

The standard open fundamental domain of the action of SL(2,β€) on β, denoted πα΅: fdo := {z | 1 < (z : β).normSq β§ |z.re| < (1 : β) / 2}

These notations are localized in the Modular locale and can be enabled via open scoped 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 ModularGroup.smul_eq_lcRow0_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 ModularGroup.T) and S=[[0,-1],[1,0]] (see ModularGroup.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 ModularGroup.exists_max_im), and then among those, to minimize |(gβ’z).re| (see ModularGroup.exists_row_one_eq_and_min_re).

theorem ModularGroup.bottom_row_coprime {R : Type u_1} [] (g : ) :
IsCoprime (β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 ModularGroup.bottom_row_surj {R : Type u_1} [] :
Set.SurjOn (fun (g : ) => βg 1) Set.univ {cd : Fin 2 β R | IsCoprime (cd 0) (cd 1)}

Every pair ![c, d] of coprime integers is the "bottom_row" of some element g=[[*,*],[c,d]] of SL(2,β€).

theorem ModularGroup.tendsto_normSq_coprime_pair (z : UpperHalfPlane) :
Filter.Tendsto (fun (p : Fin 2 β β€) => Complex.normSq (β(p 0) * βz + β(p 1))) Filter.cofinite Filter.atTop

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
Instances For
@[simp]
theorem ModularGroup.lcRow0_apply (p : Fin 2 β β€) (g : Matrix (Fin 2) (Fin 2) β) :
g = β(p 0) * g 0 0 + β(p 1) * g 0 1
@[simp]
theorem ModularGroup.lcRow0Extend_apply {cd : Fin 2 β β€} (hcd : IsCoprime (cd 0) (cd 1)) (f : (i : Fin 2) β (fun (a : Fin 2) => Fin 2 β β) i) (i : Fin 2) :
β (a : Fin 2), f i a = (![ (Matrix.GeneralLinearGroup.toLinear (Matrix.planeConformalMatrix (β(cd 0)) (-β(cd 1)) β―)), LinearEquiv.refl β (Fin 2 β β)] i) (f i) a
@[simp]
theorem ModularGroup.lcRow0Extend_symm_apply {cd : Fin 2 β β€} (hcd : IsCoprime (cd 0) (cd 1)) (f : (i : Fin 2) β (fun (a : Fin 2) => Fin 2 β β) i) (i : Fin 2) :
β (a : Fin 2), f i a = (LinearEquiv.symm (![ (Matrix.GeneralLinearGroup.toLinear (Matrix.planeConformalMatrix (β(cd 0)) (-β(cd 1)) β―)), LinearEquiv.refl β (Fin 2 β β)] i)) (f i) a
def ModularGroup.lcRow0Extend {cd : Fin 2 β β€} (hcd : IsCoprime (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
• One or more equations did not get rendered due to their size.
Instances For
theorem ModularGroup.tendsto_lcRow0 {cd : Fin 2 β β€} (hcd : IsCoprime (cd 0) (cd 1)) :
Filter.Tendsto (fun (g : { g : // βg 1 = cd }) => () β()) Filter.cofinite

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

theorem ModularGroup.smul_eq_lcRow0_add {g : } (z : UpperHalfPlane) {p : Fin 2 β β€} (hp : IsCoprime (p 0) (p 1)) (hg : βg 1 = p) :
β(g β’ z) = β( β) / (β(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 ModularGroup.tendsto_abs_re_smul (z : UpperHalfPlane) {p : Fin 2 β β€} (hp : IsCoprime (p 0) (p 1)) :
Filter.Tendsto (fun (g : { g : // βg 1 = p }) => |UpperHalfPlane.re (βg β’ z)|) Filter.cofinite Filter.atTop
theorem ModularGroup.exists_max_im (z : UpperHalfPlane) :
β (g : ), β (g' : ), UpperHalfPlane.im (g' β’ z) β€ UpperHalfPlane.im (g β’ z)

For z : β, there is a g : SL(2,β€) maximizing (gβ’z).im

theorem ModularGroup.exists_row_one_eq_and_min_re (z : UpperHalfPlane) {cd : Fin 2 β β€} (hcd : IsCoprime (cd 0) (cd 1)) :
β (g : ), βg 1 = cd β§ β (g' : ), βg 1 = βg' 1 β |UpperHalfPlane.re (g β’ z)| β€ |UpperHalfPlane.re (g' β’ z)|

Given z : β and a bottom row (c,d), among the g : SL(2,β€) with this bottom row, minimize |(gβ’z).re|.

theorem ModularGroup.coe_T_zpow_smul_eq (z : UpperHalfPlane) {n : β€} :
β() = βz + βn
theorem ModularGroup.exists_eq_T_zpow_of_c_eq_zero {g : } (hc : βg 1 0 = 0) :
β (n : β€), β (z : UpperHalfPlane), g β’ z =
theorem ModularGroup.g_eq_of_c_eq_one {g : } (hc : βg 1 0 = 1) :
g = ModularGroup.T ^ βg 0 0 * ModularGroup.S * ModularGroup.T ^ βg 1 1
theorem ModularGroup.normSq_S_smul_lt_one {z : UpperHalfPlane} (h : 1 < Complex.normSq βz) :
Complex.normSq β() < 1

If 1 < |z|, then |S β’ z| < 1.

theorem ModularGroup.im_lt_im_S_smul {z : UpperHalfPlane} (h : Complex.normSq βz < 1) :

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

The standard (closed) fundamental domain of the action of SL(2,β€) on β.

Equations
Instances For

The standard open fundamental domain of the action of SL(2,β€) on β.

Equations
Instances For

The standard (closed) fundamental domain of the action of SL(2,β€) on β.

Equations
Instances For

The standard open fundamental domain of the action of SL(2,β€) on β.

Equations
Instances For
theorem ModularGroup.one_lt_normSq_T_zpow_smul {z : UpperHalfPlane} (hz : ) (n : β€) :
1 < Complex.normSq β()

If z β πα΅, and n : β€, then |z + n| > 1.

theorem ModularGroup.exists_smul_mem_fd (z : UpperHalfPlane) :
β (g : ),

First Fundamental Domain Lemma: Any z : β can be moved to π by an element of SL(2,β€)

theorem ModularGroup.abs_c_le_one {g : } {z : UpperHalfPlane} (hz : ) (hg : ) :
|βg 1 0| β€ 1

An auxiliary result en route to ModularGroup.c_eq_zero.

theorem ModularGroup.c_eq_zero {g : } {z : UpperHalfPlane} (hz : ) (hg : ) :
βg 1 0 = 0

An auxiliary result en route to ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo.

theorem ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo {g : } {z : UpperHalfPlane} (hz : ) (hg : ) :
z = g β’ z

Second Fundamental Domain Lemma: if both z and g β’ z are in the open domain πα΅, where z : β and g : SL(2,β€), then z = g β’ z.