Prove2Me

The box over a rhombus is a fundamental domain for the Bianchi group PSL2(Z[ω])\mathrm{PSL}_2(\mathbb{Z}[\omega])

Proved
Thurston23.isFundamentalDomain_eisBox

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

hyperbolic-geometrykleinian-groupsthurston-question-23

The box

B={(x,y,t):0≤x≤12, 0≤x+3 y≤1, x2+y2+t2≥1}B = \{(x,y,t) : 0 \le x \le \tfrac12,\ 0 \le x + \sqrt3\,y \le 1,\ x^2 + y^2 + t^2 \ge 1\}

is a fundamental domain, in the sense of Mathlib's MeasureTheory.IsFundamentalDomain, for the Bianchi group SL2(Z[ω])\mathrm{SL}_2(\mathbb{Z}[\omega]) modulo the kernel of its action on hyperbolic 33-space. The rhombus {0≤x≤12, 0≤x+3y≤1}\{0 \le x \le \tfrac12,\ 0 \le x + \sqrt3 y \le 1\} is a third of the hexagonal Voronoi cell of the lattice Z[ω]\mathbb{Z}[\omega], and so a fundamental domain for its translations together with the rotations by ω\omega. Every orbit meets BB (a point of maximal height, translated to the Voronoi cell of 00, lies above the unit sphere, and a rotation by a power of ω\omega brings it over the rhombus); an element carrying a point of the interior of BB into the interior acts trivially; and the boundary of BB has volume zero. Consequently the hyperbolic volume of BB is the covolume of PSL2(Z[ω])\mathrm{PSL}_2(\mathbb{Z}[\omega]).

Preamble
import Definitions.Def_Thurston23_eisenstein
Formal statement
namespace Thurston23

open MeasureTheory

theorem isFundamentalDomain_eisBox :
    MeasureTheory.IsFundamentalDomain EisEff eisBox hvol := 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). J. Elstrodt, F. Grunewald, J. Mennicke, Groups Acting on Hyperbolic Space, Springer 1998, Chapter 7 (Bianchi groups and Humbert's formula). Formalisation: https://github.com/t4v1/thurston23/blob/main/Thurston23Eisenstein.lean (isFundamentalDomain_eisBox).

View graph