The index of $\Gamma(2+i)$ in the effective Picard group is $60$

Proved

Thurston23.index_gammaTwoIEff

by t4v1 · Sep 13, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

hyperbolic-geometrykleinian-groupsthurston-question-23

The image of $\Gamma(2+i)$ in the effective Picard group $\mathrm{PicardEff} = \mathrm{SL}_2(\mathbb{Z}[i])/\{\pm 1\}$ has index $60$ . Two facts combine. First, reduction modulo $2+i$ maps $\mathrm{SL}_2(\mathbb{Z}[i])$ onto $\mathrm{SL}_2(\mathbb{Z}[i]/(2+i)) \cong \mathrm{SL}_2(\mathbb{F}_5)$ , a group of order

|\mathrm{SL}_2(\mathbb{F}_5)| = 5\,(5^2 - 1) = 120,

so $[\mathrm{SL}_2(\mathbb{Z}[i]) : \Gamma(2+i)] = 120$ . Second, the kernel of the action of the Picard group on hyperbolic space is exactly $\{\pm 1\}$ , and $-1 \notin \Gamma(2+i)$ since $-1 \not\equiv 1 \pmod{2+i}$ ; so passing to the effective quotient halves the index. The statement is what pins the covolume of $\Gamma(2+i)$ to a number: $60$ times the volume of the half box.

Preamble

import Definitions.Def_Thurston23_picard

Formal statement

namespace Thurston23

open MeasureTheory

theorem index_gammaTwoIEff : gammaTwoIEff.index = 60 := by
  sorry

end Thurston23

Source

W. P. Thurston, Three-dimensional manifolds, Kleinian groups and hyperbolic geometry, Bull. Amer. Math. Soc. 6 (1982), 357-381, Question 23 (p. 380). Formalisation: https://github.com/t4v1/thurston23/blob/58bb3fd/Thurston23.lean#L3153-L3165 (with sections IndexOfGamma and KernelPmOne).

View graph

The index of Γ(2+i)\Gamma(2+i)Γ(2+i) in the effective Picard group is 606060

The index of $\Gamma(2+i)$ in the effective Picard group is $60$