Documentation

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

source
theorem ModularGroup.bottom_row_coprime {R : Type u_1} [CommRing R] (g : Matrix.SpecialLinearGroup (Fin 2) R) :
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.

source
theorem ModularGroup.bottom_row_surj {R : Type u_1} [CommRing R] :
Set.SurjOn (fun (g : Matrix.SpecialLinearGroup (Fin 2) R) => ↑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,β„€).

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

source
def ModularGroup.lcRow0 (p : Fin 2 β†’ β„€) :
Matrix (Fin 2) (Fin 2) ℝ β†’β‚—[ℝ] ℝ

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
    source
    @[simp]
    theorem ModularGroup.lcRow0_apply (p : Fin 2 β†’ β„€) (g : Matrix (Fin 2) (Fin 2) ℝ) :
    (lcRow0 p) g = ↑(p 0) * g 0 0 + ↑(p 1) * g 0 1
    source
    def ModularGroup.lcRow0Extend {cd : Fin 2 β†’ β„€} (hcd : IsCoprime (cd 0) (cd 1)) :
    Matrix (Fin 2) (Fin 2) ℝ ≃ₗ[ℝ] Matrix (Fin 2) (Fin 2) ℝ

    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
      source
      @[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 a✝ : Fin 2) :
      (lcRow0Extend hcd).symm f i a✝ = (![(LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 β†’ ℝ)) (Matrix.GeneralLinearGroup.toLin (Matrix.planeConformalMatrix (↑(cd 0)) (-↑(cd 1)) β‹―)), LinearEquiv.refl ℝ (Fin 2 β†’ ℝ)] i).symm (f i) a✝
      source
      @[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 a✝ : Fin 2) :
      (lcRow0Extend hcd) f i a✝ = (![(LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 β†’ ℝ)) (Matrix.GeneralLinearGroup.toLin (Matrix.planeConformalMatrix (↑(cd 0)) (-↑(cd 1)) β‹―)), LinearEquiv.refl ℝ (Fin 2 β†’ ℝ)] i) (f i) a✝
      source
      theorem ModularGroup.tendsto_lcRow0 {cd : Fin 2 β†’ β„€} (hcd : IsCoprime (cd 0) (cd 1)) :
      Filter.Tendsto (fun (g : { g : Matrix.SpecialLinearGroup (Fin 2) β„€ // ↑g 1 = cd }) => (lcRow0 cd) ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) Filter.cofinite (Filter.cocompact ℝ)

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

      source
      theorem ModularGroup.smul_eq_lcRow0_add {g : Matrix.SpecialLinearGroup (Fin 2) β„€} (z : UpperHalfPlane) {p : Fin 2 β†’ β„€} (hp : IsCoprime (p 0) (p 1)) (hg : ↑g 1 = p) :
      ↑(g β€’ z) = ↑((lcRow0 p) ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) 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.

      source
      theorem ModularGroup.tendsto_abs_re_smul (z : UpperHalfPlane) {p : Fin 2 β†’ β„€} (hp : IsCoprime (p 0) (p 1)) :
      Filter.Tendsto (fun (g : { g : Matrix.SpecialLinearGroup (Fin 2) β„€ // ↑g 1 = p }) => |(↑g β€’ z).re|) Filter.cofinite Filter.atTop
      source
      theorem ModularGroup.exists_max_im (z : UpperHalfPlane) :
      βˆƒ (g : Matrix.SpecialLinearGroup (Fin 2) β„€), βˆ€ (g' : Matrix.SpecialLinearGroup (Fin 2) β„€), (g' β€’ z).im ≀ (g β€’ z).im

      For z : ℍ, there is a g : SL(2,β„€) maximizing (gβ€’z).im

      source
      theorem ModularGroup.exists_row_one_eq_and_min_re (z : UpperHalfPlane) {cd : Fin 2 β†’ β„€} (hcd : IsCoprime (cd 0) (cd 1)) :
      βˆƒ (g : Matrix.SpecialLinearGroup (Fin 2) β„€), ↑g 1 = cd ∧ βˆ€ (g' : Matrix.SpecialLinearGroup (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|.

      source
      theorem ModularGroup.coe_T_zpow_smul_eq (z : UpperHalfPlane) {n : β„€} :
      ↑(T ^ n β€’ z) = ↑z + ↑n
      source
      theorem ModularGroup.re_T_zpow_smul (z : UpperHalfPlane) (n : β„€) :
      (T ^ n β€’ z).re = z.re + ↑n
      source
      theorem ModularGroup.im_T_zpow_smul (z : UpperHalfPlane) (n : β„€) :
      (T ^ n β€’ z).im = z.im
      source
      theorem ModularGroup.re_T_smul (z : UpperHalfPlane) :
      (T β€’ z).re = z.re + 1
      source
      theorem ModularGroup.im_T_smul (z : UpperHalfPlane) :
      (T β€’ z).im = z.im
      source
      theorem ModularGroup.re_T_inv_smul (z : UpperHalfPlane) :
      (T⁻¹ β€’ z).re = z.re - 1
      source
      theorem ModularGroup.im_T_inv_smul (z : UpperHalfPlane) :
      (T⁻¹ β€’ z).im = z.im
      source
      theorem ModularGroup.exists_eq_T_zpow_of_c_eq_zero {g : Matrix.SpecialLinearGroup (Fin 2) β„€} (hc : ↑g 1 0 = 0) :
      βˆƒ (n : β„€), βˆ€ (z : UpperHalfPlane), g β€’ z = T ^ n β€’ z
      source
      theorem ModularGroup.g_eq_of_c_eq_one {g : Matrix.SpecialLinearGroup (Fin 2) β„€} (hc : ↑g 1 0 = 1) :
      g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1
      source
      theorem ModularGroup.normSq_S_smul_lt_one {z : UpperHalfPlane} (h : 1 < Complex.normSq ↑z) :
      Complex.normSq ↑(S β€’ z) < 1

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

      source
      theorem ModularGroup.im_lt_im_S_smul {z : UpperHalfPlane} (h : Complex.normSq ↑z < 1) :
      z.im < (S β€’ z).im

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

      source
      def ModularGroup.fd :
      Set UpperHalfPlane

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

      Equations
      Instances For
        source
        def ModularGroup.fdo :
        Set UpperHalfPlane

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

        Equations
        Instances For
          source
          def Modular.termπ’Ÿ :
          Lean.ParserDescr

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

          Equations
          Instances For
            source
            def Modular.Β«termπ’Ÿα΅’Β» :
            Lean.ParserDescr

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

            Equations
            Instances For
              source
              theorem ModularGroup.abs_two_mul_re_lt_one_of_mem_fdo {z : UpperHalfPlane} (h : z ∈ fdo) :
              |2 * z.re| < 1
              source
              theorem ModularGroup.three_lt_four_mul_im_sq_of_mem_fdo {z : UpperHalfPlane} (h : z ∈ fdo) :
              3 < 4 * z.im ^ 2
              source
              theorem ModularGroup.three_le_four_mul_im_sq_of_mem_fd {Ο„ : UpperHalfPlane} (h : Ο„ ∈ fd) :
              3 ≀ 4 * Ο„.im ^ 2

              non-strict variant of ModularGroup.three_le_four_mul_im_sq_of_mem_fdo

              source
              theorem ModularGroup.one_lt_normSq_T_zpow_smul {z : UpperHalfPlane} (hz : z ∈ fdo) (n : β„€) :
              1 < Complex.normSq ↑(T ^ n β€’ z)

              If z ∈ π’Ÿα΅’, and n : β„€, then |z + n| > 1.

              source
              theorem ModularGroup.eq_zero_of_mem_fdo_of_T_zpow_mem_fdo {z : UpperHalfPlane} {n : β„€} (hz : z ∈ fdo) (hg : T ^ n β€’ z ∈ fdo) :
              n = 0
              source
              theorem ModularGroup.exists_smul_mem_fd (z : UpperHalfPlane) :
              βˆƒ (g : Matrix.SpecialLinearGroup (Fin 2) β„€), g β€’ z ∈ fd

              First Fundamental Domain Lemma: Any z : ℍ can be moved to π’Ÿ by an element of SL(2,β„€)

              source
              theorem ModularGroup.abs_c_le_one {g : Matrix.SpecialLinearGroup (Fin 2) β„€} {z : UpperHalfPlane} (hz : z ∈ fdo) (hg : g β€’ z ∈ fdo) :
              |↑g 1 0| ≀ 1

              An auxiliary result en route to ModularGroup.c_eq_zero.

              source
              theorem ModularGroup.c_eq_zero {g : Matrix.SpecialLinearGroup (Fin 2) β„€} {z : UpperHalfPlane} (hz : z ∈ fdo) (hg : g β€’ z ∈ fdo) :
              ↑g 1 0 = 0

              An auxiliary result en route to ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo.

              source
              theorem ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo {g : Matrix.SpecialLinearGroup (Fin 2) β„€} {z : UpperHalfPlane} (hz : z ∈ fdo) (hg : g β€’ z ∈ fdo) :
              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.

              source
              theorem ModularGroup.exists_one_half_le_im_smul (Ο„ : UpperHalfPlane) :
              βˆƒ (Ξ³ : Matrix.SpecialLinearGroup (Fin 2) β„€), 1 / 2 ≀ (Ξ³ β€’ Ο„).im
              source
              theorem ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le (Ο„ : UpperHalfPlane) :
              βˆƒ (Ξ³ : Matrix.SpecialLinearGroup (Fin 2) β„€), 1 / 2 ≀ (Ξ³ β€’ Ο„).im ∧ β€–UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) Ξ³)) ↑τ‖ ≀ 1

              For every Ο„ : ℍ there is some Ξ³ ∈ SL(2, β„€) that sends it to an element whose imaginary part is at least 1/2 and such that denom Ξ³ Ο„ has norm at most 1.