Prove2Me

The modular function λ\lambda: H/Γ(2)≅C∖{0,1}\mathbb H/\Gamma(2)\cong\mathbb C\setminus\{0,1\}

Open
MilnorDynamics.modular_lambda_exists

by Lucas · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysiscomplex-dynamicsmodular-forms

This is the existence of the elliptic modular function λ\lambda together with its basic mapping properties.

Let H={τ∈C:Im⁡τ>0}\mathbb H=\{\tau\in\mathbb C:\operatorname{Im}\tau>0\} be the upper half-plane with the Möbius action of SL2(Z)\mathrm{SL}_2(\mathbb Z), and let Γ(2)⊂SL2(Z)\Gamma(2)\subset\mathrm{SL}_2(\mathbb Z) be the principal congruence subgroup of level 22 (matrices congruent to the identity modulo 22). There is a holomorphic function λ:H→C\lambda:\mathbb H\to\mathbb C such that

  1. λ\lambda omits the values 00 and 11: λ(τ)∉{0,1}\lambda(\tau)\notin\{0,1\} for all τ∈H\tau\in\mathbb H;
  2. λ\lambda takes every other value: for every w∈C∖{0,1}w\in\mathbb C\setminus\{0,1\} there is τ∈H\tau\in\mathbb H with λ(τ)=w\lambda(\tau)=w;
  3. the fibres of λ\lambda are exactly the Γ(2)\Gamma(2)-orbits: for all τ,τ′∈H\tau,\tau'\in\mathbb H,
λ(τ)=λ(τ′)  ⟺  τ′=γ⋅τ  for some γ∈Γ(2).\lambda(\tau)=\lambda(\tau')\iff \tau'=\gamma\cdot\tau\ \text{ for some }\gamma\in\Gamma(2).

Equivalently, λ\lambda is Γ(2)\Gamma(2)-invariant and induces a bijection H/Γ(2)→C∖{0,1}\mathbb H/\Gamma(2)\to\mathbb C\setminus\{0,1\}. A classical witness is λ(τ)=θ2(τ)4/θ3(τ)4\lambda(\tau)=\theta_2(\tau)^4/\theta_3(\tau)^4, with θ2(τ)=∑n∈Zeπi(n+1/2)2τ\theta_2(\tau)=\sum_{n\in\mathbb Z}e^{\pi i(n+1/2)^2\tau} and θ3(τ)=∑n∈Zeπin2τ\theta_3(\tau)=\sum_{n\in\mathbb Z}e^{\pi i n^2\tau}.

This is the analytic half of the construction of the universal covering H→C∖{0,1}\mathbb H\to\mathbb C\setminus\{0,1\}; combined with the proper discontinuity of the Γ(2)\Gamma(2)-action it yields Milnor's Lemma 2.5 for the triply punctured sphere, and hence Montel's theorem.

Formalization Note The function is recorded as p:C→Cp:\mathbb C\to\mathbb C, complex differentiable on the open set {Im⁡z>0}\{\operatorname{Im}z>0\}; only its values on H\mathbb H matter. Points of H\mathbb H are Mathlib's UpperHalfPlane, coerced to C\mathbb C, and γ⋅τ\gamma\cdot\tau is Mathlib's action of SL(2, ℤ) on ℍ, under which −I-I acts trivially.

Preamble
import Mathlib

open Set Topology UpperHalfPlane
Formal statement
namespace MilnorDynamics

theorem modular_lambda_exists :
    ∃ p : ℂ → ℂ, DifferentiableOn ℂ p {z : ℂ | 0 < z.im} ∧
      (∀ τ : ℍ, p τ ≠ 0 ∧ p τ ≠ 1) ∧
      (∀ w : ℂ, w ≠ 0 → w ≠ 1 → ∃ τ : ℍ, p τ = w) ∧
      (∀ τ τ' : ℍ, p τ = p τ' ↔ ∃ γ ∈ CongruenceSubgroup.Gamma 2, γ • τ = τ') := by sorry

end MilnorDynamics
Source
J. Milnor, Dynamics in One Complex Variable, 3rd ed., Annals of Mathematics Studies 160, Princeton University Press, 2006, §2, Lemma 2.5 (The Triply Punctured Sphere), p. 17; L. V. Ahlfors, Complex Analysis, 3rd ed., McGraw-Hill, 1979, Chapter 7, §3.4 (The modular function λ(τ))

View graph