Prove2Me

Γ(2)\Gamma(2) acts properly discontinuously on H\mathbb H, freely modulo ±I\pm I

Proved
MilnorDynamics.gammaTwo_smul_nhds_disjoint

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

complex-analysiscomplex-dynamicsmodular-forms

Let H={τ∈C:Im⁡τ>0}\mathbb H=\{\tau\in\mathbb C:\operatorname{Im}\tau>0\} be the upper half-plane, on which SL2(Z)\mathrm{SL}_2(\mathbb Z) acts by Möbius transformations

(abcd)⋅τ=aτ+bcτ+d,\begin{pmatrix} a & b\\ c & d\end{pmatrix}\cdot\tau=\frac{a\tau+b}{c\tau+d},

and let

Γ(2)={γ∈SL2(Z):γ≡(1001)(mod2)}\Gamma(2)=\Bigl\{\gamma\in\mathrm{SL}_2(\mathbb Z):\gamma\equiv\begin{pmatrix}1&0\\0&1\end{pmatrix}\pmod 2\Bigr\}

be the principal congruence subgroup of level 22.

For every τ∈H\tau\in\mathbb H there is a neighbourhood UU of τ\tau in H\mathbb H such that, for every γ∈Γ(2)\gamma\in\Gamma(2),

γ(U)∩U≠∅⟹γ=±I.\gamma(U)\cap U\neq\varnothing\quad\Longrightarrow\quad\gamma=\pm I .

In words: Γ(2)\Gamma(2) acts properly discontinuously on H\mathbb H, and the induced action of Γ(2)/{±I}\Gamma(2)/\{\pm I\} is free. This is the group-theoretic half of the classical fact that the modular function λ\lambda exhibits H\mathbb H as a covering space of C∖{0,1}=H/Γ(2)\mathbb C\setminus\{0,1\}=\mathbb H/\Gamma(2), which in turn gives Milnor's Lemma 2.5 for the triply punctured sphere C^∖{0,1,∞}\hat{\mathbb C}\setminus\{0,1,\infty\}.

Formalization Note H\mathbb H is Mathlib's UpperHalfPlane, Γ(2)\Gamma(2) is CongruenceSubgroup.Gamma 2, a subgroup of SL(2, ℤ), and γ⋅τ\gamma\cdot\tau is Mathlib's action of SL(2, ℤ) on ℍ. The condition γ(U)∩U≠∅\gamma(U)\cap U\neq\varnothing is written as "some σ∈U\sigma\in U has γ⋅σ∈U\gamma\cdot\sigma\in U". The matrix −I-I acts trivially on H\mathbb H, which is why the conclusion is γ=1\gamma=1 or γ=−1\gamma=-1.

Preamble
import Mathlib

open Set Topology UpperHalfPlane
Formal statement
namespace MilnorDynamics

theorem gammaTwo_smul_nhds_disjoint (τ : ℍ) :
    ∃ U ∈ 𝓝 τ, ∀ γ ∈ CongruenceSubgroup.Gamma 2,
      (∃ σ ∈ U, γ • σ ∈ U) → γ = 1 ∨ γ = -1 := 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